Erfüllbarkeitsproblem

Das Erfüllbarkeitsproblem (SAT) ist eines der zentralen Probleme der theoretischen Informatik. Gegeben ist eine boolesche Formel in konjunktiver Normalform (CNF). Die Frage lautet, ob es eine Belegung der Variablen mit Wahrheitwerten gibt, die die gesamte Formel wahr macht. Eine CNF-Formel ist eine Konjunktion von Klauseln, wobei jede Klausel eine Disjunktion von Literalen ist. Ist eine solche Belegung vorhanden, gilt die Formel als erfüllbar; andernfalls ist sie unerfüllbar.

SAT wird oft als Entscheidungsproblem formuliert: Ja oder Nein, existiert eine erfüllende Zuordnung? Wichtige Varianten sind 2-SAT, 3-SAT und k-SAT. Bei 2-SAT (Klauseln mit höchstens zwei Literalen) lässt sich das Problem in polynomialer Zeit lösen. 3-SAT und allgemein k-SAT für k ≥ 3 sind NP-vollständig. Das allgemeine CNF-SAT ist damit als NP-vollständig klassifiziert. Eine weitergehende Generalisierung ist QBF (gequantifizierte Boolesche Formeln), dessen Entscheidungsproblem PSPACE-vollständig ist.

Historisch war SAT das erste Problem, das von Stephen Cook (unabhängig von Leonid Levin) als NP-vollständig gezeigt wurde (Cook–Levin-Theorem, 1971). Dieses Resultat begründete die NP-Vollständigkeit als Maßstab für die Schwierigkeit von Entscheidungsproblemen in der Informatik.

In der Praxis werden SAT-Solver eingesetzt, die auf DPLL-Algorithmen basieren und durch Konfliktlernen (CDCL) weiterentwickelt wurden. Ergänzend kommen lokale Suchverfahren wie WalkSAT zum Einsatz. Anwendungen finden sich in der formalen Verifikation von Software und Hardware, der Modellprüfung, der Constraint-Programmierung und der künstlichen Intelligenz.