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。公式

在空赋值下没有单位子句，却不可满足；要暴露矛盾，必须作决策或使用更强推理。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 也必须保证没有因漏写约束而得到。带算术、数组或未解释函数的可满足性模理论公理库可满足性模理论Satisfiability modulo theories · SMT判定一阶公式的布尔结构与指定背景理论是否具有同一个满足模型。还要求原子真假能由同一个背景理论模型实现；它与纯 CNF-SAT 易在工具接口上混淆，二者却有不同的模型检查层。