我将尝试首先将问题形式化，然后尝试将其简化为 SAT。
将班级调度问题定义为：
Input = { S1,S2,....,Sn | Si = {(x_i1, y_i1), (x_i2, y_i2) , ... , (x_ik, y_ik) | 0 <= x_ij < y_ij <= M } }
非正式地：输入是一组类，每个类是一组（开放）间隔，形式为 (x,y)
（M 是描述“一周结束”的一些常数）
输出：当且仅当存在某些集合时为真：
R = { (x_1j1, y_1j1) , ..., (x_njn, y_njn) | for each a,b: (x_aja,y_aja) INTERSECTION (x_bjb,y_bjb) = {} }
非正式地：当且仅当存在一些间隔分配使得每对间隔之间的交集为空时才为真。
减少到SAT：
为每个区间定义一个布尔变量，V_ij
在此基础上定义公式：
F1 = (V_11 OR V_12 OR ... OR V_1(k_1)) AND .... AND (V_n1 OR V_n2 OR ... OR V_n(k_n))
非正式地，当且仅当每个类的至少一个区间“满足”时，才满足 F1
定义Smaller(x,y) = true如果且仅if x <= y1
我们将使用它来确保间隔不重叠。
请注意，如果我们想确保 (x1,y1) 和 (x2,y2) 不重叠，我们需要：
x1 <= y1 <= x2 <= y2 OR x2 <= y2 <= x1 <= y1
由于输入保证x1<=y1, x2<=y2，它减少到：
y1<= x2 OR y2 <= x1
并使用我们的 Smaller 和 boolean 子句：
Smaller(y1,x2) OR Smaller(y2,x1)
现在，让我们定义新的子句来处理它：
对于每对类 a,b 和其中的区间 c,d (c in a, d in b)
G_{c,d} = (Not(V_ac) OR Not(V_bd) OR Smaller(y_ac,x_bd) OR Smaller(y_bd,x_ac))
非正式地，如果不使用间隔 b 或 d 之一 - 子句得到满足，我们就完成了。否则，两者都使用，我们必须确保两个区间之间没有重叠。
这保证了如果 c,d 都是“选择的”——它们不会重叠，这对于每对间隔都是正确的。
现在，形成我们的最终公式：
F = F1 AND {G_{c,d} | for each c,d}
这个公式确保我们：
- 对于每一类，至少选择一个区间
- 对于每两个间隔 c,d - 如果同时选择 c 和 d，则它们不会重叠。
小提示：这个公式允许从每个类中选择超过 1 个区间，但是如果有一些 t>1 区间的解，您可以轻松删除其中的 t-1 个，而不会改变解的正确性。
最后，选择的区间是我们定义的布尔变量 V_ij。
例子：
Alebgra = {(1,3),(3,5),(4,6)} Calculus = {(1,4),(2,5)}
定义 F：
F1 = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)
定义 G：
G{A1,C1} = Not(V1,1) OR Not(V2,1) OR 4 <= 1 OR 3 <= 1 //clause for A(1,3) C(1,4)
= Not(V1,1) OR Not(V2,1) OR false =
= Not(V1,1) OR Not(V2,1)
G{A1,C2} = Not(V1,1) OR Not(V2,2) OR 3 <= 2 OR 5 <= 1 // clause for A(1,3) C(2,5)
= Not(V1,1) OR Not(V2,2) OR false =
= Not(V1,1) OR Not(V2,2)
G{A2,C1} = Not(V1,2) OR Not(V2,1) OR 5 <= 1 OR 4 <= 3 //clause for A(3,5) C(1,4)
= Not(V1,2) OR Not(V2,1) OR false =
= Not(V1,2) OR Not(V2,1)
G{A2,C2} = Not(V1,2) OR Not(V2,2) OR 5 <= 2 OR 5 <= 3 // clause for A(3,5) C(2,5)
= Not(V1,2) OR Not(V2,2) OR false =
= Not(V1,2) OR Not(V2,2)
G{A3,C1} = Not(V1,3) OR Not(V2,1) OR 4 <= 4 OR 6 <= 1 //clause for A(4,6) C(1,4)
= Not(V1,3) OR Not(V2,1) OR true=
= true
G{A3,C2} = Not(V1,3) OR Not(V2,2) OR 6 <= 2 OR 5 <= 4 // clause for A(4,6) C(2,5)
= Not(V1,3) OR Not(V2,2) OR false =
= Not(V1,3) OR Not(V2,2)
现在我们可以展示我们的最终公式：
F = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)
AND Not(V1,1) OR Not(V2,1) AND Not(V1,1) OR Not(V2,2)
AND Not(V1,2) OR Not(V2,1) AND Not(V1,2) OR Not(V2,2)
AND true AND Not(V1,3) OR Not(V2,2)
只有在以下情况下才满足上述条件：
V1,1 = false
V1,2 = false
V1,3 = true
V2,1 = true
V2,2 = false
这代表时间表：代数=（4,6）；微积分=（1,4），根据需要。
(1) 可以很容易地计算为公式的常数，这样的常数有多项式。
我的目标是使用这个求解器在许多不同的 NP 完成问题中找到解决方案。基本上，我将不同的问题转换为 SAT，用我的求解器解决 SAT，然后将解决方案转换为原始问题可接受的解决方案。