Benutzung von SAT-Solvern

Eingabeformat: SAT-Problem in CNF:

• Variable = mathend000# positive natürliche Zahl
• Literal = mathend000# ganze Zahl (≠ 0 mathend000#, mit Vorzeichen)
• Klausel = mathend000# Zeile, abgeschlossen durch 0 mathend000#.
• Programm = mathend000# 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