我将尝试首先明确问题，然后尝试将其简化为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 是描述“星期结束”的某个常量)
输出：当且仅当存在某个集合时为 True：
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 当且仅当 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(y1,x2) OR Smaller(y2,x1)
现在，让我们定义新的条款来处理它：
对于每一对类a、b和它们中的区间c、d（c位于a中，d位于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，则它们不重叠。
小提示：这个公式允许从每个类别中选择多个间隔，但是如果存在某个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问题，然后将解决方案转化为原始问题可接受的解决方案。