Tseitin transformation October 24, 2026 The Tseitin transformation lets us convert any Boolean formula to conjunctive normal form (CNF) by introducing new variables. Let’s say we have the following expression:
ϕ : = ( ( x 1 ∨ x 2 ) ⇔ x 3 ) ⇒ ( ¬ x 4 ) . \phi := \htmlClass{tseitin-expression-4}{\htmlClass{tseitin-expression-2}{(\htmlClass{tseitin-expression-1}{(x_1 \lor x_2)} \Leftrightarrow x_3)} \Rightarrow \htmlClass{tseitin-expression-3}{(\lnot x_4)}}. ϕ := ( ( x 1 ∨ x 2 ) ⇔ x 3 ) ⇒ ( ¬ x 4 ) . Step 1. Associate new variables with the subexpressions.
y 1 ⇔ ( x 1 ∨ x 2 ) \htmlClass{tseitin-term tseitin-y1}{y_1} \Leftrightarrow (x_1 \lor x_2) y 1 ⇔ ( x 1 ∨ x 2 ) y 2 ⇔ ( y 1 ⇔ x 3 ) \htmlClass{tseitin-term tseitin-y2}{y_2} \Leftrightarrow (\htmlClass{tseitin-term tseitin-y1}{y_1} \Leftrightarrow x_3) y 2 ⇔ ( y 1 ⇔ x 3 ) y 3 ⇔ ¬ x 4 \htmlClass{tseitin-term tseitin-y3}{y_3} \Leftrightarrow \lnot x_4 y 3 ⇔ ¬ x 4 y 4 ⇔ ( y 2 ⇒ y 3 ) . \htmlClass{tseitin-term tseitin-y4}{y_4} \Leftrightarrow (\htmlClass{tseitin-term tseitin-y2}{y_2} \Rightarrow \htmlClass{tseitin-term tseitin-y3}{y_3}). y 4 ⇔ ( y 2 ⇒ y 3 ) .
Step 2. Restate the formula using these definitions.
C : = y 4 ∧ ( y 4 ⇔ ( y 2 ⇒ y 3 ) ) ∧ ( y 3 ⇔ ¬ x 4 ) ∧ ( y 2 ⇔ ( y 1 ⇔ x 3 ) ) ∧ ( y 1 ⇔ ( x 1 ∨ x 2 ) ) . \begin{aligned}
C := {} & \htmlClass{tseitin-term tseitin-y4}{y_4} \land (\htmlClass{tseitin-term tseitin-y4}{y_4} \Leftrightarrow (\htmlClass{tseitin-term tseitin-y2}{y_2} \Rightarrow \htmlClass{tseitin-term tseitin-y3}{y_3})) \\
&\land (\htmlClass{tseitin-term tseitin-y3}{y_3} \Leftrightarrow \lnot x_4) \\
&\land (\htmlClass{tseitin-term tseitin-y2}{y_2} \Leftrightarrow (\htmlClass{tseitin-term tseitin-y1}{y_1} \Leftrightarrow x_3)) \\
&\land (\htmlClass{tseitin-term tseitin-y1}{y_1} \Leftrightarrow (x_1 \lor x_2)).
\end{aligned} C := y 4 ∧ ( y 4 ⇔ ( y 2 ⇒ y 3 )) ∧ ( y 3 ⇔ ¬ x 4 ) ∧ ( y 2 ⇔ ( y 1 ⇔ x 3 )) ∧ ( y 1 ⇔ ( x 1 ∨ x 2 )) . The rest is fairly straightforward: we rewrite each equivalence as CNF using its truth table.
If you’re interested in more details, check out this tutorial .