Erfüllbarkeits-Äquivalenz

Def: F mathend000# und G mathend000# erfüllbarkeitsäquivalent, wenn Mod(F)≠∅$\iff$Mod(G)≠∅ mathend000#.

Satz: es gibt einen Polynomialzeit-Algorithmus, der zu jeder Formel F mathend000# eine erfüllbarkeitsäquivalente CNF-Formel G mathend000# berechnet.

also auch | G| = Poly(| F|) mathend000#