Satisfiability (abgekürzt SAT, deutsch Erfüllbarkeitsproblem) ist das zentrale Entscheidungsproblem der Aussagenlogik: Gegeben eine logische Formel, existiert eine Belegung ihrer Variablen, sodass die Formel wahr wird? Die Antwort ist schlicht erfüllbar oder unerfüllbar — und genau diese Frage ist entscheidend für Verifikation, Planung und viele Optimierungsaufgaben.
Formulierung in konjunktiver Normalform
SAT betrachtet Formeln üblicherweise in konjunktiver Normalform (KNF): Eine UND-Verknüpfung von Klauseln, wobei jede Klausel eine ODER-Verknüpfung von Literalen ist (eine Variable oder ihre Negation). Die Praxis bevorzugt KNF, weil sich jede aussagenlogische Formel in KNF überführen lässt und moderne Solver darauf spezialisiert sind. Eine Klausel ist erfüllt, wenn mindestens ein Literal wahr ist; die Gesamtformel ist erfüllbar, wenn alle Klauseln gleichzeitig erfüllbar sind. Ein Spezialfall mit besonderem Namen ist 3-SAT, bei dem jede Klausel genau drei Literale hat — bereits 3-SAT ist schwer lösbar (siehe unten), während 2-SAT in polynomieller Zeit lösbar ist.
Algorithmen und moderne Solver
Die klassische Lösungsstrategie ist DPLL (Davis-Putnam-Logemann-Loveland), ein systematisches Backtracking-Verfahren: Variablen werden nacheinander belegt, vereinfacht und bei Widersprüchen zurückgesetzt. Moderne Solver erweitern DPLL zu CDCL (Conflict-Driven Clause Learning): Sie lernen aus jedem gefundenen Konflikt eine neue Klausel, die den Suchraum dauerhaft beschneidet. Zusammen mit cleveren Heuristiken für die Variablenwahl lösen solche Solver (etwa MiniSat, Glucose, CaDiCaL) heute Probleme mit Millionen von Klauseln — ein bemerkenswerter praktischer Gegensatz zur theoretischen Schwere des Problems.
SAT und NP-Vollständigkeit
Nach dem Cook-Levin-Theorem (1971) ist SAT das erste nachgewiesene NP-vollständige Problem: Jedes Problem aus NP lässt sich in polynomieller Zeit auf SAT reduzieren. In der Praxis wird diese Richtung umgekehrt genutzt: Schwer zu lösende Probleme (Fertigungsplanung, Schaltkreis-Verifikation, Timetabling, Sudoku-artige Constraints) werden in SAT-Formeln übersetzt und mit einem SAT-Solver bearbeitet. SAT ist damit zugleich das theoretische Fundament der Komplexitätstheorie und ein Arbeitstier der industriellen Software- und Hardware-Verifikation.