(CNF-)SAT

Das Problem (CNF)-SAT:

• Eingabe: aussagenlog. Formel (in CNF)
• Frage: gibt es erfüllende Belegung?

Eigenschaften

• ist praktisch wichtig (viele Anwendungsaufgaben lassen sich nach SAT übersetzen)
• ist schwer (NP-vollständig) ⇒ wahrscheinlich nicht effizient lösbar
• es gibt erstaunlich gute Heuristiken (Probleme mit 1.000 ...10.000 Variablen lösbar in 1 ...100 Sekunden)

vergleiche http://www.satcompetition.org/