Erfüllbarkeitsproblem der Aussagenlogik

Kernidee und Bedeutung

Das Erfüllbarkeitsproblem der Aussagenlogik, kurz SAT (englisch „satisfiability“), ist ein Entscheidungsproblem der theoretischen Informatik. Gegeben ist eine aussagenlogische Formel F. Gesucht ist die Antwort auf die Frage, ob es eine Belegung ihrer Variablen mit den Werten wahr oder falsch gibt, durch die F den Wert wahr erhält. Eine solche Belegung heißt erfüllend; existiert keine, ist die Formel unerfüllbar.

Formal ist SAT die formale Sprache SAT = {F | F ist aussagenlogische Formel und erfüllbar}. SAT gehört zur Komplexitätsklasse NP. Das bedeutet hier, dass eine vorgeschlagene Variablenbelegung in polynomieller Zeit überprüft werden kann. SAT war außerdem das erste Problem, für das NP-Vollständigkeit nachgewiesen wurde (Satz von Cook). Deshalb kann jedes Problem aus NP in Polynomialzeit auf SAT zurückgeführt werden. NP-vollständige Probleme gelten damit als obere Schranke für die Schwierigkeit von Problemen in NP.

Eine deterministische Turingmaschine, etwa ein gewöhnlicher Computer, kann SAT beispielsweise durch eine Wahrheitstabelle in exponentieller Zeit entscheiden. Ein effizienter Polynomialzeitalgorithmus ist nicht bekannt; allgemein wird vermutet, dass ein solcher Algorithmus nicht existiert. Die Frage, ob SAT in polynomieller Zeit lösbar ist, ist äquivalent zum P-NP-Problem, einem der bekanntesten offenen Probleme der theoretischen Informatik.

In der Praxis werden SAT-Solver entwickelt, die SAT-Instanzen möglichst schnell lösen. Moderne Solver können Instanzen mittlerer Schwierigkeit mit hunderten Millionen Variablen oder Klauseln in praktikabler Zeit bearbeiten. Anwendungen gibt es unter anderem in der formalen Verifikation, der künstlichen Intelligenz, der Electronic Design Automation sowie in Planungs- und Schedulingalgorithmen. SAT-Solver gehören zur Klasse der Constraint Satisfaction Problems (CSP).

Grundbegriffe und Formdarstellungen

Eine aussagenlogische Formel besteht aus Variablen, Klammern und den Verknüpfungen Konjunktion („und“, ∧), Disjunktion („oder“, ∨) und Negation („nicht“, ¬). Jede Variable kann wahr oder falsch sein.

Ein Literal ist entweder das Auftreten einer Variable, also ein positives Literal, oder ihre Negation, also ein negatives Literal. Ein Literal heißt pur, wenn es nur in einer Ausprägung, 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 enthält genau ein Literal. Eine Horn-Klausel enthält höchstens ein positives Literal.

Eine Formel ist in konjunktiver Normalform (KNF), wenn sie nur aus Konjunktionen von Klauseln besteht. Eine Horn-Formel ist eine KNF, deren Klauseln sämtlich Horn-Klauseln sind. Die Formel (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ x₃) ∧ ¬x₁ ist eine KNF. Sie ist aber keine Horn-Formel, weil nur die erste und die dritte Klausel Horn-Klauseln sind. Die dritte Klausel ist zugleich eine Einheitsklausel.

Eine Formel ist in disjunktiver Normalform (DNF), wenn sie nur aus Disjunktionen von Monomen besteht. Ein Beispiel ist (x₁ ∧ ¬x₂) ∨ (¬x₁ ∧ x₂ ∧ x₃) ∨ ¬x₁.

Varianten und ihre Komplexität

SAT besitzt zahlreiche Varianten. Für viele Komplexitätsklassen gibt es eine Variante, die bezüglich dieser Klasse vollständig ist.

