> 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.

# CDCL：从冲突到学习子句

前置知识：[SAT 与 DPLL](https://shijin.space/knowledge/sat-dpll/index.md)中的部分赋值、单位传播和归结。

## 冲突为何值得保留

冲突驱动子句学习（Conflict-Driven Clause Learning，CDCL）在搜索遇到冲突时，分析哪些赋值共同导致了矛盾，并学习一个禁止该组合的子句。学习子句应是当前公式的逻辑后果；在不涉及额外公式变换的基本 CDCL 中，由原始子句和已证实的学习子句归结得到新子句，不会删除原公式的任何模型 \[[1, pp. 140–143](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

用 $F_0$ 表示原始公式，$L$ 表示新子句，则

$$
F_0\models L,\qquad F_0\equiv F_0\land L.
$$

学习的目的不是改变答案，而是让原本隐含的约束更早参与传播。

## 赋值轨迹、决策层与原因

求解器用赋值轨迹（trail）保存按发生顺序排列的赋值。每个赋值至少需要记录：变量的值、决策层，以及传播它的原因子句；决定取值的赋值标记为决策，未赋值变量没有有效决策层或原因。

根层记为 $0$。每做一次分支决策，就进入新的决策层；在该决策之后、下次决策之前产生的传播归于当前层。只有单位传播结束且没有冲突，才开始下一次决策。冲突发生时，传播可以立即停止 \[[1, pp. 135–140](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

原因子句允许反向解释赋值。若 $C=(\neg p\lor\neg q\lor r)$ 在 $p=q=1$ 时传播 $r=1$，就记录 $C$ 是 $r$ 的原因。概念上的蕴含图用 $p\to r$、$q\to r$ 表示这个依赖；两个前提必须共同成立，单条边不表示独立的逻辑蕴含。

## 一个贯穿传播、学习与回跳的例子

考虑八个变量 $a,b,c,d,e,f,u,v$ 和六个子句：

$$
\begin{aligned}
C_1&=(\neg a\lor b),& C_2&=(\neg c\lor d),\\
C_3&=(\neg d\lor\neg b\lor e),& C_4&=(\neg d\lor f),\\
C_5&=(\neg e\lor\neg f),& C_6&=(u\lor v),\\
F&=\bigwedge_{i=1}^{6}C_i.
\end{aligned}
$$

下面固定一种合法的决策和传播顺序，便于手算：

1. 第 $1$ 层决定 $a=1$，由 $C_1$ 传播 $b=1$。
2. 第 $2$ 层决定 $u=1$，$C_6$ 被满足，没有进一步传播。
3. 第 $3$ 层决定 $c=1$，由 $C_2$ 传播 $d=1$。
4. 处理 $d=1$ 时，先由 $C_3$ 传播 $e=1$，再由 $C_4$ 传播 $f=1$。
5. $C_5$ 的两个文字都为假，发生冲突。

用下标表示决策层，并在括号内写传播原因，轨迹是

$$
\bigl[a_1,\ b_1(C_1),\ u_2,\ c_3,\ d_3(C_2),\ e_3(C_3),\ f_3(C_4)\bigr].
$$

这个顺序不是唯一的。例如先处理 $e=1$ 引起的传播，也可能得到 $f=0$，继而在 $C_4$ 上发现冲突。冲突子句和推导过程依赖实际传播顺序，因此分析时必须与记录下来的轨迹一致。

### 先把冲突写成归结推导

从被违反的子句 $C_5$ 出发，按轨迹逆序消去当前层中较晚的传播变量：

$$
\begin{aligned}
R_0&=C_5=(\neg e\lor\neg f),\\
R_1&=\operatorname{Res}_{f}(R_0,C_4)
     =(\neg e\lor\neg d),\\
R_2&=\operatorname{Res}_{e}(R_1,C_3)
     =(\neg d\lor\neg b).
\end{aligned}
$$

因此可以学习

$$
L=(\neg d\lor\neg b).
$$

每一步都是可靠的归结。直观上，$b=d=1$ 会分别强制 $e=f=1$，与 $C_5$ 冲突，所以 $b$ 和 $d$ 不能同时为真。这个结论不依赖第 $2$ 层对 $u$ 的决定。

### 为什么在这里停止：1-UIP

在当前决策层的蕴含图中，从该层决策节点到冲突节点的每条路径都经过的赋值节点，称为唯一蕴含点（unique implication point，UIP）。当前层的决策节点本身也是一个 UIP；最靠近冲突的 UIP 称为 first UIP，通常写作 1-UIP \[[1, p. 143](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

本例中，从 $c=1$ 到冲突的两条分支分别经过 $d\to e$ 和 $d\to f$，都通过 $d$，所以 $d$ 是 1-UIP，$c$ 是更早的 UIP。较低层的 $b=1$ 是此时固定的上下文。

用逆序归结实现时，一直消去当前层中较晚的传播赋值，直到所得子句只含一个当前层文字。本例中 $R_0$ 含 $\neg e,\neg f$ 两个当前层文字，$R_1$ 含 $\neg e,\neg d$ 两个，而 $R_2$ 只含 $\neg d$，因此停止。这是一个可执行的停止条件，不需要显式构建整张蕴含图 \[[2, sec. 4.4](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2003MiniSat)\]。

对同一次冲突，沿这条当前层归结链继续追溯到更早的 UIP，可能增加较低层文字，并使回跳层保持不变或升高；这一结论有固定推导方式的前提。它不等于说 1-UIP 子句是所有逻辑后果中最短的子句，也不能替代额外的学习子句最小化 \[[1, pp. 143–145](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

### 回跳到哪一层

设学习子句为 $L=(\ell^*\lor\ell_1\lor\cdots\lor\ell_k)$，其中 $\ell^*$ 是唯一的当前层文字。标准断言式回跳选择其他文字的最大决策层：

$$
j=\max\{\operatorname{level}(\ell_i):1\le i\le k\}.
$$

如果没有其他文字，即学到单位子句，则取 $j=0$。撤销所有高于 $j$ 层的赋值后，其他文字仍然为假，而 $\ell^*$ 变成未赋值，因此新子句成为单位子句并传播 $\ell^*$；这称为断言性质 \[[1, pp. 143–144](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

本例中 $b$ 位于第 $1$ 层，所以从第 $3$ 层回跳到第 $1$ 层，跳过了无关的第 $2$ 层。撤销 $u,c,d,e,f$ 后，$b=1$ 仍保留，$L$ 立即传播 $d=0$，随后 $C_2$ 传播 $c=0$。这里传播的是 $d=0$，不能把这个过程简化成“翻转最近一次决策”。

继续决定 $u=1,e=0,f=0$ 并补全 $v=0$，得到一个模型：

$$
(a,b,c,d,e,f,u,v)=(1,1,0,0,0,0,1,0).
$$

逐一代入可见六个原始子句均为真。例子同时说明：当前分支发生冲突，不代表整个公式 UNSAT。

## 1-UIP 分析：逆序扫描与标记

前面的归结过程可以直接沿 trail 实现，不必先画出蕴含图。下面沿用本文的基本 CDCL 设定：根层赋值由公式本身推出，每个非根层只有一次决策，并且先传播到不动点才做下一次决策。过程仅处理当前层 $d>0$ 的冲突，根层冲突由外层循环直接判为 UNSAT \[[2, sec. 4.4](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2003MiniSat)\]。

trail 中保存的是当前为真的文字，索引从 $0$ 开始。$\operatorname{var}(q)$ 返回文字的变量，$\operatorname{level}(x)$ 返回变量的决策层，$\operatorname{reason}(p)$ 返回传播文字 $p$ 的原因子句。若 $p$ 是决策文字，就没有原因子句。

扫描过程维护四项状态：

- $S$ 保存已经标记、尚未消去的变量，用来避免在依赖汇合处重复计数。
- $B$ 收集最终子句中的较低层文字，保持它们在原因子句中的符号。
- $k$ 记录已经发现、尚未处理的当前层变量数。
- $i$ 从 trail 末端向前移动，选择最新的已标记赋值。

$R$ 仅表示本轮要扫描的子句文字：最初是冲突子句，之后是去掉被传播文字的原因子句。它不是每一步完整的归结结果；已经发现的其余依赖保存在 $S$ 和 $B$ 中。下面是算法伪代码，读取求解器的 trail、决策层和原因记录，不是可独立运行的程序。

```pseudocode
\begin{algorithm}
\caption{First-UIP Conflict Analysis}
\begin{algorithmic}
\FUNCTION{AnalyzeFirstUIP}{$C$}
    \STATE $d \gets \operatorname{level}()$
    \STATE $S \gets \varnothing$, $B \gets \varnothing$, $k \gets 0$
    \STATE $i \gets |\operatorname{trail}|-1$, $R \gets C$
    \REPEAT
        \FORALL{$q \in R$}
            \STATE $x \gets \operatorname{var}(q)$
            \IF{$\operatorname{level}(x)>0$ \AND $x\notin S$}
                \STATE $S \gets S\cup\{x\}$
                \IF{$\operatorname{level}(x)=d$}
                    \STATE $k \gets k+1$
                \ELSE
                    \STATE $B \gets B\cup\{q\}$
                \ENDIF
            \ENDIF
        \ENDFOR
        \WHILE{$\operatorname{var}(\operatorname{trail}[i])\notin S$}
            \STATE $i \gets i-1$
        \ENDWHILE
        \STATE $p \gets \operatorname{trail}[i]$, $i \gets i-1$
        \STATE $S \gets S\setminus\{\operatorname{var}(p)\}$
        \STATE $k \gets k-1$
        \IF{$k>0$}
            \STATE $R \gets \operatorname{reason}(p)\setminus\{p\}$
        \ENDIF
    \UNTIL{$k=0$}
    \STATE $\ell \gets \neg p$, $L \gets B\cup\{\ell\}$
    \STATE $j \gets \max\bigl(\{0\}\cup\{\operatorname{level}(\operatorname{var}(q)):q\in B\}\bigr)$
    \RETURN $(L,j,\ell)$
\ENDFUNCTION
\end{algorithmic}
\end{algorithm}
```

每轮扫描完 $R$ 时，$k$ 等于当前依赖中尚未处理的当前层变量数。若取出最新的赋值 $p$ 后 $k>0$，就用 $p$ 的原因展开它的前提，相当于消去当前归结式中的 $\neg p$。若取出 $p$ 后 $k=0$，说明展开它之前只剩这一个当前层变量，因此保留 $\neg p$ 并停止；此时不能再继续消去它。这就是 1-UIP 停止条件 \[[2, sec. 4.4](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2003MiniSat); [1, pp. 143–144](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

在取出 $p$ 并将 $k$ 减一之后，若 $k>0$，那么 $p$ 必有传播原因：该层决策在 trail 中早于所有本层传播，若已经退到决策文字，它后面的本层依赖就已处理完，此时必有 $k=0$。因此算法不会对一个需要继续展开的决策文字读取原因。根层变量被跳过，是因为它们的真值已由公式推出；这相当于使用根层事实做单位归结，不是任意删除子句文字。

将算法用于前面的 $C_5$ 冲突，可以逐轮核对：

1. 扫描 $C_5=\{\neg e,\neg f\}$，标记 $e,f$，得到 $k=2$。逆序取出 $f$ 后 $k=1$，下一轮扫描 $C_4\setminus\{f\}=\{\neg d\}$。
2. 新标记 $d$ 后 $k=2$。继续逆序取出 $e$，令 $k=1$，下一轮扫描 $C_3\setminus\{e\}=\{\neg d,\neg b\}$。
3. $d$ 已标记，不重复增加 $k$；$b$ 在较低层，将 $\neg b$ 放入 $B$。取出 $d$ 后 $k=0$，停止并返回 $L=\{\neg d,\neg b\}$、$j=1$、$\ell=\neg d$。

这里的符号方向很重要：trail 中记录 $d$ 为真，学习子句中保留的是 $\neg d$。$S$ 在每次调用时重新初始化；工程实现通常复用标记数组，并显式清理本次使用过的标记。标记和计数减少了重复检查，但不改变前面逐步归结得到的结论。

## 学习子句最小化：什么时候可以删除文字

1-UIP 规定在当前层的归结何时停止，并不保证所得子句已经没有冗余文字。较低层赋值之间仍可能存在可利用的原因关系。删除一个文字会加强子句，因此必须证明加强后的子句仍是公式的逻辑后果；局部最小化和递归最小化就是两种利用原因关系的检查方法 \[[1, pp. 144–146](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

### 局部最小化：一次归结就能删去一个文字

另外考虑一个独立于前面 $F$ 的小公式：

$$
\begin{aligned}
D_1&=(\neg b\lor d),&
D_2&=(\neg d\lor\neg c\lor e),\\
D_3&=(\neg b\lor\neg c\lor f),&
D_4&=(\neg e\lor\neg f),\\
G&=\bigwedge_{i=1}^{4}D_i.
\end{aligned}
$$

第 $1$ 层决定 $b=1$，由 $D_1$ 传播 $d=1$；第 $2$ 层决定 $c=1$，先由 $D_2$ 传播 $e=1$，再由 $D_3$ 传播 $f=1$，在 $D_4$ 上发现冲突。按照这条轨迹分析：

$$
\begin{aligned}
R_0&=(\neg e\lor\neg f),\\
R_1&=\operatorname{Res}_{f}(R_0,D_3)
     =(\neg e\lor\neg b\lor\neg c),\\
K&=\operatorname{Res}_{e}(R_1,D_2)
   =(\neg d\lor\neg b\lor\neg c).
\end{aligned}
$$

$K$ 中只有 $\neg c$ 属于当前层，因此已经满足 1-UIP 的停止条件。但 $d$ 的原因 $D_1=(\neg b\lor d)$ 仍可继续利用：

$$
K_{\min}=\operatorname{Res}_{d}(K,D_1)
       =(\neg b\lor\neg c).
$$

这次归结去掉 $\neg d$，加入的 $\neg b$ 原本就在 $K$ 中，所以净效果是删除一个文字。它没有改变结论的可靠性，也保留了断言文字 $\neg c$；回跳到第 $1$ 层后，$b=1$ 使 $K_{\min}$ 立即传播 $c=0$。

更一般地，若 $K=\neg p\lor B$，$p$ 的原因是 $p\lor A$，并且 $A$ 的全部文字已包含在 $B$ 中，那么归结得到 $A\lor B=B$，即可删除 $\neg p$。这是一项足够条件，需要检查原因中的其余文字，而不是只检查 $p$ 是否来自传播 \[[1, p. 145](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

### 递归最小化：沿多步原因链证明冗余

把上述 $G$ 中的 $D_1$ 换成两个子句，其余子句不变：

$$
E_1=(\neg b\lor s),\qquad E_2=(\neg s\lor d).
$$

现在第 $1$ 层的传播链是 $b\to s\to d$，第 $2$ 层的冲突分析仍得到 $K=(\neg d\lor\neg b\lor\neg c)$。只查看 $d$ 的直接原因 $E_2$ 时，会遇到不在 $K$ 中的 $\neg s$，因而上述局部检查不能直接删掉 $\neg d$。继续追溯 $s$ 的原因，则有

$$
\begin{aligned}
K'&=\operatorname{Res}_{d}(K,E_2)
   =(\neg s\lor\neg b\lor\neg c),\\
K_{\min}&=\operatorname{Res}_{s}(K',E_1)
         =(\neg b\lor\neg c).
\end{aligned}
$$

递归检查可以把其他保留文字所对应的赋值作为已知边界，沿候选文字的原因向前追溯。若所有依赖最终都落到这个边界或已经证实的根层事实，就能证明候选文字冗余；若遇到边界之外、没有原因可继续展开的决策赋值，这条检查路径就不能完成删除证明。检查失败只表示该方法尚未证明可删，不意味着不存在其他证明 \[[1, pp. 145–146](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

### 反例：更短不等于仍然正确

回到最初的四子句公式 $G$。已经证明 $G\models(\neg b\lor\neg c)$，但不能再任意删除其中一个文字：

- 若删去 $\neg b$，得到单位子句 $(\neg c)$。赋值 $(b,c,d,e,f)=(0,1,0,0,0)$ 满足全部四个原始子句，却使 $\neg c$ 为假。
- 若删去 $\neg c$，得到单位子句 $(\neg b)$。赋值 $(b,c,d,e,f)=(1,0,1,0,0)$ 同样满足 $G$，却使 $\neg b$ 为假。

因此，这两个进一步缩短的子句都会排除原公式的合法模型。最小化算法应保留 1-UIP 的断言文字，对其他文字做有依据的删减，并按最终子句重新计算回跳层。这里的“最小化”通常是依据特定规则消除冗余，不承诺求得所有逻辑后果中长度最短的子句。

## CDCL 的基本循环

下面用伪代码表示 CDCL 的基本循环。AnalyzeFirstUIP 使用前文的逆序扫描过程，返回初步的 1-UIP 子句，本循环未启用进一步的学习子句最小化。其余辅助过程共同操作当前求解器的状态，具体实现仍未展开，伪代码不能独立运行。返回满足赋值表示 SAT，返回 $\mathrm{UNSAT}$ 表示无解。$C$ 是传播返回的冲突子句；$\mathrm{None}$ 表示没有冲突，与空子句不同。冲突分析显式给出学习子句 $L$、回跳层 $j$ 和断言文字 $\ell$。

```pseudocode
\begin{algorithm}
\caption{CDCL}
\begin{algorithmic}
\INPUT CNF formula $F$
\OUTPUT A model of $F$, or \textsc{Unsat}
\STATE \CALL{Initialize}{$F$}
\WHILE{\TRUE}
    \STATE $C \gets$ \CALL{Propagate}{}
    \IF{$C \ne \mathrm{None}$}
        \IF{$\operatorname{level}() = 0$}
            \RETURN \textsc{Unsat}
        \ENDIF
        \STATE $(L, j, \ell) \gets$ \CALL{AnalyzeFirstUIP}{$C$}
        \STATE \CALL{Backtrack}{$j$}
        \STATE \CALL{AddClause}{$L$}
        \STATE \CALL{Enqueue}{$\ell, L$}
    \ELIF{\CALL{AllAssigned}{}}
        \RETURN \CALL{Assignment}{}
    \ELSE
        \STATE \CALL{Decide}{\CALL{ChooseLiteral}{}}
    \ENDIF
\ENDWHILE
\end{algorithmic}
\end{algorithm}
```

Initialize 初始化公式、赋值轨迹和根层传播队列；Propagate 没有冲突时返回 $\mathrm{None}$，有冲突时返回冲突子句，空子句也属于冲突。Enqueue 的第二个参数记录原因子句；Decide 合并了新建决策层与记录无原因的决策赋值。

该伪代码强调“传播—冲突分析—回跳—加入学习子句—断言传播”的顺序，省略重启、子句删除和公式预处理。根层冲突之所以足以回答 UNSAT，是因为此时矛盾不再依赖未撤销的分支假设；若需要让外部检查器验证结论，还要输出相应证明轨迹 \[[1, secs. 4.2, 4.4.1.4](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

## 双监视文字如何减少传播工作

单位传播频繁发生。若每赋值一个变量都重新统计所有相关子句的状态，维护成本可能很高。双监视文字为长度至少为 $2$ 的子句维护两个监视位置，只在监视文字变假时检查是否需要移动监视或触发传播；单位子句单独处理 \[[1, pp. 149–151](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

设 $w$ 刚刚变假，另一个监视文字为 $q$：

1. 若 $q$ 为真，子句已经满足，可以暂不处理。
2. 否则在非监视文字中寻找一个**非假文字**，即真或未赋值的文字；找到就用它替换 $w$。
3. 若找不到替代项，且 $q$ 未赋值，子句成为单位子句，传播 $q$ 为真。
4. 若找不到替代项，且 $q$ 也为假，子句冲突。

因此，“找不到替代项”不总是传播：还必须检查另一个监视文字。监视位置也不要求永远指向未赋值文字。

### 赋值立即生效，传播队列随后处理

trail 同时承担赋值记录和传播队列的作用。把文字 $p$ 入队时，先把它设为真、记录当前决策层与原因，再将它追加到 trail。此时所有子句都能查询到这个真值，但由 $p$ 引起的后续传播尚未处理。

用从 $0$ 开始的指针 $h$ 标记下一个待处理位置。正常无冲突地推进时，$\operatorname{trail}[0:h]$ 中的事件已经处理，$\operatorname{trail}[h:]$ 中的事件仍在等待。读出 $p=\operatorname{trail}[h]$ 后递增 $h$，再检查那些监视了 $\neg p$ 的子句；新传播的文字继续追加到同一条 trail。无冲突且 $h=|\operatorname{trail}|$ 时，才达到传播不动点 \[[2, secs. 3, 4.3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2003MiniSat)\]。

本文记 $W[\ell]$ 为监视文字 $\ell$ 的子句列表，因此处理 $p=1$ 时访问 $W[\neg p]$。MiniSat 将监视条目存放在互补文字的索引下，源码相应访问 `watches[p]`；两者只是索引约定不同，不能混用 \[[3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2013MiniSatCore)\]。

### 将四种情况放进传播循环

下面的伪代码假定初始化已经删除重复文字和重言式，在开始传播前为长度至少为 $2$ 的子句建立了两个不同的监视位置，并将单位子句入队。空子句或互相矛盾的初始单位赋值由初始化过程报告冲突。

```pseudocode
\begin{algorithm}
\caption{Propagation with Two Watched Literals}
\begin{algorithmic}
\FUNCTION{Propagate}{}
    \WHILE{$h<|\operatorname{trail}|$}
        \STATE $p\gets\operatorname{trail}[h]$, $h\gets h+1$
        \FORALL{$C\in\operatorname{Snapshot}(W[\neg p])$}
            \STATE $q\gets$ \CALL{OtherWatch}{$C,\neg p$}
            \IF{$\operatorname{value}(q)\ne 1$}
                \STATE $r\gets$ \CALL{FindNonFalse}{$C\setminus\{\neg p,q\}$}
                \IF{$r\ne\mathrm{None}$}
                    \STATE \CALL{MoveWatch}{$C,\neg p,r$}
                \ELIF{$\operatorname{value}(q)=0$}
                    \RETURN $C$
                \ELSE
                    \STATE \CALL{Enqueue}{$q,C$}
                \ENDIF
            \ENDIF
        \ENDFOR
    \ENDWHILE
    \RETURN $\mathrm{None}$
\ENDFUNCTION
\end{algorithmic}
\end{algorithm}
```

$\operatorname{value}(\ell)$ 返回 $1$、$0$ 或未赋值状态 $\mathrm{U}$，并考虑文字的正负号。FindNonFalse 返回一个值不为 $0$ 的候选文字；不存在时返回 $\mathrm{None}$。MoveWatch 同时修改子句中的监视位置，把对应条目从旧列表移到新列表。走到 Enqueue 时，另一个监视文字 $q$ 必为未赋值状态，因此可以将 $q$ 置真，并把 $C$ 记录为原因。

Snapshot 表示遍历本轮待处理条目的快照，使移动监视时不会漏掉尚未访问的条目。这是便于说明语义的写法；实际实现可用读写指针原地压缩列表。冲突提前返回时，也必须保留未处理条目的监视关系。伪代码读取共享的 trail、指针和监视列表，辅助数据结构未展开，不能独立运行 \[[3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2013MiniSatCore)\]。

### 沿原来的冲突例子跟踪队列

沿用前面的六子句公式。假设 $C_3=(\neg d\lor\neg b\lor e)$ 最初监视 $\neg d,\neg b$。第 $1$ 层处理 $b=1$ 时，$\neg b$ 变假；$e$ 尚未赋值，可以把这个监视位置移到 $e$，因此随后 $C_3$ 监视的是 $\neg d,e$。

第 $2$ 层传播完成后，$\operatorname{trail}=[a,b,u]$，$h=3$。第 $3$ 层决定 $c=1$ 后，可以按下面的合法顺序处理：

1. 把 $c$ 追加到 trail。处理 $c$ 时，$h$ 从 $3$ 变为 $4$，由 $C_2$ 将 $d$ 置真并入队。
2. 处理 $d$ 时，$h$ 变为 $5$。先检查 $C_3$：另一个监视文字 $e$ 未赋值，剩余候选 $\neg b$ 为假，所以传播 $e$。再检查 $C_4$，传播 $f$。此时 trail 已是 $[a,b,u,c,d,e,f]$。
3. 处理 $e$ 时，$h$ 变为 $6$。在 $C_5=(\neg e\lor\neg f)$ 中，另一个监视文字 $\neg f$ 已经为假，因而返回冲突。虽然 $f$ 对应的队列事件尚未处理，$f=1$ 的赋值已经生效。

这说明冲突可以发生在队列尚未排空时。返回冲突后，当前条目的扫描也可能尚未完成，不能据此认为传播已达到不动点；外层循环需要先分析冲突并回跳。

### 回跳时重置队列，但不恢复历史监视位置

标准回跳截去 trail 中高于目标决策层的后缀，撤销相应赋值和原因记录，并把 $h$ 设为保留前缀的长度。这里的前提仍是每次新决策前已经传播到不动点，所以保留下来的较低层前缀已经处理完 \[[3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2013MiniSatCore)\]。

本例回跳到第 $1$ 层后保留 $[a,b]$，令 $h=2$。加入学习子句 $(\neg d\lor\neg b)$，再将断言文字 $\neg d$ 入队，得到 $[a,b,\neg d]$。下一次 Propagate 从索引 $2$ 开始，由 $C_2$ 继续传播 $\neg c$。

新加入的非单位学习子句还需要正确建立监视。常见做法是监视断言文字，以及其余文字中决策层最高的一项，使后续回溯仍满足监视方案所依赖的赋值顺序；单位学习子句则单独在根层入队。MiniSat 的冲突分析会把这两项安排在学习子句的前两个位置，随后由子句入库过程建立监视 \[[3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2013MiniSatCore)\]。

在标准 trail 后缀回溯和正确维护监视列表的条件下，不需要恢复监视位置的历史状态。撤销赋值不会产生新的“监视文字变假”事件；以后再次赋值时，仍由当前监视列表触发检查。这里保留的是监视结构，变量赋值、原因和队列边界仍必须按回跳结果更新 \[[2, secs. 3, 4.3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2003MiniSat)\]。

### 阻塞文字：在读取子句前确认它已经满足

监视条目还可以缓存一个属于该子句的文字，称为阻塞文字（blocking literal）。若查询到它当前为真，就能确认子句已经满足，直接跳过这一条目，从而减少对子句存储的访问。它为假或未赋值时不能下结论，仍需读取子句并按前面的规则处理。

缓存的文字不必始终是当前另一个监视文字，但必须仍属于该子句；若子句被改写，相关缓存也要得到正确维护。上面的教学伪代码省略了这一优化，MiniSat 的 `propagate` 则在读取子句之前先检查 `blocker` \[[3](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2013MiniSatCore)\]。

传播过程在当前子句数据库上维护赋值；[预处理与内处理](https://shijin.space/knowledge/sat-preprocessing/index.md)还会改变子句或变量表示，需要同时说明变换保持的语义和模型恢复方法。

## 分支、重启与子句管理

这些机制影响搜索效率，但需要与前面的正确性依据分开理解。完整的更新算例、重启规则与比较方法见 [CDCL 搜索策略](https://shijin.space/knowledge/sat-search-strategies/index.md)。

**分支启发式。** VSIDS 一类方法提高近期参与冲突分析的变量活跃度，并通过衰减降低旧事件的权重；分支时优先选择活跃的未赋值变量。变量选择与取值极性是两个问题，相位保存可记住先前使用的取值。不同实现的加分对象和衰减方式可能不同 \[[1, pp. 148–149](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

**搜索重启。** 重启撤销非根层的搜索赋值，通常保留学习子句和部分启发式状态，再从根层继续。它不意味着忘掉已经证明的结论。任意的重启、学习与删除组合不自动保证终止；应结合保留足够进展信息或允许足够长搜索区间等条件讨论完备性 \[[4, sec. 3.6.4.5](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-DarwichePipatsrisawat2021Complete); [1, p. 148](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

**LBD 与删除策略。** 在记录时刻 $\tau$，子句 $C$ 的文字分布在多少个不同决策层上，其文字块距离（literal block distance，LBD）就是多少：

$$
\operatorname{LBD}_{\tau}(C)
=\left|\{\operatorname{level}_{\tau}(\ell):\ell\in C\}\right|.
$$

本例学到 $L=(\neg d\lor\neg b)$ 时，两个文字分别在第 $3$、第 $1$ 层，因此记录的 LBD 为 $2$。LBD 与计算时的轨迹有关，不是子句语法固有的常数。低 LBD 常用于优先保留子句，但它是质量启发式，不能保证每个低 LBD 子句都更有用 \[[1, pp. 148–149](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL)\]。

删除已被原公式蕴含的学习子句不会改变原公式的模型集合，但实现还须保留有效的原因引用和必要的进展条件。较少的子句降低内存和传播开销，也可能失去未来可复用的推理；这是需要实验评估的取舍 \[[2, sec. 4.7](https://shijin.space/knowledge/sat-cdcl/index.md#ref-sat-cdcl-EenSorensson2003MiniSat)\]。

## 阅读实现时检查什么

沿同一个例子跟踪求解器时，可以依次检查：

- 每个传播文字是否有一个在传播时确实为单位的原因子句。
- 冲突分析是否得到原公式蕴含的子句，并在预期位置停止。
- 回跳后学习子句是否成为单位子句，断言文字是否被加入传播队列。
- 监视列表、传播队列位置和原因引用是否与撤销后的轨迹一致。
- SAT 结果能否满足全部原始子句，UNSAT 结果是否有可独立检查的证明。

在这个基础上，再讨论分支策略、子句质量或并行共享的改进，才能区分算法正确性、搜索效果与实现成本。

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

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

<div id="ref-sat-cdcl-MarquesSilvaLynceMalik2021CDCL" class="csl-entry">

1\. Joao Marques-Silva, Ines Lynce, and Sharad Malik. *Conflict-driven clause learning SAT solvers*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200987).

</div>

<div id="ref-sat-cdcl-EenSorensson2003MiniSat" class="csl-entry">

2\. Niklas Eén and Niklas Sörensson. *An extensible SAT-solver*. Theory and applications of satisfiability testing. 2004. [DOI](https://doi.org/10.1007/978-3-540-24605-3_37).

</div>

<div id="ref-sat-cdcl-EenSorensson2013MiniSatCore" class="csl-entry">

3\. Niklas Eén and Niklas Sörensson. *MiniSat: Core solver implementation*. 2013. [原文](https://github.com/niklasso/minisat/blob/37dc6c67e2af26379d88ce349eb9c4c6160e8543/minisat/core/Solver.cc).

</div>

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

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

</div>

</div>

## 配套演示

- [SAT 求解：从 DPLL 到 CDCL · 16:9](https://shijin.space/slides/sat-cdcl/index.html)
- [SAT 求解：从 DPLL 到 CDCL · 4:3](https://shijin.space/slides/sat-cdcl/index-4-3.html)