CNF-Kompression (Motivation)

vereinfachte Annahme: SAT-Solver ist schneller, wenn

• weniger (Zusatz-)Variablen
• weniger Klauseln

führt zu der Aufgabe:

• Eingabe: boolesche Formel F
• Ausgabe: kleine zu F (erfüllbarkeits)äquivalente CNF.

Anwendungen:

• F ist Halbadder, Volladder
• F ist Addition, Multiplikation usw. für geringe Bitbreite

Aber: mehr Klauseln ⇒ mehr Propagationen