CNF 可满足性问题

CNF 把一个布尔任务写成“全部约束都要通过”的清单，而每条约束又允许若干文字任选其一为真。部分赋值不是残缺模型，而是一张不断收紧的工作表：一个真文字足以关闭整条子句；一个假文字只删除一个出口；直到最后一个出口也被关闭才产生冲突。单位子句恰处在二者之间——只剩一个出口，因此它把下一步赋值逻辑地强制出来。

这种局部状态使大型公式能够增量处理。求解器无须在每次赋值后重新计算整份公式，只需访问可能因该赋值而改变状态的子句。局部处理并没有改变全局目标：所有传播、分支和学习最终都必须保持“存在一个共同赋值满足全部子句”这一量词，不能把分别满足各子句的若干赋值拼成模型。

考虑

从部分赋值 $M=(x=0)$ 出发，第一子句只剩 $y$，所以必须取 $y=1$；第三子句继而只剩 $z$，强制 $z=1$；最后一子句再强制 $w=1$。所得总赋值 $(x,y,z,w)=(0,1,1,1)$ 可逐项核对：四个子句分别由 $y,\mathrm{\neg }x,z,w$ 满足。若起始工作表却是 $x=0,y=0$，第一子句的两个文字都假，它已经冲突，后续怎样选择 $z,w$ 都不能修复。

这个例子展示了可满足分支，但不能据此断言传播总会解决 CNF-SAT。公式

在空赋值下没有单位子句，却不可满足。若决定 $a=1$，后两条子句分别强制 $b=1$ 与 $b=0$；若决定 $a=0$，前两条又给出同一冲突。这两个分支覆盖 $a$ 的全部可能值，才把“传播暂时停住”推进为不可满足证明。

Horn-SAT、2-SAT 等受限语法可有多项式算法，一般 CNF-SAT 的 NP 完全性并不意味着每个实例同样困难，也不允许用某次基准的运行时间替代最坏情形结论。

抽象求解接口可由DPLL 算法理路DPLL 算法DPLL algorithm · Davis–Putnam–Logemann–Loveland algorithm · DPLL交替执行单元传播与布尔分支，并在冲突后回溯以完整判定 CNF 可满足性。实现：单位传播收紧工作表，决策与回溯覆盖尚未检查的赋值。现代冲突驱动子句学习理路冲突驱动子句学习Conflict-driven clause learning · CDCL · Clause-learning SAT solving从传播冲突中推导原公式蕴涵的新子句，并据此非时序回跳和继续搜索的 SAT 算法。还会把一次冲突压缩成由原式蕴涵的新子句，使以后不再进入同类死路。两种算法都只能改变搜索方式，不能改变模型定义。

电路验证、排程、规划和有界模型检查通常先把领域约束编码为 CNF。编码正确性有两个方向：每个编码模型应能解码成合法见证，每个原问题见证也应能扩展成编码模型。前者使 SAT 结论可信，后者使 UNSAT 结论可信。

漏写约束通常放入额外模型，可能造成伪 SAT；误加约束通常删掉合法模型，可能造成伪 UNSAT。例如两项互斥任务都被安排在同一时段，若编码遗漏互斥子句，求解器可以正确地满足这份错误编码。辅助变量编码也应以存在量化后的等可满足性核对，而非要求新增变量与原变量完全同义。

带算术、数组或未解释函数的可满足性模理论理路可满足性模理论Satisfiability modulo theories · SMT判定一阶公式的布尔结构与指定背景理论是否具有同一个满足模型。还要求原子真假能由同一个背景理论模型实现；它与纯 CNF-SAT 易在工具接口上混淆，二者却有不同的模型检查层。

带编号的RUP重放理路证明助理与内核检查Proof assistant and kernel checking · LCF-style trusted kernel · Proof kernel区分证明项与可信内核，并给出带编号、传播提示和删除的RUP证书重放规则、坏证书拒绝及接受可靠性证明。给出四子句UNSAT证书：分别学习相反单位子句、删除原子句，再通过活动编号推出空子句。其可靠性以每个活动子句都被原公式蕴涵为不变量，区分传播中的局部冲突与整个反驳的完成。