Tseitin-Transformation

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

Berechne G mit Var(F)⊆Var(G) und ∀b : b $\models$ F$\iff$∃b' : b⊆b'∧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: ∀b' : val(n_T, b') = val(T, b).

Realisierung:

• falls (Bsp.) T = L∨R, dann n_T↔(n_L∨n_R) als CNF-Constraintsystem
• jedes solche System hat ≤8 Klauseln mit 3 Literalen, es sind ingesamt | F| solche Systeme.