> For AI agents: the complete documentation index is available at https://shijin.space/llms.txt, the full documentation bundle is available at https://shijin.space/llms-full.txt.

# SAT 与 DPLL

前置知识：布尔运算、集合和递归。阅读路线见[专题概览](https://shijin.space/knowledge/sat/index.md)。

## 文字、子句和合取范式

布尔变量取值于 $\{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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

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

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

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

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

二者分别是搜索成功和冲突的基本判据 \[[1, pp. 101–102](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。含有 $x$ 和 $\neg x$ 的子句恒真，可以直接删除；重复文字可以合并。

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

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

考虑

$$
\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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-Prestwich2021CNF)\]。

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

## 部分赋值与公式化简

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

令文字 $\ell$ 为真，公式限制 $F|_\ell$ 通过两步得到：删除包含 $\ell$ 的子句，并从其余子句中删除 $\neg\ell$。前一步删除已经满足的约束，后一步删除已经为假的选择 \[[1, sec. 3.2.2](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

例如

$$
\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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

考虑

$$
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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

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

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

```pseudocode
\begin{algorithm}
\caption{DPLL}
\begin{algorithmic}
\FUNCTION{DPLL}{$F, \alpha$}
    \STATE $(F, \alpha) \gets$ \CALL{PropagateToFixpoint}{$F, \alpha$}
    \IF{$\varnothing \in F$}
        \RETURN \textsc{Unsat}
    \ENDIF
    \IF{$F = \varnothing$}
        \RETURN $\alpha$
    \ENDIF
    \STATE $x \gets$ \CALL{ChooseVariable}{$F$}
    \FORALL{$\ell \in \{x, \neg x\}$}
        \STATE $F' \gets$ \CALL{Condition}{$F, \ell$}
        \STATE $\alpha' \gets$ \CALL{Extend}{$\alpha, \ell$}
        \STATE $m \gets$ \CALL{DPLL}{$F', \alpha'$}
        \IF{$m \ne \mathrm{UNSAT}$}
            \RETURN $m$
        \ENDIF
    \ENDFOR
    \RETURN \textsc{Unsat}
\ENDFUNCTION
\end{algorithmic}
\end{algorithm}
```

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

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

其正确性来自三个事实：单位传播只做当前子问题中必需的赋值；$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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

对不可满足的 CNF，完整的命题归结可以推导出空子句，称为反驳完备性；单位归结的限制使它没有这个一般保证 \[[1, pp. 102–103](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

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

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

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

$$
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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

**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](https://shijin.space/knowledge/sat-dpll/index.md#ref-sat-dpll-DarwichePipatsrisawat2021Complete)\]。

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

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

## 从回溯走向学习

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

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

## 参考文献 {#references-sat-dpll}

<div id="refs-sat-dpll" class="references csl-bib-body">

<div id="ref-sat-dpll-DarwichePipatsrisawat2021Complete" class="csl-entry">

1\. Adnan Darwiche and Knot Pipatsrisawat. *Complete algorithms*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200986).

</div>

<div id="ref-sat-dpll-Prestwich2021CNF" class="csl-entry">

2\. Steven Prestwich. *CNF encodings*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200985).

</div>

</div>