DPLL Algorithm

DPLL(\(T\)) Algorithm

无量词理论(Quantifier-Free Theories)

考虑存在如下断言: \[ \begin{eqnarray*} &&(x_1=x_2\lor x_1=x_3)\land(x_1=x_2\lor x_1=x_4)\land x_1\neq x_2\land x_1\neq x_3 \land x_1\neq x_4, \tag{1}\\ &&((x_1+2x_3<5)\lor\neg(x_3\le1)\land(x_1\ge3)), \tag{2}\\ &&(i=j\land a[j]=1)\land\neg(a[j]=1).\tag{3} \end{eqnarray*} \]

上述三个断言都是与之相对应的等式断言, 线性演算断言和数组逻辑断言. 有一个通用的框架来定义这些断言, 就是一阶逻辑(first-order logic). 需要注意的是, 上述三个公式都是无量词修饰(quantifier-free)的, 或者说没有范阈限制, 一阶逻辑理论(first-order theory).

存在一个框架或者说一个判定过程, 用以解决上述可判定的无量词一阶逻辑理论问题, 并且是由 CDCL 框架泛化而来, 通常称为 DPLL(\(T\)).

DPLL(\(T\)) 概述

每一个理论 \(T\) 都是定义在一个符号集合 \(\Sigma\) 上的. 在等式逻辑的例子中, \(\Sigma=\{'='\}\). 当定义 \(\Sigma\) 上的文字或者原子或者公式的时候, 就意味着, 公式中的文字只能使用 \(\Sigma\) 中的符合. 用 \(at(\varphi)\) 表示一个给定否定范式公式 \(\varphi\) 的 \(\Sigma\) 原子的集合, 用 \(at_i(\varphi)\) 表示公式 \(\varphi\) 中第 \(i\) 个原子. 对于给定的原子 \(a\), 用 \(e(a)\) 来表示这个原子的布尔编码, 将其扩展到在符号集合 \(\Sigma\) 上的公式 \(t\), 用 \(e(t)\) 来表示将 \(t\) 中的每一个原子对应的布尔编码代入公式所形成的布尔公式. 比如说, 如果 \(x=y\) 是定义在符号集合 \(\Sigma\) 上的原子命题, 那么布尔变量 \(e(x=y)\) 就表示它的编码. 如果 \[ \varphi := x=y\lor x=z. \] 是一个定义在符号集合 \(\Sigma\) 上的公式(\(\Sigma\)-formula), 那么 \[ e(\varphi) := e(x=y)\lor e(x=z). \] 对于一个 \(\Sigma\)-formula 公式 \(\varphi\) 来说, 布尔公式 \(e(\varphi)\) 被称作公式 \(\varphi\) 的命题框架(propositional skeleton).

假设一个等式逻辑公式 \(\varphi\), \[ \varphi := x=y \land((y=z\land \neg(x=z))\lor x=z). \] 公式 \(\varphi\) 的命题框架是 \[ e(\varphi) := e(x=y)\land((e(y=z)\land\neg e(x=z))\lor e(x=z)). \] 布尔公式 \(\mathcal{B}\) 设值为 \(e(\varphi)\), 记为 \(\mathcal{B} := e(\varphi)\).

下一步, 将公式 \(\mathcal{B}\) 传给一个 SAT 求解器. 假设, 经过求解器的求解, SAT 给判定过程 \(DP_T\) 返回了一组使得公式可满足的赋值.

\(DP_T\): 一个理论 T(theory)是定义在符号集合 \(\Sigma\) 的, 符合理论 \(T\) 定义的文字是 \(T\)-文字, \(DP_T\) 程序就是针对 \(T\)-文字合取式的判定过程.

\[ \alpha := \{e(x=y)\mapsto {\rm TRUE}, e(y=z)\mapsto {\rm TRUE}, e(x=z)\mapsto {\rm FALSE}\}. \]

