algorithm - bool 可满足性的类调度 [多项式时间缩减] 第 2 部分

Question

我几天前问了一个关于如何将大学类(class)安排问题转化为 bool 可满足性问题的问题。

( Class Scheduling to Boolean satisfiability [Polynomial-time reduction] )

我得到了@Amit 的回答，他非常优雅且易于编码。基本上，他的回答是这样的:他考虑的不是类(class)，而是时间间隔。

所以对于第 i 门类(class)，他只是控诉了这门类(class)的所有可能间隔。当每个类(class)至少有 1 个真实区间并且没有区间重叠时，我们获得了一个解决方案。

当我们只考虑类(class)而不考虑其他时，这种方法非常有效。我通过对间隔内的房间进行编码来概括它。

例如，不用 [8-10] 来表示类(class)可以在上午 8 点到 10 点之间进行。

我用 [0.00801 - 0.01001] 表示类(class)可以在早上 8 点到 10 点之间在房间 1 上课。

我确定您目前正在徘徊“为什么要使用 double ？”好吧，因为我的问题来了:

为了继续推广这种方法，我还在这个区间内编码了教师的编号。

我用 [1.00801 - 1.01001] 表示类(class)可以在早上 8 点到 10 点之间在房间 1 上课，由老师 n°1 教授。

这是我现在得到的:

像这样 [1.008XX - 1.010XX] 可以和 [2.008YY - 2.010YY] 同时发生，这是真的，如果老师 1 在早上 8 点到 10 点之间在 X 教室上课，老师 2 可以上午 8 点到 10 点之间也在 Y 教学，当且仅当房间可用时。

问题是:使用这种方法我不能保证 XX 和 YY 会不同并且 YY 可用，因为 [1.008XX - 1.010XX] 不与 [2.008XX - 2.010XX] 重叠，所以现在，求解器认为这是可能的。

而且我仍然不知道如何通过使用这种间隔方法来确保这一点......我需要一种编码 {Interval, room and teacher-id} 的方法，以便:

• 老师不能在同一时间段内出现在两个地方。
• 同一个房间不能有 2 位老师在同一个时间间隔内。
• 类(class)至少有 1 个区间为真。

在此先感谢您的帮助，此致 !

---

跟进问题: Class Scheduling to Boolean satisfiability [Polynomial-time reduction] Final Part

Answer 1

这个答案是 Part 1's answe 的扩展r，并尽可能使用相同的符号。

好的，假设每个区间都分配给一位教师(如果不止一位教师可以采用区间，只需有多个实例，每个实例有不同的教师)，所以要指示教师 t在时间 x 到 y 的教室 p 上课，我们可以使用这个类给出的旧变量 - V_{i ,j} - 用于类别和间隔。

对于每个教师 t 和每对区间 c=(x1,y1), d=(x2,y2)在老师可能参加的类(class) (a,b) 中，添加子句:

Q_{t,i,j} = Not(V_ac) OR Not(V_bd) OR Smaller(y1,x2) OR Smaller(y2,x1)

直觉上，上面的条款保证了一个老师不能同时出现在两个地方——分配给他们的同一个老师没有间隔重叠。

通过将每位教师 t 的每一对 (i,j) 与 AND 链接到原始公式，它满足您的第一个约束 - 教师不能在同一时间间隔的 2 个地方。 - 因为每个老师不能同时在两个地方。

你的第二个约束不能有 2 位老师在相同的时间间隔内出现在同一个房间里。 也满足了这样一个事实，即不能有两个类(class)的时间和类(class)重叠。

第三个约束类(class)至少有 1 个区间为真。 由 F1 子句满足，因为您必须选择至少一个区间(有一位老师分配)为每门类(class)。