合取范式

合取范式（conjunctive normal form，简称 CNF）是由若干子句合取而成的命题公式，每个子句是若干文字的析取。文字是命题变量或一个命题变量的否定，例如 $p$ 与 $\mathrm{\neg }q$。CNF 将“所有约束同时成立”写成外层的与，将“一条约束中至少一种选择成立”写成内层的或，是可满足性问题和归结原理的常见输入形式。

考虑公式 $F=\mathrm{\neg }(p\to q)\vee r$。蕴含 $p\to q$ 只在 $p$ 真而 $q$ 假时失败，所以其否定为 $p\wedge \mathrm{\neg }q$。于是 $F$ 表示：要么 $r$ 真，要么同时满足 $p$ 真、$q$ 假。将这个“要么”分配到两个条件后，得到 $$F\equiv (p\vee r)\wedge (\mathrm{\neg }q\vee r).$$ 右端有两个子句，每个子句含两个文字。下面解释这个改写的含义和它的代价。

子句、空子句与空合取

一般 CNF 可写为 $$\underset{i=1}{\overset{m}{\bigwedge }}\left(\underset{j=1}{\overset{k_i}{\bigvee }}{\ell }_{ij}\right),$$ 其中 ${\ell }_{ij}$ 是文字，$m$ 为子句数，$k_i$ 为第 $i$ 个子句的文字数。一文字子句如 $(p)$ 称为单位子句；它直接要求 $p$ 真。子句 $p\vee \mathrm{\neg }p$ 无论如何赋值都真，称为重言子句，可以从外层合取中删除。

把子句视为文字集合时，重复的文字可以删除，因为 $p\vee p\equiv p$。零个文字的析取约定为假，称为空子句，常记为 $◻$；只要 CNF 含有它，整式就不可满足。零个子句的合取约定为真，因而可满足。空子句集和包含空子句的子句集是相反的边界情形，归结程序尤其需要区分它们。

“每个子句至多含三个文字”的公式称为 3-CNF；有的资料将这个名称保留给恰好三个文字的子句，使用时应声明约定。一般 CNF 不要求每个子句列出全部变量；要求每个极大项含所有变量的主合取范式是更特殊的表示。

等价变换的连续步骤

将有限命题公式改成等价 CNF，可以先消去蕴含，再把否定推到变量前，最后使用分配律。原例逐步成为 $$\begin{array}{cc}\mathrm{\neg }(p\to q)\vee r& \equiv \mathrm{\neg }(\mathrm{\neg }p\vee q)\vee r\\ & \equiv (p\wedge \mathrm{\neg }q)\vee r\\ & \equiv (p\vee r)\wedge (\mathrm{\neg }q\vee r).\end{array}$$ 第一步使用蕴含的真值定义，第二步使用德摩根律与双重否定。第三步需要的规律是 $(A\wedge B)\vee C\equiv (A\vee C)\wedge (B\vee C)$。

这一分配律可以直接证明。若 $C$ 为真，两边都真；若 $C$ 为假，左边只剩 $A\wedge B$，右边的两个析取项分别只剩 $A$ 与 $B$，两边仍相同。这两个情况覆盖了每个赋值，因此证明的是逻辑等价，而不只是两个公式碰巧同为可满足。

每行是同一次赋值。两个子句都为一时，原公式也为一。

读图时先看 $r=0$ 的四行。第一子句要求 $p=1$，第二子句要求 $q=0$，所以只留下 $(p,q,r)=(1,0,0)$。再看 $r=1$ 的四行，两个子句都已经被 $r$ 满足，$p,q$ 可任意取值。故原式和 CNF 都有五个满足赋值。这里的五不是从公式外形猜出的，而是从每个子句的要求得到的。

变式为 $\mathrm{\neg }(p\wedge q)\vee r$。将否定推入后直接得到 $\mathrm{\neg }p\vee \mathrm{\neg }q\vee r$，它本身就是只有一个子句的 CNF，无需再分配。唯一使它为假的赋值为 $p=q=1,r=0$，所以它有七个满足赋值。原例中的否定作用于蕴含，变式中作用于合取，不能照抄同一个结果。

等价 CNF 的长度可能指数增长

分配律保持真值，却可能复制大量子公式。例如 $$(a_1\wedge b_1)\vee \cdots \vee (a_k\wedge b_k)$$ 直接分配后，每次从第 $i$ 对中选择 $a_i$ 或 $b_i$，构成一个包含 $k$ 个文字的子句。选择共有 $2^k$ 种。$k=2$ 时四个子句是 $$(a_1\vee a_2)\wedge (a_1\vee b_2)\wedge (b_1\vee a_2)\wedge (b_1\vee b_2).$$ 输入只列了 $k$ 对变量，这种直接转换却产生指数数量的子句。这个例子说明该转换方法的长度增长，不能仅凭它断言每一种扩充变量的编码也都指数增长。

辅助变量与等可满足编码

SAT 编码常引入新变量代表子公式，以控制长度。若用 $z$ 代表 $a\wedge b$，关系 $z\leftrightarrow (a\wedge b)$ 可写成 $$(\mathrm{\neg }z\vee a)\wedge (\mathrm{\neg }z\vee b)\wedge (z\vee \mathrm{\neg }a\vee \mathrm{\neg }b).$$ 前两个子句表达 $z\to a$、$z\to b$；第三个表达 $(a\wedge b)\to z$。所以三个子句同时成立，恰好强制 $z=a\wedge b$。析取门也可类似编码为 $$z\leftrightarrow (a\vee b):(z\vee \mathrm{\neg }a)\wedge (z\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }z\vee a\vee b).$$

给原式每个二元连接词引入一个变量，加入相应门的子句，再加入要求根变量为真的单位子句，就得到 Tseitin 风格编码。连接词集合和每个门的输入数固定时，每个门只贡献常数个有界长子句，总长度与原公式的语法树大小成线性关系。

正确的对应关系是：原公式的每个满足赋值，都能按子公式的实际真值扩展成新 CNF 的满足赋值；反过来，新 CNF 的满足赋值因门约束而保证根变量等于原式的值，根单位子句又保证该值为真。因此原式 $F(x)$ 与编码 $T(x,z)$ 满足 $$F(x)\equiv \mathrm{\exists }zT(x,z).$$ 它们等可满足，但直接把 $F(x)$ 和 $T(x,z)$ 当作同一组自由变量上的等价公式会出错。例如 $F=a\wedge b$ 在 $a=b=1$ 时真；若额外指定根变量 $z=0$，编码却为假。忘记根单位子句也会出错：单独的门关系允许把根设成原式的假值，不能强制原式成立。