Tseitin-Transformation

Gegeben F, gesucht erfüllbarkeitsäquivalentes G in CNF.

Berechne G mit Var(F) $\subseteq$ Var(G) und $\forall$b : b $\models$ F$\iff$$\exists$b' : b $\subseteq$ b' $\wedge$ b' $\models$ G.

Plan:

• für jeden nicht-Blatt-Teilbaum T des Syntaxbaumes von F eine zusätzliche Variable n_T einführen,
• wobei gelten soll: $\forall$b' : val(n_T, b') = val(T, b').

Realisierung:

• falls (Bsp.) F = L $\vee$ R, dann n_T $\leftrightarrow$ (n_L $\vee$ n_r) als CNF-Constraintsystem
• jedes solche System hat $\le$8 Klauseln mit 3 Literalen, es sind ingesamt | F| solche Systeme.