Erfüllbarkeits-Äquivalenz

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

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

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