类布尔到布尔可满足性

我有一些理论/实践问题，我现在还不知道如何pipe理，这里是：

我创build了一个SAT求解器 ，当存在一个SAT求解器时，它可以find一个模型，并且在使用遗传algorithm的情况下，在C中CNF问题不是这样的情况下certificate矛盾。

SAT问题看起来基本上像这样的问题： 我的目标是使用这个求解器在很多不同的NP完成问题中find解决scheme。 基本上，我将不同的问题转化为SAT，用我的求解器解决SAT，然后将解决scheme转化为原始问题可以接受的解决scheme。

我已经成功的N * N数独和N皇后问题，但这里是我的新目标：为了减less课程排课问题，但我不知道如何forms化类调度问题，以便于转换它在SAT之后。

目标显然是在几个月内产生一个这样的时间表的图片：

我发现这个源代码谁能够解决课程安排，但没有任何削减SAT遗憾：/

我还发现一些关于一般规划的文章（例如http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf ）。

但是这篇文章中使用的规划域定义语言对于我来说似乎是相当普遍的，代表了一个类调度问题。 ：/

是否有人有一个想法，如何有效地forms化类调度，以减less到SAT和之后，将SAT解决scheme（如果存在^^）转换为课程表？

我基本上对任何build议都是开放的，现在我不知道如何expression，如何减less问题，如何将SAT解决scheme转换成时间表。

在此先感谢每一位将在我的问题上花费一些时间的人，最好的问候，

---

后续问题 ： 类调度到布尔可满足性[多项式时间减less]第2部分

Answer 1

我将尝试先将问题正式化，然后尝试将其降至SAT。

将课程安排问题定义为：

Input = { S1,S2,....,Sn | Si = {(x_i1, y_i1), (x_i2, y_i2) , ... , (x_ik, y_ik) | 0 <= x_ij < y_ij <= M } } 

非正式地说：input是一组类，每个类是一组（（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) = {} } 

非正式地：当且仅当存在一定间隔的分配，使得每对间隔之间的交集为空时。

---

减less到SAT：

为每个区间定义一个布尔variablesV_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)) 

非正式地，当且仅当每个class级的间隔中的至less一个“满足”

当且仅if x <= y ^1时 Smaller(x,y) = true定义Smaller(x,y) = true
我们将使用它来确保间隔不重叠。
请注意，如果我们要确保（x1，y1）和（x2，y2）不重叠，我们需要：

 x1 <= y1 <= x2 <= y2 OR x2 <= y2 <= x1 <= y1 

由于input保证x1<=y1, x2<=y2 ，它减less到：

 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都是“被select”的 – 它们不重叠，并且对于每对间隔都是如此。

现在，形成我们的最终公式：

 F = F1 AND {G_{c,d} | for each c,d} 

这个公式确保我们：

1. 对于每个class级，至lessselect一个时间间隔
2. 对于每两个时间间隔c，d – 如果select了c和d，则它们不重叠。

小记：这个公式允许从每个类中select多于一个的时间间隔，但是如果有一个t> 1的时间间隔的解，可以很容易地删除它们中的t-1而不改变解的正确性。

最后，select的间隔是我们定义的布尔variablesV_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's：

 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）可以很容易地计算为公式的常数，这样的常数有多项式数。