Tseitin CNF 转换 | Codeboy's Blog

形式陈述

Tseitin 转换接收命题公式或按 DAG 表示的布尔电路 $G$ 。它为每个内部节点 $g$ 引入新变量 $z_g$ ，加入常数个子句表达 $z_g$ 与该门输出的双向定义，并以单位子句断言根变量为真。以二元门为例，

z\leftrightarrow(x\land y)

编码为

(\neg z\lor x)\land(\neg z\lor y) \land(z\lor\neg x\lor\neg y),

而 $z\leftrightarrow(x\lor y)$ 编码为

(\neg x\lor z)\land(\neg y\lor z) \land(x\lor y\lor\neg z).

若原变量集合为 $X$ 、辅助变量集合为 $Z$ 、输出 CNF 为 $T_G(X,Z)$ ，正确的投影陈述是

\alpha\models G \quad\Longleftrightarrow\quad \exists\beta:Z\to\{0,1\},\;\alpha\cup\beta\models T_G.

因此 $G(X)\equiv\exists Z\,T_G(X,Z)$ ，两者经存在量化消去辅助变量后在原词汇上等价； $G$ 与未量化的 $T_G$ 不是同一词汇中的逻辑等价公式。更精确地，令 $D_G$ 只含全部门的双向定义、不含断言根为真的单位子句。对任意原变量赋值 $\alpha$ ，恰有一个 $\beta$ 使 $\alpha\cup\beta\models D_G$ ，它就是逐门求值得到的内部导线赋值；对 $T_G=D_G\land z_{root}$ ，若 $\alpha\models G$ ，这唯一扩张也是模型，若 $\alpha\not\models G$ ，则不存在扩张模型。若每个节点只产生常数个子句，变量与子句总数均为 $O(|G|)$ 。

直觉

直接用分配律把嵌套公式展开成 CNF，可能反复复制同一子公式。Tseitin 转换改用“给中间结果命名”：每个辅助变量像电路导线，局部子句只检查这根导线是否忠实反映相邻门。全局正确性来自所有局部定义同时成立，而不是来自把原公式的全部析取组合展开。

新变量解释了保证为何是投影式的。原赋值只描述外部输入，求解器还要为内部导线选择值；定义子句把这些值钉死在真实门值上。因而一个 CNF 模型投影到 $X$ 必定是原公式模型，一个原模型也能沿电路拓扑顺序扩张成 CNF 模型。所谓“等可满足”不是模糊的同成同败，而是这两条可构造映射。

例子与边界

令

\varphi=(p\land q)\lor\neg r.

取 $u\leftrightarrow p\land q$ 、 $v\leftrightarrow\neg r$ 、 $t\leftrightarrow u\lor v$ ，再断言 $t$ 。完整 CNF 为

\begin{aligned} &(\neg u\lor p)\land(\neg u\lor q) \land(u\lor\neg p\lor\neg q)\\ {}\land{}&(\neg v\lor\neg r)\land(v\lor r)\\ {}\land{}&(\neg u\lor t)\land(\neg v\lor t) \land(u\lor v\lor\neg t)\land(t). \end{aligned}

当 $(p,q,r)=(0,0,0)$ 时，定义依次给出 $(u,v,t)=(0,1,1)$ ，九个子句均真。当 $(p,q,r)=(1,0,1)$ 时，定义强制 $u=v=t=0$ ，与单位子句 $(t)$ 冲突；这正对应原公式为假。这个核对同时显示：任意给辅助变量乱赋值并不能伪造模型。

边界在于并非所有称作“Tseitin-like”的优化都保留上述唯一扩张。Plaisted–Greenbaum 极性编码会在只需某一蕴含方向时省略子句；其正确性依赖根极性和模型投影证明，不能把全双向模板的结论逐字移植。若共享子表达式本来由 DAG 表示，必须只为共享节点建一个变量；先把 DAG 展开成树再编码，可能在进入转换前已经丢失线性规模优势。

推论与应用

Tseitin 编码把电路、程序路径条件和验证条件交给CNF-SAT，同时保留从模型回读原输入的路径。硬件等价检查常编码“两个输出不同”的 miter 并断言其输出；若 CNF 可满足，投影模型给出具体反例输入，若不可满足，才说明在被编码的输入域内没有差异。

局部定义还影响传播强度。两个都保持投影可满足性的编码，可能让单位传播在同一部分赋值下推出不同数量的中间信号；较短 CNF 不必更快，传播更强的模板也不必总能抵消额外子句。编码比较应分别报告规模、可解码性和 propagation completeness，不能把求解器运行时间倒推为逻辑保证。

参考资料

Grigori S. Tseitin, “On the Complexity of Derivation in Propositional Calculus,” in Automation of Reasoning 2, Springer, 1983, pp. 466–483; Russian original, 1968。
David A. Plaisted and Steven Greenbaum, “A Structure-Preserving Clause Form Translation,” Journal of Symbolic Computation 2(3), 1986, pp. 293–304。
Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, 2nd ed., Springer, 2016, §2.3。

形式陈述 ​

形式陈述