为什么 NoRoomConflicts 会在NoRoomConflicts_alt "works"时生成二元关系

Question

考虑下面的合金模型，这是学生提交的剥离版本。问题是一个课程调度系统，学生试图说没有冲突（同时在同一地方举行的两个不同的课程）：

abstract sig Room{}
one sig S20, S30, S50 extends Room{}
abstract sig Period{}
one sig Mon, Tue, Wed, Thu, Fri extends Period{}
// Courses and the room and periods when they meet.
some sig Course {
  where : Room,
  when  : some Period
}
// No two Courses with any common meeting Periods can be
// in the same Room - from the student.
pred NoRoomConflicts_student {
  no c : Course |  no d : Course |
    c != d && some c.when & d.when && d.where = c.where
}
run NoRoomConflicts_student
// No two Courses with any common meeting Periods can be
// in the same Room - my recasting.
pred NoRoomConflicts_alt {
  no c : Course, d : Course |
    c != d && some c.when & d.when && d.where = c.where
}
run NoRoomConflicts_alt

当运行noroomconflicts_alt时，我们获得了符合规格的解决方案

但是，当运行noroomconflicts_student时，突然" D"成为课程和解决方案之间的二进制关系。

（a）为什么" d"以这种方式转换？

（b）给定（a），c！= d不应该引起类型错误吗？

注意：我不是声称这两个谓词是等效的（我的头部疼痛试图做双重否定） - 我只想知道当运行noroomconflicts时，" D"突然成为二进制关系。

版本：合金分析仪4.2_2015-02-22（构建日期：2015-02-22 18:21 EST）

Answer 1

首先，您在解决方案中看到的是某些量化变量（在这种情况下为d）会被化为skolemed，以便您可以看到它们的值。如果您要求解表单的约束（所有x | some y | ...），则y的skolemization值必须是一个关系 - 给出每个x的y值。这不是合金变量的实际类型，这就是为什么没有类型错误的原因。有关完整说明，请参见我的书的第5.2.2节（软件摘要）。

第二，两个公式不是相同的。这在我的书的第293页上进行了解释。简而言之，这是因为" no c，d | p"意味着您找不到c和d，因此p和" no c | no d | p"表示您找不到Ca d p。