• HORNSAT beschränkt SAT auf Horn-Formeln, also KNF-Formeln, deren Klauseln höchstens ein positives Literal enthalten. HORNSAT ist P-vollständig und in Linearzeit entscheidbar.
• DNF-SAT beschränkt SAT auf Formeln in disjunktiver Normalform. Eine DNF-Formel ist genau dann erfüllbar, wenn es ein Monom ohne komplementäre Literale gibt, also ohne zugleich ein Literal und seine Negation. Daher ist DNF-SAT in polynomieller Zeit entscheidbar.
• 2-SAT beschränkt SAT auf Formeln, deren Klauseln höchstens zwei Literale enthalten. 2-SAT ist in Linearzeit entscheidbar.
• 3-SAT beschränkt die Klauseln auf höchstens drei Literale. Trotzdem ist 3-SAT NP-vollständig, weil sich SAT in Polynomialzeit auf 3-SAT reduzieren lässt. Dasselbe gilt für k-SAT mit k > 3.

Bei P3-SAT wird eine 3-SAT-Instanz mit p Variablen und q Klauseln durch einen Graphen mit p + q Knoten dargestellt. Sie gehört zu P3-SAT, wenn sie in 3-SAT vorliegt und dieser Graph planar ist. Auch P3-SAT ist NP-vollständig.

MAX-SAT fragt nicht, ob alle Klauseln erfüllbar sind, sondern nach der maximalen Anzahl erfüllbarer Klauseln einer Formel. MAX-SAT ist NP-vollständig und sogar APX-vollständig. Daher kann kein PTAS für MAX-SAT existieren, falls P ≠ NP.

MAJ-SAT entscheidet, ob die Mehrzahl aller möglichen Variablenbelegungen die Formel erfüllt. MAJ-SAT ist PP-vollständig. QBF verallgemeinert SAT auf quantifizierte aussagenlogische Formeln, also Formeln mit Quantoren. QBF ist PSPACE-vollständig.

Systematische Suche mit DPLL

Da SAT NP-vollständig ist, sind für das allgemeine Problem nur Exponentialzeitalgorithmen bekannt. Seit den 2000er Jahren ermöglichen jedoch effiziente und skalierbare SAT-Solver das praktische Lösen vieler großer Instanzen.

Der Davis-Putnam-Logemann-Loveland-Algorithmus, kurz DPLL oder DLL, stammt aus den 1960er Jahren. Er war der erste SAT-Solver mit systematischer Suche durch Backtracking. DPLL darf nicht mit dem Davis-Putnam-Algorithmus verwechselt werden. DPLL löst CNF-SAT, also SAT für Formeln in konjunktiver Normalform.

Ein einfacher Backtracking-Algorithmus wählt ein Literal l aus, weist ihm zunächst einen Wahrheitswert zu und vereinfacht die Formel. Klauseln, die dadurch wahr werden, werden entfernt; Literale, die dadurch falsch werden, werden aus den Klauseln entfernt. Anschließend wird rekursiv geprüft, ob die vereinfachte Formel Fₗ erfüllbar ist. Ist sie erfüllbar, gilt auch F als erfüllbar. Führt diese Wahl zu einer unerfüllbaren Formel, wird l der komplementäre Wahrheitswert zugewiesen und die Prüfung mit F¬l wiederholt. Sind beide Teilprobleme unerfüllbar, ist auch F unerfüllbar.

Der Algorithmus endet, wenn eine leere Klausel entsteht oder alle Variablen belegt sind. Eine leere Klausel bedeutet einen Konflikt, weil ihr letztes Literal falsch geworden ist. Sind alle Variablen belegt, wurde eine erfüllende Belegung gefunden.

DPLL ergänzt dieses Verfahren um zwei Vereinfachungsregeln:

• Bei Einheitsresolution (Unit Propagation) muss das einzige Literal einer Einheitsklausel wahr sein. Alle Klauseln, die dieses Literal enthalten, werden entfernt; Vorkommen des negierten Literals werden aus allen Klauseln gestrichen. Dadurch entstehen oft weitere Einheitsklauseln, sodass der Suchraum deutlich kleiner wird.
• Bei Pure Literal Elimination wird ein pures Literal so belegt, dass alle Klauseln mit diesem Literal wahr werden. Diese Klauseln werden anschließend entfernt.

Die Effizienz hängt stark von der Wahl des Branching Literals ab, also des Literals, über dessen Belegung verzweigt wird. Diese Wahl kann bei bestimmten Instanzen den Unterschied zwischen konstanter und exponentieller Laufzeit ausmachen. DPLL bezeichnet deshalb eher eine Familie von Algorithmen mit unterschiedlichen Heuristiken.