判定过程 \(DP_T\) 要判定一组文字所对应的这组赋值的合取式是否是可满足的. 这个合取式记为 \(\hat{Th(\alpha)}\). 对于上面的一组赋值, \[ \hat{Th(\alpha)} := x=y\land y=z\land\neg(x=z). \] 显然, 这个公式是不可满足的, 也就是说这个公式的否定是重言式. 因此要被添加到公式 \(\mathcal{B}\) 中, 这里说明一下, 为什么要把重言式添加到公式中, 因为重言式并不会影响公式的判定结果, 为了提高判定过程的执行效率, 就需要让求解器知道哪些赋值是无意义的, 比如此例, 如果不将该重言式添加到公式 \(\mathcal{B}\) 中, 那么 SAT 求解器就可能重复赋值, 而影响判定过程的执行效率. 该重言式的布尔编码: \[ e(\neg\hat{Th(\alpha)}) := (\neg e(x=y)\lor\neg e(y=z)\lor e(x=z)). \] 这个子句是与当前的赋值相矛盾的, 所以要阻止其被重复赋值. 这种子句称为封锁子句(blocking clause). 通常, 将 \(DP_T\) 过程所返回的结果记为 \(t\), 也称为引理(lemma). 在上述例子中, \(t := \neg\hat{Th(\alpha)}\), 也就是说, 这个引理是完全赋值 \(\alpha\) 的否定, 并且是一个子句, 但是通常 \(t\) 是多子句的形式, 这取决于 \(DP_T\) 的实现形式.

