SAT 与 DPLL#

前置知识：布尔运算、集合和递归。阅读路线见专题概览。

#文字、子句和合取范式

布尔变量取值于 $\{0,1\}$，分别表示假和真。变量 $x$ 及其否定 $\neg x$ 称为文字（literal）；若 $\ell$ 是一个文字，$\neg\ell$ 表示其互补文字，因而 $\neg(\neg x)=x$。

子句（clause）是若干文字的析取，合取范式（conjunctive normal form，CNF）是若干子句的合取。例如

$$F=(a\lor b)\land(\neg a\lor c)\land(\neg b\lor c).$$

赋值 $a=1,b=0,c=1$ 使每个子句都为真，因此是 $F$ 的一个满足赋值，也称模型。SAT 判断模型是否存在；它不要求找出所有模型 [1, sec. 3.2]。

为便于描述算法，也把子句写成文字集合，把 CNF 写成子句集合：

$$F=\{\{a,b\},\{\neg a,c\},\{\neg b,c\}\}.$$

这个记法有两个容易混淆的边界情况：

• 空公式 $F=\varnothing$ 没有需要满足的子句，值为真。
• 空子句 $\varnothing\in F$ 没有能使该子句为真的文字，因此整个公式不可满足。

二者分别是搜索成功和冲突的基本判据 [1, pp. 101–102]。含有 $x$ 和 $\neg x$ 的子句恒真，可以直接删除；重复文字可以合并。

#从命题公式到 CNF：Tseitin 编码

实际问题得到的命题公式未必已经是 CNF。直接使用分配律可以得到逻辑等价的 CNF，但反复展开可能使公式规模指数增长。Tseitin 编码给子公式引入辅助变量，用局部约束描述其含义，再要求代表整个公式的变量为真。对于由固定元数的常见布尔运算构成的公式，辅助变量数和编码规模均可保持为输入规模的线性量级 [2, secs. 2.2.1–2.2.2]。

考虑

$$\varphi=(a\land b)\lor\neg c.$$

引入 $z$ 表示 $a\land b$，引入 $t$ 表示整个公式：

$$z\leftrightarrow(a\land b),\qquad t\leftrightarrow(z\lor\neg c).$$

每个双向定义都可以拆成 CNF。对第一个定义，$z=1$ 要求 $a=b=1$，反过来 $a=b=1$ 要求 $z=1$；第二个定义也同时保留两个方向。因此得到

$$\begin{aligned} D_z&=(\neg z\lor a)\land(\neg z\lor b) \land(z\lor\neg a\lor\neg b),\\ D_t&=(\neg t\lor z\lor\neg c) \land(t\lor\neg z)\land(t\lor c),\\ T&=D_z\land D_t\land(t). \end{aligned}$$

最后的单位子句 $(t)$ 不可省略。$D_z\land D_t$ 只规定辅助变量应如何取值，没有要求原公式成立。例如 $a=b=0,c=1,z=t=0$ 满足两个定义，却使 $\varphi$ 为假；加入 $(t)$ 才会排除这个赋值。

这里需要区分三个层次：

• 逻辑等价要求对相关变量的每个赋值，两边的真假相同。
• 等可满足只要求两边同时有解或同时无解，不自动给出模型之间的对应关系。
• 模型投影与扩展说明怎样在两个公式的模型之间转换。本例中，$T$ 的任意模型限制到 $a,b,c$ 后都满足 $\varphi$；反过来，$\varphi$ 的任意模型都能按子公式的值补出 $z,t$，得到 $T$ 的模型。

因而，本例不仅等可满足，还满足逐个原变量赋值的对应关系：

$$\varphi(a,b,c)\equiv\exists z\,\exists t\;T(a,b,c,z,t).$$

不能直接把它写成扩展变量集合上的 $\varphi\equiv T$。例如 $a=b=c=1$ 满足 $\varphi$，但任意补一个 $z=0$ 就会违反 $D_z$；正确的扩展应取 $z=t=1$。引入辅助变量后，SAT 求解器处理的是 $T$，应用端需要的是投影回原变量的模型 [2, sec. 2.2.2]。