Die wichtigsten Schwächen des einfachen DPLL-Verfahrens sind naive Verzweigungsentscheidungen, fehlendes Lernen aus Konflikten und chronologisches Zurückgehen im Suchbaum jeweils nur um eine Ebene. In der Praxis werden diese Schwächen durch Heuristiken, Clause Learning und Backjumping behandelt.

CDCL: Konflikte analysieren und Suche beschleunigen

Conflict-Driven Clause Learning (CDCL) erweitert DPLL um Clause Learning und Backjumping. Zusätzlich verwendet CDCL Two Watched Literals zur Beschleunigung der Einheitsfortpflanzung sowie Random Restarts, um ungünstigen Zuweisungsfolgen zu entkommen.

Beim Backjumping wird nicht chronologisch zurückgegangen. Der Solver überspringt Suchbaumebenen, die für den aktuellen Konflikt nicht verantwortlich sind. Außerdem werden Kombinationen von Variablenbelegungen, die einen Konflikt verursachen, als neue Klausel gelernt. Eine solche Klausel heißt conflict clause und verhindert, dass dieselbe problematische Kombination später erneut entsteht.

CDCL unterscheidet willkürliche Entscheidungen von durch Unit Propagation erzwungenen Belegungen. Diese Beziehungen werden in einem Implikationsgraphen festgehalten. Ein Implikationsgraph ist ein gerichteter, azyklischer Graph G = (V, E). Seine Knoten bestehen aus Tupeln (x ∈ {false, true}, d), die eine Belegung auf Suchbaumebene d darstellen, oder aus einem Konfliktknoten c. Ein Konflikt liegt vor, wenn ein Literal gleichzeitig wahr und falsch sein müsste. Eine erzwungene Belegung wird durch eine gerichtete Kante von der auslösenden Belegung zur neuen Belegung dargestellt.

Im Beispiel mit den Variablen x₁ bis x₁₂ wird zunächst x₁ = false gewählt. Dadurch wird x₄ = true erzwungen. Danach führt die Wahl x₃ = true zu x₈ = false und anschließend zu x₁₂ = true. Die Wahl x₂ = false erzwingt x₁₁ = true. Wird schließlich x₇ = true gewählt, reduzieren sich die Klauseln (¬x₇ ∨ ¬x₃ ∨ x₉) und (¬x₇ ∨ x₈ ∨ ¬x₉) zu x₉ beziehungsweise ¬x₉. Daraus entsteht ein Konfliktknoten.

Zur Konfliktanalyse werden Schnitte im Implikationsgraphen untersucht. Ein geeigneter Schnitt teilt den Graphen so, dass eine Seite alle Entscheidungsknoten und die andere den Konfliktknoten enthält. Im Beispiel sind x₁, x₃ und x₇ Entscheidungsknoten; x₈ ist dagegen eine Konsequenz früherer Entscheidungen. Ein Schnitt kann etwa die Ursache x₃ ∧ x₇ ∧ ¬x₈ ⇒ Konflikt liefern. Durch Kontraposition entsteht daraus die conflict clause ¬x₃ ∨ ¬x₇ ∨ x₈. Ein anderer Schnitt kann die Klausel ¬x₁ ∨ x₃ ∨ x₇ erzeugen. Das maximale Entscheidungslevel der Variablen in der gelernten Klausel bestimmt, zu welcher Ebene zurückgesprungen wird. Ist der Konflikt nicht auflösbar, meldet CDCL die Formel als unerfüllbar.

Two Watched Literals (TWL oder 2WL) ist eine Datenstruktur. Für jede noch nicht erfüllte Klausel werden zwei Literale beobachtet. Die Klauseln werden über Watch-Listen an den beobachteten Literalen gespeichert. Die zentrale Invariante lautet: „Solange kein Konflikt gefunden wurde darf ein watched literal nur false sein, solange der andere watched literal true ist und alle unwatched literals false sind.“ Wird ein beobachtetes Literal falsch, wird nach Möglichkeit ein anderes nicht falsches Literal als Ersatz beobachtet. Ist das andere beobachtete Literal noch unbelegt, wird Unit Propagation ausgelöst; ist es ebenfalls falsch, liegt ein Konflikt vor. TWL wurde für den SAT-Solver Chaff entwickelt.

