Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von „Erfüllbarkeit“) ist ein Entscheidungsproblem der theoretischen Informatik. Es beschäftigt sich mit der Frage, ob eine gegebene aussagenlogische Formel erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von mit den Werten wahr oder falsch, sodass zu wahr ausgewertet wird?
SAT gehört zur Komplexitätsklasse NP der Probleme, die von einer nichtdeterministischen Turingmaschine in polynomieller Zeit gelöst werden können. Außerdem war SAT das erste Problem, für das NP-Vollständigkeit nachgewiesen wurde (Satz von Cook). Damit kann jedes Problem aus NP in polynomieller Zeit auf SAT zurückgeführt werden (Polynomialzeitreduktion). NP-vollständige Probleme stellen also eine Art obere Schranke für die Schwierigkeit von Problemen in NP dar.
Eine deterministische Turingmaschine (etwa ein konventioneller Computer) kann SAT in exponentieller Zeit entscheiden, zum Beispiel durch das Aufstellen einer Wahrheitstabelle. Es ist kein effizienter Algorithmus für SAT bekannt und es wird allgemein vermutet, dass ein solcher Polynomialzeitalgorithmus nicht existiert. Die Frage, ob SAT in polynomieller Zeit gelöst werden kann, ist äquivalent zum P-NP-Problem, einem der bekanntesten offenen Probleme der theoretischen Informatik.
Ein Großteil der Forschung beschäftigt sich mit der Entwicklung möglichst effizienter Verfahren zur Lösung von SAT in der Praxis (sogenannter SAT-Solver). Moderne SAT-Solver können Instanzen mittlerer Schwierigkeit mit hunderten Millionen Variablen oder Klauseln in praktikabler Zeit lösen. Das ist ausreichend für praktische Anwendungen, z. B. in der formalen Verifikation, in der künstlichen Intelligenz, in der Electronic Design Automation und in verschiedenen Planungs- und Schedulingalgorithmen.
Sie gehören zu den Constraint Satisfaction Problems (CSP).
Terminologie Eine aussagenlogische Formel besteht aus Variablen, Klammern und den aussagenlogischen Verknüpfungen Konjunktion („und“, oft notiert mit ∧), Disjunktion („oder“, ∨) und Negation („nicht“, ¬). Eine Variable kann entweder den Wert wahr oder den Wert falsch annehmen. Ein Literal ist ein Auftreten einer Variable (positives Literal) oder ihrer Negation (negatives Literal). Ein Literal heißt pur, wenn es nur in einer Ausprägung, also entweder positiv oder negativ, vorkommt. Ein Monom ist eine endliche Menge von Literalen, die ausschließlich konjunktiv verknüpft sind. Eine Klausel ist eine endliche Menge von Literalen, die ausschließlich disjunktiv verknüpft sind. Eine Einheitsklausel ist eine Klausel, die nur aus einem einzelnen Literal besteht. Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal.
Eine aussagenlogische Formel ist in konjunktiver Normalform (KNF), wenn sie nur aus Konjunktionen von Klauseln besteht. Eine Horn-Formel ist eine konjunktive Normalform, die ausschließlich aus Horn-Klauseln besteht. Die Formel befindet sich in konjunktiver Normalform. Da nur die erste und die dritte Klausel Horn-Klauseln sind, ist sie aber keine Horn-Formel. Die dritte Klausel ist eine Einheitsklausel.
Eine aussagenlogische Formel ist in disjunktiver Normalform (DNF), wenn sie nur aus Disjunktionen von Monomen besteht. Die Formel befindet sich in disjunktiver Normalform.
Definition und Varianten Eine Formel heißt genau dann erfüllbar, wenn eine Zuweisung von Werten wahr oder falsch zu jeder Variable existiert, sodass die Formel wahr ist. Formal ist SAT definiert als die formale Sprache
ist aussagenlogische Formel und erfüllbar
In der Praxis versteht man unter SAT meistens das Problem, herauszufinden ob eine Formel erfüllbar ist. Es existieren zahlreiche Varianten und für die meisten Komplexitätsklassen existiert eine Variante von SAT, die bezüglich dieser Klasse vollständig ist.
Polynomiell entscheidbare Varianten von SAT
HORNSAT beschränkt SAT auf Horn-Formeln, das heißt auf Formeln in konjunktiver Normalform bei der jede Klausel höchstens ein positives Literal enthält. HORNSAT ist P-vollständig und in Linearzeit entscheidbar. DNF-SAT beschränkt SAT auf Formeln, die in disjunktiver Normalform gegeben sind. DNF-SAT ist in polynomieller Zeit entscheidbar, da eine in DNF gegebene Formel genau dann erfüllbar ist, wenn es ein Monom gibt das keine komplementären Literale enthält. 2-SAT beschränkt SAT auf Formeln, deren Klauseln maximal 2 Literale enthalten. 2-SAT ist in Linearzeit entscheidbar.
3-SAT Das Problem 3-SAT schränkt die Anzahl Literale auf 3 Literale pro Klausel ein. Trotz dieser Einschränkung ist 3-SAT NP-vollständig, da SAT sich in polynomieller Zeit auf 3-SAT reduzieren lässt. Dasselbe gilt für alle Probleme k-SAT mit k > 3.
P3-SAT Eine Instanz des Problems 3-SAT, bestehend aus p Variablen und q Klauseln, lässt sich auch mittels eines Graphen mit (p + q) vielen Knoten darstellen. Eine Formel ist in P3-SAT, wenn sie in 3-SAT ist und dieser Graph planar ist. P3-SAT ist NP-vollständig.
MAX-SAT Das Problem MAX-SAT besteht darin, die maximale Anzahl erfüllbarer Klauseln einer gegebenen Formel zu bestimmen. MAX-SAT ist NP-vollständig und sogar APX-vollständig. Daraus folgt, dass kein PTAS für MAX-SAT existieren kann, falls P ≠ NP.
MAJ-SAT MAJ-SAT ist das Problem zu entscheiden, ob die Mehrzahl aller möglichen Variablenbelegungen die Formel erfüllt. MAJ-SAT ist PP-vollständig.
QBF (QSAT) QBF verallgemeinert SAT für quantifizierte, aussagenlogische Formeln, also Formeln, die Quantoren enthalten. QBF ist PSPACE-vollständig.
Algorithmen Da SAT NP-vollständig ist, sind ausschließlich Exponentialzeitalgorithmen für SAT bekannt. Seit den 2000er Jahren werden aber effiziente und skalierbare Algorithmen (SAT-Solver) entwickelt, die praktikables SAT-Solving für zahlreiche Anwendungen erlauben. Beispiele für Anwendungen sind formale Verifikation, Künstliche Intelligenz, Electronic Design Automation und verschiedene Planungs- und Schedulingalgorithmen.
SAT-Solver können aufgrund ihrer Funktionsweise in verschiedene Klassen eingeteilt werden.
Ein grundlegender randomisierter Algorithmus zur Lösung des k-SAT-Problems stammt von Uwe Schöning (1999), die Randomisierung konnte später von Robin A. Moser vollständig entfernt werden (um 2009). Der schnellste bekannte (randomisierte) Algorithmus für allgemeines k-SAT ist PPSZ (Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, Francis Zane),Paturi, Pudlàk, Saks, Zane, An improved exponential-time algorithm for K-SAT, J. ACM, Band 52, 2005, S. 337–364Dominik Schweder, John P. Steinberger, PPSZ for General k-SAT – Making Hertli’s Analysis Simpler and 3-SAT Faster, 2017, Online entstanden aus dem Vorläufer PPZ von 1999, der nicht so gut wie der Algorithmus von Schöning war, und basierend auf Encoding. 2014 gab Timon Hertli Verbesserungen für den Fall unique 3-SAT.Hertli: Breaking the PPSZ Barrier for Unique 3-SAT. In: Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, Elias Koutsoupias (Hrsg.): Automata, Languages, and Programming – 41st International Colloquium, ICALP 2014, Kopenhagen, Juli 2014. Teil 1: Proceedings, Part I: Lecture Notes in Computer Science 8572. Springer 2014, S. 600–611
Backtracking und DPLL Der Davis-Putnam-Logemann-Loveland-Algorithmus (DPLL oder DLL) aus den 1960er Jahren war der erste SAT-Solver, der eine systematische Suche mittels Backtracking implementierte. Er ist nicht zu verwechseln mit dem Davis-Putnam-Algorithmus, auf dem er basiert. Viele moderne Ansätze basieren auf dem gleichen Konzept und optimieren oft lediglich die Effizienz des Algorithmus für bestimmte Klassen von Eingaben, wie z. B. zufällige SAT-Instanzen oder Instanzen, die in Anwendungen der Industrie auftreten. DPLL löst das CNF-SAT-Problem. Das bedeutet, die aussagenlogischen Formeln müssen in der konjunktiven Normalform vorliegen (Menge von Klauseln).
Ein grundlegender Backtracking-Algorithmus für eine Formel funktioniert wie folgt: Wähle ein Literal aus . Weise einen Wahrheitswert wahr oder falsch zu. Vereinfache zu , indem alle Klauseln entfernt werden, die nun wahr sind und alle Literale entfernt werden, die nun falsch sind. Splitting Rule. Prüfe rekursiv, ob erfüllbar ist. ist erfüllbar ist erfüllbar. ist nicht erfüllbar: Weise den komplementären Wahrheitswert zu. Vereinfache und prüfe dann erneut rekursiv, ob die resultierende Formel erfüllbar ist. Ist erfüllbar, so ist auch erfüllbar. Ist nicht erfüllbar, so ist auch nicht erfüllbar.
Der Algorithmus terminiert, wenn eine Klausel leer wird (nicht erfüllbar, ihr letztes Literal wurde falsch) oder wenn alle Variablen belegt sind (erfüllbar).
DPLL verbessert den simplen Backtracking-Algorithmus durch zwei Regeln.
Einheitsresolution (Unit Propagation) Tritt eine Einheitsklausel auf, so muss ihr einziges Literal wahr sein. Weise dem Literal den entsprechenden Wahrheitswert zu und entferne alle Klauseln, die enthalten. Entferne Vorkommen des Literals aus allen Klauseln.
In der Praxis führt Einheitsresolution oft dazu, dass wiederum Einheitsklauseln erzeugt werden und somit der naive Suchraum signifikant verkleinert wird.
Pure Literal Elimination Kommt ein Literal als pures Literal vor, so kann ihm ein Wert zugewiesen werden, sodass alle Klauseln, die das Literal enthalten, wahr werden. Entferne diese Klauseln.
Der Algorithmus zusammengefasst im Pseudocode: function DPLL(F : set of clauses) # Konsistent bedeutet, es kommt ausschließlich ¬l oder l vor if F is a consistent set of literals then # Hier können zusätzlich die Literale zurückgegeben werden return true; if F contains an empty clause then return false; for every unit clause {l} in F do F ← unit-propagate(l, F); for every literal l that occurs pure in F do F ← pure-literal-assign(l, F); l ← choose-literal(F); # Mit Kurzschlussauswertung für das Oder return DPLL({F : l = true}) or DPLL({F : l = true}); # Dabei wenden unit-propagate(l, F) und pure-literal-assign(l, F) die beiden Regeln entsprechend an und geben die vereinfachte Formel zurück.
Die Effizienz von DPLL hängt sehr stark von der Auswahl des Literals (Branching Literal) ab. Für manche Instanzen kann diese Wahl den Unterschied zwischen konstanter und exponentieller Laufzeit ausmachen. Darum definiert DPLL vielmehr eine ganze Familie von Algorithmen, die unterschiedliche Heuristiken für die Wahl von verwenden.
Die Probleme von DPLL können in drei Punkten zusammengefasst werden: Die Entscheidungen für Branching Literals werden naiv getroffen. Aus Konflikten wird nichts gelernt, außer dass die aktuelle (partielle) Variablenbelegung zu einem Konflikt führt. Dabei lassen sich mehr Informationen über die Ursache des Konfliktes extrahieren und so große Teile des Suchraumes ausschließen. Backtracking springt nur jeweils eine Ebene im Suchbaum nach oben, was zu einem sehr großen Suchraum führt. In der Praxis werden diese Probleme gelöst durch
Heuristiken, z. B. in einem Look-Ahead-Solver Clause Learning (CDCL) Backjumping (CDCL)
Conflict-Driven Clause Learning (CDCL) Modernes Conflict-driven Clause Learning (CDCL) erweitert DPLL um die Konzepte Clause Learning und Backjumping, implementiert Two Watched Literals (TWL, 2WL), um die Suche nach Einheitsklauseln zu beschleunigen und verwendet Random Restarts, um schwierigen Situationen nach einer Reihe von schlechten Entscheidungen für Variablenbelegungen zu entfliehen.
Backjumping und Clause Learning Bei CDCL findet das Backtracking nicht mehr chronologisch statt, sondern es werden Ebenen des Suchbaumes übersprungen. Außerdem werden Informationen über Variablenbelegungen, die in Kombination einen Konflikt verursachen, als Klausel der Klauselmenge hinzugefügt.
Um Backjumping zu ermöglichen, merkt sich CDCL, welche Zuweisungen von Wahrheitswerten zu Variablen willkürlich waren und welche Zuweisungen durch Unit Propagation erzwungen wurden. In der Praxis funktioniert das mittels eines Implikationsgraphen.