SAT 求解器¶
在阅读本文之前，需要有基础的命题逻辑知识。如果你没有听说过合取范式 (CNF) 或是 DPLL 算法, 你可以点击链接前往本站的另一篇教程。
本文主要介绍 CDCL 算法和它的更多优化. 具体实现可以参见我的编译器. 如果喜欢的话, 别忘了给它点一个 star.
CDCL 算法¶
在 DPLL 算法中, 我们有以下三个步骤:
- 删除永真式;
- 执行单元传播;
- 分类讨论, 递归执行.
CDCL 算法 (conflict-driven clause learning) 是对 DPLL 的优化, 可以减少每次单元传播的耗时, 也可以减少分类讨论的次数.
前件¶
DPLL 的搜索是一棵二叉树. 如果 DPLL 的当前节点无法满足, 它就会返回到当前节点的父节点.
举个例子, 假如我们已经进行了三次分类讨论, 现在正在检查这个赋值: \(\{A_1 = 1, A_2 = 0, A_3 = 1\}\). 它在执行单元传播时产生了空的子句. 这时, DPLL 会撤回对 \(A_3\) 的赋值, 然后令 \(A_3 = 0\) 再次尝试.
然而, 如果这个冲突不是 \(A_3\) 导致的呢? 比如说, 如果 \(A_1\) 的值只能是 0, 那么无论如何更改 \(A_2\) 和 \(A_3\) 都是在做无用功. 我们能否撤回到真正导致冲突的节点, 而不仅仅是上一个节点呢?
CDCL 解决了这个问题. 不过为了计算"导致冲突的节点"和"返回到的层级", 我们还需要一些定义.
我们每做出一次分类讨论, 当前所在节点在搜索树中深度就增加 1. 我们把这个深度叫做决定层级 (decision level). 换句话说, 最开始没有进行任何分类讨论时, 决定层级是 0; 当我们开始尝试 \(A_1\) 是真是假时, 决定层级是 1; 当我们尝试 \(A_2\) 时, 决定层级就变为 2, 以此类推.
在单元传播中, 可能会产生一些新的单元子句, 触发更多的单元传播. 假设传播子句 \(\omega_1\) 时, 产生了一个新的单元子句 \(\lbrace L\rbrace\), 其中文字 \(L\) 含有的变量是 \(A\). 这时, 我们把 \(\omega_1\) 称作 \(A\) 的前件 (antecedent). 直觉上来看, \(A\) 的前件就是 \(A\) 的真值得以确定的原因.
作为一个例子, 我们不妨来看看这个公式的决定层级和前件.
假设我们先给 \(x_4\) 赋值为 0, 那么 \(x_4\) 的决定层级就是 1 (有时, 我们写作 \(x_4 = 0 @ 1\)). 它没有前件. 这时, 第一个子句 \(x_1\lor \neg x_4\) 可以被删除, 但单元传播无法得到更多信息.
接下来, 我们给 \(x_1\) 赋值为 0, 那么它的决定层级是 2, 或者写作 \(x_1 = 0 @ 2\). 它也没有前件. 这可以触发第二个子句 \(\omega_2\) 的单元传播, 得到 \(x_3 = 1\). 这里的决定层级依然是 2, 所以写作 \(x_3 = 1 @ 2\); 这个决定是由 \(\omega_2\) 导致的, 所以 \(x_3\) 的前件是 \(\omega_2\).
这次传播结束后, 第三个子句会再次触发一个单元传播, 使得 \(x_2 = 1 @ 2\). 这个决定是由 \(\omega_3\) 导致的, 所以 \(x_2\) 的前件是 \(\omega_3\). 至此, 我们就找到了一个使得原公式为真的赋值, 所以原来的公式是可满足的.