Random Restarts setzen die Variablenbelegungen zurück und beginnen mit einer anderen Reihenfolge. Gelernte Klauseln und die aktuell gelernten Informationen werden übernommen. Ein Neustart kann nach einer festen Zahl n von Konflikten, in Abständen nach einer geometrischen Reihe oder dynamisch bei einer Konflikthäufung erfolgen. Die Strategien werden häufig an Instanzklassen angepasst; aggressive Neustarts waren in vielen Fällen effizient.

Lokale Suche, Parallelisierung und Praxis

Lokale-Suche-Solver beginnen mit einer zufälligen Belegung aller Variablen. Sind alle Klauseln erfüllt, geben sie die Belegung zurück. Andernfalls wird eine Variable negiert und die Suche fortgesetzt. Die Formel liegt dabei in KNF vor.

GSAT wählt bevorzugt die Variable, deren Negation die Zahl der unerfüllten Klauseln minimiert, kann aber mit einer bestimmten Wahrscheinlichkeit auch eine zufällige Variable wählen. WalkSAT wählt zunächst eine zufällig ausgewählte unerfüllte Klausel und negiert darin eine Variable. Bevorzugt wird die Variable, durch deren Änderung möglichst wenige bereits erfüllte Klauseln unerfüllt werden. Die Wahrscheinlichkeit, eine falsche Variablenzuweisung zu korrigieren, ist der Kehrwert der Anzahl der Variablen in der Klausel. Beide Verfahren erlauben zufällige Entscheidungen, um lokale Maxima zu umgehen, und zufällige Neustarts, wenn längere Zeit keine Lösung gefunden wird.

Parallele SAT-Solver werden in drei Kategorien eingeteilt: Portfolio, Divide-and-conquer und parallele lokale Suche.

• Portfolio-Solver führen verschiedene SAT-Ansätze parallel aus. Da ein Solver bei manchen Instanzen schnell, bei anderen aber langsam sein kann und sich die beste Methode nicht zuverlässig vorhersagen lässt, werden unterschiedliche Verfahren kombiniert. Nachteilig ist, dass die Prozesse grundsätzlich dieselbe Arbeit verrichten können; trotzdem sind Portfolio-Solver praktisch erfolgreich.
• Cube-and-conquer teilt eine Formel in zwei Phasen auf. In der Cube-Phase wird die Instanz in einige Tausend bis einige Millionen Teilprobleme, sogenannte Würfel, zerlegt. Ein Würfel ist eine Konjunktion einer Teilmenge der Literale der Originalformel F. Mit F konjunktiv verknüpft entsteht jeweils eine Formel F′, die unabhängig bearbeitet werden kann. Die Disjunktion aller F′ ist zu F äquivalent; der Algorithmus endet, sobald ein Teilproblem erfüllbar ist. Entscheidungs-, Richtungs- und Cutoff-Heuristiken bestimmen die Aufteilung. Für die Cube-Phase wird meist ein Look-Ahead-Solver eingesetzt.
• Parallele lokale Suche kann Variablenänderungen parallel durchführen oder unterschiedliche Auswahlstrategien gleichzeitig als Portfolio ausführen.

Die jährliche SAT-Competition findet im Rahmen der International Conference on Theory and Applications of Satisfiability Testing statt. Bewertet werden unter anderem sequentielle Leistung, mäßige Parallelisierung auf einer Shared-Memory-Maschine, massive Parallelisierung auf verteilten Maschinen und inkrementelle SAT-Solver. Inkrementelle Solver bearbeiten eine Folge verwandter SAT-Instanzen und verwenden gelernte Informationen aus früheren Instanzen wieder.

Die SAT-Association fördert Forschung zu SAT, SAT-Solvern und formaler Verifikation, vertritt die SAT-Community, beaufsichtigt die genannten Konferenzen und Wettbewerbe und gibt das Journal on Satisfiability, Boolean Modeling, and Computation (JSAT) heraus.