排课布尔可满足性[多项式时间减少] [英] Class Scheduling to Boolean satisfiability [Polynomial-time reduction]
问题描述
我有一些理论框架/实际的问题，我没有线索，现在如何管理，这就是：
我创建了一个 SAT求解能够发现，当一个人存在，并证明的矛盾时，它的一个模型不使用遗传算法用C CNF 问题的情况下。
一个SAT-问题基本上是这样那样的问题：
我已经成功换了N * N的数独，也是N皇后问题，但这里是我的新目标：减少排课问题SAT，但我不知道怎么才能正式一类调度问题它之后容易变换饱和
的目的是显而易见的，在数个月，以产生一个时间表的图片像这样的：
我发现这个<一href="http://www.$c$cproject.com/Articles/23111/Making-a-Class-Schedule-Using-a-Genetic-Algorithm">source-$c$c谁能够解决该类调度，但没有任何减少到SAT遗憾的是：/
我也发现有关规划的一般（一些文章<一个href="http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf">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}
这个公式可以确保我们：
- 对于每个类，至少一个间隔被选择
- 对于每两个间隔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的：
现在我们可以证明我们的最终的公式：
F =（v 1.1或v 1.2或V1,3）AND（V2,1或V2,2）
而不是（v 1.1）否（V2,1}而不是（v 1.1）否（V2,2}
而不是（v 1.2）否（V2,1}而不是（v 1.2）否（V2,2}
及真实而不是（V1,3）否（V2,2}
以上是满意的，只有当：
v 1.1 = FALSE
V1,2 = FALSE
V1,3 =真
V2,1 =真
V2,2 = FALSE
这代表了时间表：代数=（4,6）;演算=（1,4），根据需要。
（1）可容易地计算作为常数的公式pretty的，也有这样的常量多项式数目
I have some theorical/practical problem and I don't have clue for now on how to manage, Here it is:
I create a SAT solver able to find a model when one is existing and to prove the contradiction when it's not the case on CNF problems in C using genetics algorithms.
A SAT-problem looks basically like this kind of problem : My goal is to use this solver to find solutions in a lot of differents NP-completes problems. Basically, I translate differents problems into SAT, solve SAT with my solver and then transforme the solution into a solution acceptable for the original problem.
I already succeed for the N*N Sudoku and also the N-queens problems, but here is my new goal : to reduce the Class Scheduling Problem to SAT but I have no idea how to formalize a class-scheduling problem in order to easily transform it in SAT after.
The goal is obviously, in few months, to generate a picture of a schedule like this one :
I found this source-code who is able to solved the class-scheduling but without any reductions to SAT unfortunately :/
I also found some articles about Planning in general (http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf for instance).
But the planning domain definition language used in this article seems quite too general for me to represents a Class-scheduling problem. :/
Does someone has an idea on how to formalize efficiently a Class-scheduling in order to reduce it to SAT and after, transform the SAT solution (if it exists ^^) into a Class-schedule ?
I'm basically open to any suggestions, I for now have no idea on how to represents, how to reduce the problem, how to transform the SAT-solution into a schedule...
Thanks in advance for everyone who will spend some times on my problem, Best regards,
I am going to try and first formalize the problem, and then attempt to reduce it to SAT.
Define the class scheduling problem as:
Input = { S1,S2,....,Sn | Si = {(x_i1, y_i1), (x_i2, y_i2) , ... , (x_ik, y_ik) | 0 <= x_ij < y_ij <= M } }
Informally: The input is a set of classes, each class is a set of (open) intervals in the form (x,y)
(M is some constant that describes the "end of the week")
Output: True if and only if there exists some set:
R = { (x_1j1, y_1j1) , ..., (x_njn, y_njn) | for each a,b: (x_aja,y_aja) INTERSECTION (x_bjb,y_bjb) = {} }
Informally: true if and only if there is some assignment of intervals such that the intersection between each pair of intervals is empty.
Reduction to SAT:
Define a boolean variable for each interval, V_ij
Based on it, define the formula:
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))
Informally, F1 is satisfied if and only if at least one of the interval for each class is "satisfied"
Define Smaller(x,y) = true if and only if x <= y1
We will use it to make sure intervals don't overlap.
Note that if we want to make sure (x1,y1) and (x2,y2) don't overlap, we need:
x1 <= y1 <= x2 <= y2 OR x2 <= y2 <= x1 <= y1
Since the input guarantees x1<=y1, x2<=y2, it reduces to:
y1<= x2 OR y2 <= x1
And using our Smaller and boolean clauses:
Smaller(y1,x2) OR Smaller(y2,x1)
Now, let's define new clauses to handle with it:
For each pair of classes a,b and intervals c,d in them (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))
Informally, if one of the intervals b or d is not used - the clause is satisfied and we are done. Otherwise, both are used, and we must ensure there is no overlap between the two intervals.
This guarantees that if both c,d are "chosen" - they do not overlap, and this is true for each pair of intervals.
Now, form our final formula:
F = F1 AND {G_{c,d} | for each c,d}
This formula ensures us:
- For each class, at least one interval is chosen
- For each two intervals c,d - if both c and d are chosen, they do not overlap.
Small note: This formula allows to chose more than 1 interval from each class, but if there is a solution with some t>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.
这篇关于排课布尔可满足性[多项式时间减少]的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
