Benutzung von SAT-Solvern

Eingabeformat: SAT-Problem in CNF:

• Variable = positive natürliche Zahl
• Literal = ganze Zahl (≠ 0, mit Vorzeichen)
• Klausel = Zeile, abgeschlossen durch 0.
• Programm = Header p cnf <#Variablen> <#Klauseln>, dann Klauseln

Beispiel

p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

Löser: minisat input.cnf output.text