我有一些理论框架/实际的问题，我没有线索，现在如何管理，这就是：

我创建了一个 SAT求解能够发现，当一个人存在，并证明的矛盾时，它的一个模型不使用遗传算法用C CNF 问题的情况下。

一个SAT-问题基本上是这样那样的问题： 我的目标是利用该解算器找到了很多型动物的 NP-完成的问题的解决方案。基本上，我翻译型动物问题转化为SAT，SAT解决我的解算器，然后变压器的解决方案到解决方案接受了原问题。

我已经成功换了N * N的数独，也是N皇后问题，但这里是我的新目标：减少排课问题SAT，但我不知道怎么才能正式一类调度问题它之后容易变换饱和

的目的是显而易见的，在数个月，以产生一个时间表的图片像这样的：

我发现这个source-$c$c谁能够解决该类调度，但没有任何减少到SAT遗憾的是：/

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

但规划域定义语言本文中使用似乎很一般，不能用于我重新presents一个类调度问题。 ：/

是否有人对如何才能将其降低到SAT后，改造SAT的解决方案（如果存在的话^^）入类时间表？高效正式A级调度的想法

我的任何建议基本上是开放的，我现在不知道如何重新presents，如何降低的问题，如何将国家税务总局，解决方案到一个时间表......

在此先感谢大家谁都会花一些时间对我的问题， 最好的问候，

我要尝试首次形式化问题，然后尝试将其降低到周六

定义类调度问题为：

 输入= {S1，S2，...，锡|的Si = {（x_i1，y_i1），（x_i2，y_i2），...，（x_ik，y_ik）| 0℃= x_ij＆其中; y_ij＆LT; = M}}
 

通俗地说：输入是一组类，每一类是一组（开放）的形式区间（X，Y） （M是一些常数，它描述了一周结束）

输出：当且仅当存在一些设置：

  R = {（x_1j1，y_1j1），...，（x_njn，y_njn）|对于每个的a，b：（x_aja，y_aja）交点（x_bjb，y_bjb）= {}}
 

非正式：当且仅当有间隔的一些分配，使得每对间隔之间的交集为空

削减至星期六：

定义为每间隔一个布尔变量， V_ij 此基础上，定义公式：

  F1 =（V_11或V_12或者......或者V_1（K_1））AND .... AND（V_n1或V_n2或者......或者V_n（k_n））
 

非正式的，F1是满意的，当且仅当时间间隔为每类至少有一个是满意

定义小（X，Y）=真，当且仅如果x＆LT; = Y 1 我们将用它来确保间隔不重叠。 请注意，如果我们想确保（X1，Y1）和（x2，y2）上不重叠，我们需要：

  X1＆LT; = Y1＆LT; = X＆LT; = Y2和X2＆LT; = Y2＆LT; = X1＆LT; = Y1
 

由于输入的保证 X1＆LT; = Y1，X2＆LT; = Y2 ，它简化为：

  Y1＆LT; = X2或Y2＆LT; = X1
 

和使用我们的小型和布尔条款：

 小（Y1，X2）或更小（Y2，X1）
 

现在，让我们来定义新的条款来处理它：

有关每一对的类A，B和间隔C，D在其中（三中A，D b）中

  G_ {C，D} =（NOT（V_ac）否（V_bd）或更小（y_ac，x_bd）或更小（y_bd，x_ac））
 

通俗地说，如果间隔B或D一种是不使用 - 该条款得到满足，我们正在做。否则，两者同时使用，我们必须确保有两个区间之间没有重叠。 这保证如果两个C，D是选择 - 它们不重叠，并且这是适用于每对间隔

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

  F = f1和{G_ {C，D} |对于每个C，D}
 

这个公式可以确保我们：

小记：这个公式允许选择1个多区间为每个类，但如果有一些T> 1间隔的解决方案，可以轻松去除T-1它们不改变溶液的正确性

目前结束时，所选择的间隔是布尔变量V_ij我们定义

示例：

  Alebgra = {（1,3），（3,5），（4,6）}积分= {（1,4），（2,5）}
 

定义F：

  F =（v 1.1或v 1.2或V1,3）AND（V2,1或V2,2）
 

定义G的：

 1 intervals, you can easily remove t-1 of them without changing correctness of the solution.


At the end, the chosen intervals are the boolean variables V_ij we defined.



Example:
Alebgra = {(1,3),(3,5),(4,6)} Calculus = {(1,4),(2,5)}
Define F:
F = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)
Define 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} 
Now we can show our final formula:
    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}
The above is satisfied only when:
V1,1 = false
V1,2 = false
V1,3 = true
V2,1 = true
V2,2 = false
And that stands for the schedule: Algebra=(4,6); Calculus=(1,4), as desired.



(1) can be computed as a constant to the formula pretty easily, there are polynomial number of such constants.