合取范式

CNF 是一份必须全部满足的约束清单。外层合取要求每条子句成立，内层析取只要求至少一个文字为真；一个子句失败，恰好意味着其中所有文字为假。例如 $(p\vee q)\wedge (\mathrm{\neg }p\vee r)$ 在已知 $q$ 为假时，第一条迫使 $p$ 为真，第二条随即迫使 $r$ 为真。子句既能检查结果，也能传播已经确定的取值。

CNF 的永真性容易逐子句检查：每条子句都必须包含某对 $p,\mathrm{\neg }p$，才能在所有赋值下为真；空合取按约定也永真。可满足性则要找到同时满足所有子句的赋值，不同子句的要求可能互相冲突，一般问题是 NP 完全的。与之对偶的析取范式理路析取范式Disjunctive normal form · DNF由文字的合取形成项，再对这些项取析取得到的命题公式形状。是若干合取方案任选其一，它的可满足性可以逐项检查。不能把“给定赋值容易检查”误解成“一定容易找到赋值”。

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

边界之一是规模：逐层分配可能指数爆炸，当 $n\ge 1$ 且这 $2n$ 个变量两两不同时，公式 $(p_1\wedge q_1)\vee \cdots \vee (p_n\wedge q_n)$ 的任何只使用原变量的等价 CNF 都至少需要 $2^n$ 个子句。这个下界可直接转用DNF 的极小满足赋值论证理路析取范式Disjunctive normal form · DNF由文字的合取形成项，再对这些项取析取得到的命题公式形状。：否定该公式得到 $\underset{i}{\bigwedge }(\mathrm{\neg }{p}_i\vee \mathrm{\neg }{q}_i)$，把各变量真值同时取反便是链接页的例子；而含 $m$ 个子句的 CNF 取否定后只有 $m$ 个 DNF 项，所以 $m\ge 2^n$。

工程上可用Tseitin 转换理路Tseitin CNF 转换Tseitin CNF transformation · Tseitin transformation · Tseitin encoding为公式或布尔电路的内部节点引入辅助变量，以线性规模生成保持可满足性投影的 CNF。：为每个内部子公式引入新变量，用短子句固定相应门的双向定义，并额外用单位子句断言根变量为真。根本身若只是文字，就直接断言该文字。对有界元数的公式或电路节点，输出规模与原表示线性相关。但保证随之减弱——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。