Erfüllbarkeits-Äquivalenz

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

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