线性规模编码避免了转换阶段的无谓膨胀，不保证编码后的实例容易求解；编码产生的传播能力和搜索结构仍会影响实际性能。

#部分赋值与公式化简

部分赋值只给一部分变量指定值。未赋值是求解器中的状态，不是布尔逻辑的第三种真值。一个尚未满足的子句可能仍有未赋值文字，因此尚未满足不等于已经冲突。

令文字 $\ell$ 为真，公式限制 $F|_\ell$ 通过两步得到：删除包含 $\ell$ 的子句，并从其余子句中删除 $\neg\ell$。前一步删除已经满足的约束，后一步删除已经为假的选择 [1, sec. 3.2.2]。

例如

$$\begin{aligned} F&=\{\{a,b\},\{\neg a,c\},\{\neg b,c\}\},\\ F|_a&=\{\{c\},\{\neg b,c\}\}. \end{aligned}$$

这里的剩余公式描述的是固定 $a=1$ 之后的子问题。它与任意赋值下的原公式并不等价；应把已经固定的赋值与剩余公式一起理解。

#单位传播：先完成被迫的赋值

如果一个子句中所有文字都为假，只剩一个未赋值文字 $\ell$，那么任何扩展当前部分赋值的模型都必须令 $\ell$ 为真。这就是单位传播（unit propagation，也常称 BCP）。传播得到的新赋值又可能使其他子句变成单位子句，因此需要反复执行，直到没有可传播的文字或出现冲突 [1, sec. 3.5.2]。

考虑

$$F=(a)\land(\neg a\lor b)\land(\neg b\lor c)\land(\neg c).$$

按照从左到右的一种传播顺序，单位子句 $(a)$ 强制 $a=1$，随后依次强制 $b=1$ 和 $c=1$；此时 $(\neg c)$ 为假，检测到冲突。选择另一种传播顺序也会检测到冲突，但最先返回的冲突子句可能不同。

传播结束而没有冲突，不能据此回答 SAT。 例如

$$G=(x\lor y)\land(x\lor\neg y) \land(\neg x\lor y)\land(\neg x\lor\neg y)$$

没有单位子句，但不可满足：$x=1$ 后，后两个子句分别要求 $y=1$ 和 $y=0$；$x=0$ 后，前两个子句给出同样的矛盾。单位传播是高效但不完备的推理过程，需要与搜索或更强推理结合 [1, pp. 103, 115–116]。

#DPLL：传播之后划分搜索空间

DPLL 在当前赋值下先做单位传播；若既没有冲突，也没有满足全部子句，就选择一个未赋值变量 $x$，分别搜索 $x=1$ 和 $x=0$。下面用伪代码表示这一过程，初始调用为 $\operatorname{DPLL}(F,\varnothing)$：返回部分满足赋值表示 SAT，返回 $\mathrm{UNSAT}$ 表示无解。辅助过程的具体实现未展开，伪代码不能独立运行。

这里将 $F$ 视为子句集合：$\varnothing\in F$ 表示出现空子句，$F=\varnothing$ 表示所有子句均已满足。PropagateToFixpoint 做单位传播直到不再产生新赋值或发现冲突；ChooseVariable 选择剩余公式中的未赋值变量。Condition 将文字 $\ell$ 置真并返回该分支的剩余公式，Extend 返回扩展后的赋值副本，后续传播也只更新当前分支。空赋值也可能满足空公式，因此用 $m\ne\mathrm{UNSAT}$ 判断是否找到模型。

每个分支拥有自己的剩余公式和赋值，失败后撤销该分支的决定与传播。若全部子句已经满足，尚未赋值的变量可以任意补全。纯文字消除可以作为额外化简，但不是这个核心过程所必需的 [1, sec. 3.5]。

其正确性来自三个事实：单位传播只做当前子问题中必需的赋值；$x=1$ 与 $x=0$ 覆盖所有可能模型；每次分支都固定一个新变量，所以有限变量上的搜索树有限。不设资源限制、完整处理两个分支时，该过程会终止并给出正确结论。完备性并不提供多项式时间保证。

#归结：把两个约束合成一个逻辑后果

若两个子句分别包含 $x$ 和 $\neg x$，可对 $x$ 做归结（resolution）：

