合取范式

CNF 把任意布尔条件整理成"一份必须全部满足的约束清单"：外层合取说每条约束都要过关，内层析取说每条约束给出若干可选的满足方式，至少中一个即可。这恰是约束求解的自然姿态——一个赋值违反某条约束，当且仅当它把该子句的所有文字同时弄假，于是"排查失败原因"可以逐子句进行，这正是 SAT 求解器逐子句传播与学习冲突的工作方式。与之对偶的析取范式公理库析取范式Disjunctive normal form · DNF由若干合取项之析取构成且与原公式逻辑等价的标准形。则是"若干套完整方案任选其一"。值得记住的直观：CNF 易于"看出永真难、看出矛盾易"的对偶现象——检验 CNF 是否永真只需逐子句看是否都含互补文字对，容易；而检验其可满足性是 NP 完全的核心问题。

$(p\vee \mathrm{\neg }q)\wedge (q\vee r)$ 已是 CNF。把 $p\vee (q\wedge r)$ 按分配律展开得 $(p\vee q)\wedge (p\vee r)$，两步真值表即可核对等价。退化情形按约定处理：空子句（零个文字的析取）没有可为真的选项，恒假；空合取（零个子句）没有约束，恒真——这两条约定使归结证明"导出空子句即矛盾"的说法严格成立。

边界之一是规模：逐层分配可能指数爆炸，公式 $(p_1\wedge q_1)\vee \cdots \vee (p_n\wedge q_n)$ 的任何等价 CNF 都需要 $2^n$ 个子句。工程上改用 Tseitin 转换：为每个子公式引入新变量并用短子句钉住其语义，输出规模与原公式线性相关。但保证随之减弱——Tseitin 结果与原公式不是逻辑等价，而是等可满足：新公式可满足当且仅当原公式可满足，其满足赋值投影回原变量恰给原公式的模型。两种保证不可混用：需要在所有赋值下逐点一致时（如电路等价性验证的规格端）等可满足的替身不能顶替等价的原式。

CNF 是布尔可满足性生态的标准输入格式：可满足性公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。问题以 CNF 形态成为 Cook–Levin 定理公理库Cook–Levin 定理Cook–Levin theorem · SAT is NP-complete布尔可满足性问题 SAT 是 NP 完全问题。中第一个 NP 完全问题，限制子句长度后的 3-SAT公理库3-SAT3-SAT · Three-satisfiability每个子句恰含三个文字的合取范式可满足性问题。 则是复杂性归约网络的枢纽——任意 CNF 可经引入新变量拆分长子句改写为等可满足的 3-CNF。证明论方向，归结（resolution）证明系统只操作 CNF 子句，其证明长度下界是证明复杂性理论的经典课题。此外，逻辑程序设计中的 Horn 子句（至多一个正文字的子句）是 CNF 的可高效判定片段，硬件验证与规划问题的编码流水线普遍以 Tseitin 式转换落地为 CNF。