vereinfachte Annahme: SAT-Solver ist schneller, wenn
- weniger (Zusatz-)Variablen
- weniger Klauseln
führt zu der Aufgabe:
- Eingabe: eine boolesche Formel F
- Ausgabe: eine klein(st)e zu F (erfüllbarkeits)äquivalente CNF.
Anwendungen:
- F ist Halbadder, Volladder
- F ist Addition, Multiplikation usw. für geringe Bitbreite
2009-06-22
