Tseitin-Transformation

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

Berechne G mathend000# mit Var(F)⊆Var(G) mathend000# und ∀b : b $\models$ F$\iff$∃b' : b⊆b'∧b' $\models$ G mathend000#.

Plan:

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

Realisierung:

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