形式陈述

文字是命题变量 $p$$p$ 或其否定 $\neg p$$\mathrm{\neg }p$；子句是有限个文字的析取；合取范式（CNF）是有限个子句的合取：

$$ \bigwedge_{i=1}^m\left(\bigvee_{j=1}^{k_i}\ell_{ij}\right). $$$$\underset{i=1}{\overset{m}{\bigwedge }}\left(\underset{j=1}{\overset{k_i}{\bigvee }}{\ell }_{ij}\right).$$

每个命题公式都与某个 CNF 逻辑等价，可通过消去 $\to,\leftrightarrow$$\to ,\leftrightarrow$、把否定推到变量前，再用分配律得到。直接等价转换可能指数膨胀；Tseitin 转换加入新变量，可在线性规模产生与原公式等可满足的 CNF，其满足赋值投影回原变量恰给原公式模型。

直觉

CNF 是“一组必须全部满足的约束”，每个约束又允许若干文字至少一个成立；它正好匹配 SAT 求解器逐子句排除冲突的工作方式。

例子与边界

$(p\lor\neg q)\land(q\lor r)$$(p\vee \mathrm{\neg }q)\wedge (q\vee r)$ 是 CNF。$p\lor(q\land r)$$p\vee (q\wedge r)$ 可分配为 $(p\lor q)\land(p\lor r)$$(p\vee q)\wedge (p\vee r)$。空子句没有可真文字，表示假；空合取没有约束，表示真。Tseitin 结果通常不是在扩展变量上与原式逐赋值等价，而是通过存在量化新变量保持可满足性，不能混淆两种保证。

推论与应用

CNF 是 SAT、分辨率证明和布尔约束求解的标准输入。$k$$k$-CNF 限制每个子句长度，3-SAT 则是复杂性归约的核心问题。

参考资料

• Kenneth H. Rosen, Discrete Mathematics and Its Applications, 8th ed., McGraw-Hill, 2019，§1.3, propositional equivalences and normal forms。
• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§1.5, Exercise 9, conjunctive normal form。