单元传播

一个单位子句像只剩一个未封闭出口的约束。选择这个出口不是启发式猜测，而是任何未来模型都必须接受的后果。传播新文字后，其他子句可能再失去倒数第二个出口，于是形成连锁反应。算法的力量来自把一次决定的后果追到不动点，使搜索只在真正尚有自由度的位置分支。

reason clause 给这条链装上可逆的因果标签。若只保存“$b$ 被设为真”而不保存是哪条子句强制它，求解器仍可继续搜索，却无法可靠解释后来为何冲突，也不能从冲突中推导安全的新子句。逻辑后果与工程记录在这里恰好对齐。

考虑

若队列先处理 $(a)$，便追加 $a$；第二子句只剩 $b$，以它为 reason 追加 $b$；随后依次追加 $c,d$。最后子句 $(\mathrm{\neg }d)$ 被 $d$ 证伪，成为 conflict clause。反向查看 reason 可得到清楚的蕴含链

而输入又要求 $\mathrm{\neg }d$。若队列先处理 $(\mathrm{\neg }d)$，传播方向相反，最终仍会碰到 $(a)$ 冲突；结论不依赖最初选择哪个单位子句。

单元传播并不完备。公式

在空 trail 下没有单位子句，传播立即到达不动点，但分别检查 $x=0$ 与 $x=1$ 都会产生矛盾。因而“没有新传播”只表示局部规则暂时沉默，不表示已有模型；同样，传播次数多也不能作为实例更难的稳定尺度。

不完备性也不只来自 UNSAT。公式 $(x\vee y)\wedge (x\vee \mathrm{\neg }y)$ 在空 trail 下没有单位子句，单位闭包为空，却在语义上蕴涵 $x$：若 $x=0$，两个子句分别强制 $y$ 与 $\mathrm{\neg }y$。所以“所有传播文字都是逻辑后果”是可靠性结论，反方向“所有逻辑后果都会传播”并不成立。

单位传播是 DPLL 与 CDCL 每个决策层的固定点计算。一个分支是否能尽早失败，很大程度上取决于编码在部分赋值下能暴露多少单位后果；这也是 SAT 编码会比较 propagation completeness，而不只比较子句数量的原因。

朴素实现会在每次赋值后扫描全部子句。双监视文字公理库双监视文字Two-watched-literals scheme · Two literal watching · Watched literals每个非单位子句监视两个文字，只在监视文字变假时扫描并维护单位传播状态。用每个子句的两个观察点实现同一推理接口，只访问监视刚变假的文字的子句；它改变索引与扫描成本，不改变哪些单位后果有效。Horn 公式等受限类别上，反复单位传播还能承担完整判定的核心，但这个结论依赖语法限制，不能推广到一般 CNF。