类调度到布尔可满足性[多项式时间缩减]

Question

我有一些理论/实际问题,我现在还没有关于如何管理的线索,这里是:

我创建了一个SAT求解器,能够在存在模型时找到模型,并且当使用遗传算法在C中出现CNF问题时,不能证明矛盾.

SAT问题看起来基本上就像这样的问题: 我的目标是使用此求解器在许多不同的NP完成问题中找到解决方案 .基本上,我将不同的问题转换为SAT,用我的求解器解决SAT,然后将解决方案转换为原始问题可接受的解决方案.

我已经成功完成了N*N Sudoku以及N-queens问题,但这是我的新目标:将类调度问题减少到SAT,但我不知道如何形成类调度问题以便轻松转换它在SAT之后.

显然,在几个月内,我们的目标就是制作一张如下图所示的时间表:

我发现这个源代码能够解决类调度但不幸的是没有减少SAT:/

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

但是,本文中使用的规划域定义语言似乎对我来说过于笼统,以表示类调度问题.:/

是否有人知道如何有效地形成类调度以便将其减少到SAT以及之后,将SAT解决方案(如果它存在^^)转换为类调度？

我基本上对任何建议持开放态度,我现在不知道如何表示,如何减少问题,如何将SAT解决方案转换为计划......

---

跟进问题:类调度到布尔可满足性[多项式时间减少]第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 } } 

非正式:输入是一组类,每个类是(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) = trueif和仅if x <= y¹
我们将使用它来确保间隔不重叠.
请注意,如果我们想确保(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}

这个公式确保我们:

1. 对于每个班级,至少选择一个班次
2. 对于每两个间隔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)可以很容易地计算公式的常数,这样的常数有多项式数.