vereinfachte Annahme: SAT-Solver ist schneller, wenn
- weniger (Zusatz-)Variablen
- weniger Klauseln
führt zu der Aufgabe:
- Eingabe: boolesche Formel F
mathend000#
- Ausgabe: kleine zu F
mathend000# (erfüllbarkeits)äquivalente CNF.
Anwendungen:
- F
mathend000# ist Halbadder, Volladder
- F
mathend000# ist Addition, Multiplikation usw. für geringe Bitbreite
Aber: mehr Klauseln
⇒
mathend000# mehr Propagationen
2014-03-31