$$\frac{A\lor x\qquad B\lor\neg x}{A\lor B}.$$

若 $A$ 与 $B$ 都为假，两个前提就分别要求 $x=1$ 和 $x=0$，不可能同时满足，因此归结式是前提的逻辑后果。这里 $A,B$ 表示不包含被归结变量的剩余文字析取。

加入归结式保留原公式的所有模型；它不同于直接删除两个前提。DP 变量消除需要考虑涉及某变量的正负子句对，加入相应归结式后再删除包含该变量的子句，其结果对应对该变量做存在量化 [1, secs. 3.2.1, 3.3.1]。

对不可满足的 CNF，完整的命题归结可以推导出空子句，称为反驳完备性；单位归结的限制使它没有这个一般保证 [1, pp. 102–103]。

#DP 与 DPLL：消去变量，还是保留分支

归结可以用于两种不同的工作：加入一个已经隐含的约束，或者在保留可满足性的前提下消去变量。DP（Davis–Putnam）采用后一条路线；DPLL（Davis–Putnam–Logemann–Loveland）则通过分支搜索处理变量。两者都能用于 SAT 判定，但维护的中间对象不同 [1, secs. 3.3.1, 3.5]。

用一个小公式比较这两种操作：

$$F=(x\lor a)\land(\neg x\lor b).$$

DP 消去 $x$。 对两个子句归结，得到 $(a\lor b)$；加入归结式后，再删除所有含 $x$ 或 $\neg x$ 的子句，剩下

$$G=(a\lor b),\qquad G\equiv\exists x\;F.$$

这个等价关系的含义是：对 $a,b$ 的任意赋值，$G$ 成立，当且仅当能够选一个 $x$ 使 $F$ 成立。若 $a=0,b=1$，可以取 $x=1$；若 $a=1,b=0$，应取 $x=0$；若 $a=b=1$，两种取值都可以；若 $a=b=0$，不存在可行的 $x$ [1, pp. 104–105]。

DPLL 对 $x$ 分支。 固定 $x$ 后分别得到

$$F|_x=(b),\qquad F|_{\neg x}=(a).$$

第一条分支用单位传播令 $b=1$，第二条分支用单位传播令 $a=1$。它们合起来覆盖所有原公式模型；进行 SAT 判定时，一条分支找到模型即可停止，只有要回答 UNSAT 时才必须排除所有尚未排除的分支。在剩余变量上，两条分支的析取满足

$$\exists x\;F\equiv F|_x\lor F|_{\neg x}\equiv b\lor a.$$

DP 将这个存在性条件直接保存在一个消去 $x$ 的公式中；DPLL 保留分支取值，在各分支中继续化简和搜索。DP 的代价在于生成归结式：若 $x$ 正向出现于 $m$ 个子句、负向出现于 $n$ 个子句，消元时至多要考察 $mn$ 对前提，连续消元可能导致中间公式膨胀。DPLL 避免预先生成全部这些归结式，但搜索树同样可能指数增长，不能仅凭采用分支就获得多项式时间保证 [1, secs. 3.3.1, 3.5]。

加入归结式与消元后的模型含义不同。 $F\land(a\lor b)$ 与 $F$ 逻辑等价；消元结果 $G$ 却只约束 $a,b$。例如 $a=1,b=0$ 满足 $G$，若随意补成 $x=1$，第二个原始子句就为假；恢复原问题的模型必须选一个可行的 $x$。

CDCL 在搜索过程中按冲突需要生成学习子句。在本文不含额外公式变换的基本流程中，它将逻辑后果加入当前公式，并不因此删除产生这些结论的原始约束。这是搜索与归结协作的方式，后面的冲突分析将给出具体推导。

#从回溯走向学习

DPLL 可以证明一个分支失败，却未必把失败原因保存为一个可在别处使用的约束。若多个分支由于同一组相关赋值而冲突，简单搜索可能重复发现同一个问题。

CDCL保留搜索框架，同时记录传播原因，在冲突时通过归结导出学习子句。新子句排除造成冲突的赋值组合，并指导回跳后应传播什么；这把当前分支的失败转换成后续搜索可以复用的推理结果 [1, secs. 3.6.2–3.6.4]。

#参考文献