在封锁子句添加到公式中后, SAT 求解器再次被调用并给公式赋新值, 比如说, \[ {\alpha}' := \{ e(x=y)\mapsto {\rm TRUE}, e(y=z)\mapsto{\rm TRUE}, e(x=z)\mapsto{\rm TRUE} \}. \] 那么, 对应的 \(\Sigma\)-公式 \[ {\hat Th(\alpha')} := x=y\land y=z\land x=z. \] 是可满足的, 也说明原公式 \(\varphi\) 是可满足的. 可以看到, 只要是满足 \({\hat Th(\alpha')}\) 的赋值同样是满足公式 \(\varphi\) 的.

当然, 如果原公式 \(\varphi\) 大小线性甚至指数增加, 通过完全赋值的方法显然效率很低. 有很多种提升效率的方法, 在对子句进行部分赋值之后即调用判定过程 \(DP_T\), 而不是等到全部赋值之后. 一组相矛盾的部分赋值能够得到更加强大的引理 \(t\), 因为它可以组织所有对它进行扩展的赋值. 另外, 如果一组部分赋值不是矛盾的, 那也可以回传给 SAT 求解器用以更进一步的推导. 比如上面的例子, 存在一组部分赋值 \[ \alpha := \{ e(x=y)\mapsto {\rm TRUE}, e(y=z) \mapsto {\rm TRUE} \}. \] 所对应要传递给 \(DP_T\) 的合取公式 \[ {\hat Th(\alpha)} := x=y\land y=z. \] 这个公式能够让 \(DP_T\) 推导出 \(x=z\), 同时能够让 SAT 求解器知道, 根据当前的部分赋值 \(\alpha\) 能够推导出 \(e(x=z)\mapsto {\rm TRUE}\). 因此, 类比在 SAT 求解器种的布尔约束传播(Boolean constraint propagation), 这里可以称作是理论传播(theory propagation). 这种传播可能会导致进一步的布尔约束传播, 也就是说这个过程在 SAT 求解器做出下一个判定之前可能会迭代很多次.

现在引出一个算法, LAZY-BASIC(算法1), 用以判定一个 \(T\)-公式 \(\varphi\) 是否是可满足的. 这个算法的做法是, 从公式 \(\mathcal{B}=e(\varphi)\) 开始, 迭代地对命题公式 \(\mathcal{B}\) 进行求解, 并用DEDUCTION(演绎推理)方法计算出的约束条件的编码逐步增强这一过程. \[ \begin{aligned} &\mathbf{Algorithm\ 1:}\ \rm LAZY\mbox{-}BASIC\\ &\mathbf{Input:}\ {\rm A\ formula}\ \varphi\\ &\mathbf{Output:}\ {\rm ''Satisfiable''\ if}\ \varphi\ {\rm is\ satisfiable,\ and\ ''Unsatisfiable''\ otherwise}\\ &\\ &1.\hspace{2mm}\mathbf{function\ }{\rm LAZY\mbox{-}BASIC}(\varphi)\\ &2.\hspace{10mm}\mathcal{B}:=e(\varphi);\\ &3.\hspace{10mm}\mathbf{while\ }{\rm(TRUE)\ }\mathbf{do}\\ &4.\hspace{16mm}\langle\alpha,res\rangle:={\rm SAT\mbox{-}SOLVER}(\mathcal{B});\\ &5.\hspace{16mm}\mathbf{if\ }res={\rm ''Unsatisfiable''\ }\mathbf{then\ return\ }{\rm ''Unsatisfiable''};\\ &6.\hspace{16mm}\mathbf{else}\\ &7.\hspace{23mm}\langle t,res\rangle:={\rm DEDUCTION}(\hat{Th}(\alpha));\\ &8.\hspace{23mm}\mathbf{if\ }res={\rm ''Satisfiable''\ }\mathbf{then\ return\ }{\rm ''Satisfiable''};\\ &9.\hspace{23mm}\mathcal{B}:=\mathcal{B}\land e(t); \end{aligned} \] LAZY-BASIC算法其实在上一小节已经大致说明了, 这里再总结一下. 算法首先将公式 \(\varphi\) 进行布尔编码赋值给 \(\mathcal{B}\), 进入循环体. 公式 \(\mathcal{B}\) 传给 SAT 求解器, 并返回一个元组 \(<assignment, result>\), 其中 \(assignment\)中包含的就是使得公式 \(\mathcal{B}\) 可满足的一组赋值, 而 \(result\) 是说明公式是否可满足; 进入判断, 如果不可满足, 那么整个公式就是不可满足的. 否则, 将布尔编码对应的 \(T\)-文字合取式传给 DEDUCTION(), 判断 \(\hat{Th(\alpha)}\) 公式是否是可满足的, 并同样返回一个元组; 如果结果是可满足的, 如前文所说, 那么整个公式就是可满足的. 否则, 就把这组赋值对应的布尔编码添加到公式 \(\mathcal{B}\) 中, 以防止重复赋值. 当然, 可以把这个算法集成到 CDCL-SAT 中去, 以获得更高的效率. 算法2就是在 CDCL-SAT 求解器中集成了 DEDUCTION方法的算法. \[ \begin{aligned} &\mathbf{Algorithm\ 2:\ }{\rm LAZY\mbox{-}CDCL}\\ &\mathbf{Input:}\ {\rm A\ formula}\ \varphi\\ &\mathbf{Output:}\ {\rm ''Satisfiable''\ if\ the\ formula\ }\ {\rm is\ satisfiable,\ and\ ''Unsatisfiable''\ otherwise}\\ \\ &1.\hspace{2mm}\mathbf{function}\ {\rm LAZY\mbox{-}CDCL} \\ &2.\hspace{10mm}{\rm ADDCLAUSES}(cnf(e(\varphi))); \\ &3.\hspace{10mm}\mathbf{while\ }{\rm TRUE\ }\mathbf{do} \\ &4.\hspace{18mm}\mathbf{while\ }{\rm (BCP()\ =\ ''conflict'')}\ \mathbf{do} \\ &5.\hspace{26mm}backtrack\mbox{-}level:={\rm ANALYZE\mbox{-}CONFLICT()}; \\ &6.\hspace{26mm}\mathbf{if\ }backtrack\mbox{-}level<0\ \mathbf{then\ return\ }{\rm ''Unsatisfiable''}; \\ &7.\hspace{26mm}\mathbf{else\ }{\rm BackTrack}(backtrack\mbox{-}level);\\ &8.\hspace{18mm}\mathbf{if\ }{\rm \neg DECIDE()\ }\mathbf{then}\hspace{55mm}\triangleright\ {\rm Full\ assignment} \\ &9.\hspace{26mm}\langle t,res\rangle:={\rm DEDUCTION}(\hat{Th}(\alpha));\hspace{19.5mm}\triangleright\ {\rm \alpha\ is\ the\ assignment}\\ &10.\hspace{24mm}\mathbf{if\ }res={\rm ''Satisfiable''\ }\mathbf{then\ return\ }{\rm ''Satisfiable''};\\ &11.\hspace{24mm}{\rm ADDCLAUSES}(e(t)); \\ \end{aligned} \]

理论传播和DPLL(\(T\))框架

但是 LAZY-CDCL 算法可以进一步优化. 比如说, 在公式 \(\varphi\) 中有一个变量 \(x_1\), 存在两个文字分别是 \(x_1\ge 10\) 和 \(x_1\lt 0\). 假设在 DECIDE() 过程中, 两个文字分别被赋值为 \(e(x_1\ge 10)\mapsto \rm TRUE\) 和 \(e(x_1\lt 0)\mapsto \rm TRUE\). 不可避免地，任何对DEDUCTION() 的调用都会存在这两个事实之间的矛盾, 而与任何其他判定无关. 但是算法2直到完全赋值之后才执行 \(then\) 之后的语句, 所以用以进行完全赋值的时间就被浪费了. 而且, 如果完全赋值被拒绝了, 也就是说一组完全复制不能使公式可满足, 那么可能是由于一组赋值的子集存在矛盾的情况, 换句话说, 上述错误的赋值可能并没有被排除在外, 这就造成了效率的极大降低. 所以, 可以考虑把 DEDUCTION 提前, 在未完全赋值之前执行. 这样做有两个目的:

1. 矛盾的赋值可以尽早排除.
2. 那些尚未被赋值的蕴涵信息可以告知 SAT 求解器. 继续上述例子, 如果 \(e(x_1\ge 10)\mapsto \rm TRUE\), 那么就可一断定 \(e(x_2\lt 0)\) 赋值为 \(\rm FALSE\), 以避免冲突的赋值.

这就引出了优化之后的算法, DPLL(\(T\)). 如算法3所示. \[ \begin{aligned} &\mathbf{Algorithm\ 3:\ }{\rm DPLL}(T)\\ &\mathbf{Input:}\ {\rm A\ formula}\ \varphi\\ &\mathbf{Output:}\ {\rm ''Satisfiable''\ if\ the\ formula\ }\ {\rm is\ satisfiable,\ and\ ''Unsatisfiable''\ otherwise}\\ \\ &1.\hspace{2mm}\mathbf{function}\ {\rm DPLL}(T) \\ &2.\hspace{10mm}{\rm ADDCLAUSES}(cnf(e(\varphi))); \\ &3.\hspace{10mm}\mathbf{while\ }{\rm TRUE\ }\mathbf{do} \\ &4.\hspace{18mm}\mathbf{repeat}\\ &5.\hspace{26mm}\mathbf{while\ }{\rm (BCP()\ =\ ''conflict'')}\ \mathbf{do} \\ &6.\hspace{34mm}backtrack\mbox{-}level:={\rm ANALYZE\mbox{-}CONFLICT()}; \\ &7.\hspace{34mm}\mathbf{if\ }backtrack\mbox{-}level<0\ \mathbf{then\ return\ }{\rm ''Unsatisfiable''}; \\ &8.\hspace{34mm}\mathbf{else\ }{\rm BackTrack}(backtrack\mbox{-}level);\\ &9.\hspace{26mm}\langle t,res\rangle:={\rm DEDUCTION}(\hat{Th}(\alpha));\\ &10.\hspace{24mm}{\rm ADDCLAUSES}(e(t));\\ &11.\hspace{16mm}\mathbf{until\ }t\equiv{\rm TRUE};\\ &12.\hspace{16mm}\mathbf{until\ }\alpha\ {\rm is\ a\ }full\ {\rm assignment\ }\mathbf{then\ return\ }{\rm ''Satisfiable''};\\ &13.\hspace{16mm}{\rm DECIDE()};\\ \end{aligned} \] 下面对 DPLL(\(T\)) 做简要说明. 内层的 while 循环还是执行布尔约束传导判断是否存在冲突, 这与 CDCL 算法的主要部分是一致的. 重要的是集成了 DEDUCTION(), 判断文字布尔编码对应的合取范式是否是可满足的. 不论是否可满足都将其加入到原公式中去, 如果是可满足, 那么不影响最终判定结果; 如果不满足, 那么就将矛盾的赋值排除在外. 外层的 repeate 循环直到 DEDUCTION() 返回的结果为真时结束. 并判断赋值公式 \(\alpha\) 是否是完全赋值, 如果是完全赋值, 则原公式可满足. 否则, 同样执行 CDCL 算法中的 DECIDE() 方法, 判断是否没有再可以赋值的变量了, 循环继续. 该算法相较于 CDCL 算法主要的不同之处就在于(当然是对于等式逻辑来说的), 对于子句的部分赋值对应布尔编码的合取式子进行了可满足性的判定, 并通过理论传播策略, 加速了判定过程的执行, 并尽可能早地将造成矛盾条件的赋值剔除, 以达到较好的性能.