Tseytin transformation

一种将公式转换为等可满足 CNF 形式的变换。与直接暴力应用 De Morgan 律和分配律相比（规模为指数），Tseitin transformation 得到的公式规模为线性，但是需要引入额外辅助变量。

基本思想为：

1. 为原公式 P 中的所有子公式 $\phi$（除 atom 外）引入辅助变量 $x_{\phi }$，包括 P 本身
2. 得到如下等可满足公式：

$$x_P\wedge (x_{\phi }\leftrightarrow \phi [\psi \backslash x_{\psi }])\wedge \dots$$

（每个子公式 $\phi$ 对应一个蕴涵式）

3. 其中每个蕴涵式都可以转换为 CNF 形式，且最多额外引入一个额外的合取项（归纳法易证）

Example

---

Related

• Horn Clause 可以用于将某些非 Horn 子句形式的公式转换为 Horn 形式，需引入辅助谓词