本文共 1609 字，大约阅读时间需要 5 分钟。
Tseitin算法是一个在线性时间内将命题公式转化为CNF范式的算法。
Convert the following formula into CNF with Tseitin’s transformation:
将以下命题公式转化为CNF范式： ( P → ( ¬ Q ∧ R ) ) ∧ ( P → ¬ Q ) (P \to (\lnot Q \land R)) \land (P \to \lnot Q) (P→(¬Q∧R))∧(P→¬Q) The original formula is equivalence to ( ¬ P ∨ ( ¬ Q ∧ R ) ) ∧ ( ¬ P ∨ ¬ Q ) (\neg P\vee (\neg Q\wedge R))\wedge (\neg P \vee \neg Q) (¬P∨(¬Q∧R))∧(¬P∨¬Q) Tseitin算法开始 So we have T 1 ↔ T 2 ∧ T 3 T_{1}\leftrightarrow T_{2}\wedge T_{3} T1↔T2∧T3 T 2 ↔ ¬ P ∨ T 4 T_{2}\leftrightarrow \neg P\vee T_{4} T2↔¬P∨T4 T 3 ↔ ¬ P ∨ ¬ Q T_{3}\leftrightarrow \neg P\vee \neg Q T3↔¬P∨¬Q T 4 ↔ ¬ Q ∧ R T_{4}\leftrightarrow \neg Q\wedge R T4↔¬Q∧R Thus F 1 : ( ¬ T 1 ∨ T 2 ) ∧ ( ¬ T 1 ∨ T 3 ) ∧ ( T 1 ∨ ¬ T 2 ∨ ¬ T 3 ) F_{1}:(\neg T_{1}\vee T_{2})\wedge(\neg T_{1}\vee T_{3})\wedge(T_{1}\vee\neg T_{2} \vee\neg T_{3}) F1:(¬T1∨T2)∧(¬T1∨T3)∧(T1∨¬T2∨¬T3) F 2 : ( ¬ T 2 ∨ ¬ P ∨ T 4 ) ∧ ( T 2 ∨ P ) ∧ ( T 2 ∨ ¬ T 4 ) F_{2}:(\neg T_{2}\vee\neg P\vee T_{4})\wedge (T_{2}\vee P)\wedge (T_{2}\vee\neg T_{4}) F2:(¬T2∨¬P∨T4)∧(T2∨P)∧(T2∨¬T4) F 3 : ( ¬ T 3 ∨ ¬ P ∨ ¬ Q ) ∧ ( T 3 ∨ P ) ∧ ( T 3 ∨ Q ) F_{3}:(\neg T_{3}\vee\neg P\vee\neg Q)\wedge (T_{3}\vee P)\wedge (T_{3}\vee Q) F3:(¬T3∨¬P∨¬Q)∧(T3∨P)∧(T3∨Q) F 4 : ( ¬ T 4 ∨ ¬ Q ) ∧ ( ¬ T 4 ∨ R ) ∧ ( T 4 ∨ Q ∨ ¬ R ) F_{4}:(\neg T_{4}\vee\neg Q)\wedge (\neg T_{4}\vee R)\wedge (T_{4}\vee Q\vee\neg R) F4:(¬T4∨¬Q)∧(¬T4∨R)∧(T4∨Q∨¬R) Finally, the original formula is equivalent in satisfiability with T 1 ∧ F 1 ∧ F 2 ∧ F 3 ∧ F 4 T_{1}\wedge F_{1}\wedge F_{2}\wedge F_{3}\wedge F_{4} T1∧F1∧F2∧F3∧F4F 1 F_1 F1到 F 4 F_4 F4其实就是第二步（就是T在箭头左边那些式子）的等价变形。
copyright: swy
转载地址：http://yuwai.baihongyu.com/