Konfliktgesteuertes Klausellernen - Conflict-driven clause learning

In der Informatik ist das konfliktgetriebene Klausellernen ( CDCL ) ein Algorithmus zur Lösung des Booleschen Erfüllbarkeitsproblems (SAT). Bei einer booleschen Formel verlangt das SAT-Problem eine Zuweisung von Variablen, damit die gesamte Formel wahr ist. Die interne Funktionsweise von CDCL SAT-Solvern wurde von DPLL-Solvern inspiriert .

Konfliktgesteuertes Klausellernen wurde von Marques-Silva und Sakallah (1996, 1999) sowie Bayardo und Schrag (1997) vorgeschlagen.

Hintergrund

Um eine klare Vorstellung vom CDCL-Algorithmus zu erhalten, ist Hintergrundwissen zu den folgenden Themen erforderlich.

Boolesches Erfüllbarkeitsproblem

Das Erfüllbarkeitsproblem besteht darin, eine befriedigende Zuordnung für eine gegebene Formel in konjunktiver Normalform (KNF) zu finden.

Ein Beispiel für eine solche Formel ist:

( ( nicht A ) oder ( nicht C ) )   und   ( B oder C ),

oder in einer gängigen Notation:

${\displaystyle (A'\lor C')\land (B\lor C)}$

wobei A , B , C Boolesche Variablen sind, , , , und Literale und und Klauseln sind. ${\displaystyle A'}$${\displaystyle C'}$${\displaystyle B}$${\displaystyle C}$${\displaystyle A'\lor C'}$${\displaystyle B\lor C}$

Eine befriedigende Zuweisung für diese Formel ist zB:

${\displaystyle A=Falsch,B=Falsch,C=Wahr}$

da es die erste Klausel wahr macht (da ist wahr) sowie die zweite (da ist wahr). ${\displaystyle A'}$${\displaystyle C}$

Dieses Beispiel verwendet drei Variablen ( A , B , C ) und es gibt zwei mögliche Zuweisungen (Wahr und Falsch) für jede von ihnen. Also hat man Möglichkeiten. In diesem kleinen Beispiel kann man eine Brute-Force-Suche verwenden , um alle möglichen Zuweisungen auszuprobieren und zu überprüfen, ob sie der Formel entsprechen. Aber in realistischen Anwendungen mit Millionen von Variablen und Klauseln ist eine Brute-Force-Suche unpraktisch. Die Aufgabe eines SAT-Solvers besteht darin, effizient und schnell eine zufriedenstellende Aufgabe zu finden, indem er verschiedene Heuristiken für komplexe CNF-Formeln anwendet. ${\displaystyle 2^{3}=8}$

Einheitsklauselregel (Einheitsausbreitung)

Wenn bei einer nicht erfüllten Klausel alle Literale oder Variablen bis auf eines mit False ausgewertet werden, muss das freie Literal True sein, damit die Klausel True ist. Zum Beispiel, wenn die folgende unzufriedene Klausel mit ausgewertet wird und wir haben müssen , damit die Klausel wahr ist. ${\displaystyle A=Falsch}$${\displaystyle B=Falsch}$${\displaystyle C=Wahr}$${\displaystyle (A\lor B\lor C)}$

Boolesche Einschränkungspropagation (BCP)

Die iterierte Anwendung der Einheitsklauselregel wird als Einheitsausbreitung oder Boolesche Beschränkungsausbreitung (BCP) bezeichnet.

Auflösung

Betrachten Sie zwei Klauseln und . Die Klausel , die durch Zusammenführen der beiden Klauseln und Entfernen von beiden und erhalten wird , wird als Resolvent der beiden Klauseln bezeichnet. ${\displaystyle (A\lor B\lor C)}$${\displaystyle (\neg C\lor D\lor\neg E)}$${\displaystyle (A\lor B\lor D\lor\neg E)}$${\displaystyle \neg C}$${\displaystyle C}$

DP-Algorithmus

Der DP-Algorithmus wurde 1960 von Davis und Putnam eingeführt. Informell führt der Algorithmus iterativ die folgenden Schritte aus, bis keine Variablen mehr in der Formel übrig sind:

• Wählen Sie eine Variable aus und fügen Sie alle nicht tautologischen Resolventen hinzu (ein Resolver ist nicht tautologisch, wenn er und für eine Variable nicht enthält ).${\displaystyle A}$${\displaystyle A}$${\displaystyle V}$${\displaystyle \neg V}$${\displaystyle V}$
• Entfernen Sie alle ursprünglichen Klauseln, die .${\displaystyle A}$

DPLL-Algorithmus

Davis, Putnam, Logemann, Loveland (1962) hatten diesen Algorithmus entwickelt. Einige Eigenschaften dieses Algorithmus sind:

• Es basiert auf der Suche.
• Es ist die Basis für fast alle modernen SAT-Solver.
• Es verwendet chronologisches Backtracking, ohne zu lernen.

Ein Beispiel mit Visualisierung des DPLL-Algorithmus mit chronologischem Backtracking:

• 

  Alle Klauseln, die eine CNF-Formel bilden

• 

  Wähle eine Variable

• 

  Treffen Sie eine Entscheidung, Variable a = False (0), daher werden grüne Klauseln True

• 

  Nach mehreren Entscheidungsfindungen finden wir einen Implikationsgraphen , der zu einem Konflikt führt.

• 

  Gehen Sie jetzt zurück auf die unmittelbare Ebene und weisen Sie dieser Variablen zwangsweise den entgegengesetzten Wert zu

• 

  Aber eine erzwungene Entscheidung führt immer noch zu einem weiteren Konflikt

• 

  Gehen Sie zum vorherigen Level zurück und treffen Sie eine erzwungene Entscheidung

• 

  Treffen Sie eine neue Entscheidung, die jedoch zu einem Konflikt führt

• 

  Treffen Sie eine erzwungene Entscheidung, aber dies führt erneut zu einem Konflikt

• 

  Zurück zum vorherigen Level

• 

  Fahren Sie auf diese Weise fort und der letzte Implikationsgraph

CDCL (konfliktgetriebenes Klausellernen)

Der Hauptunterschied zwischen CDCL und DPLL besteht darin, dass das Zurückspringen von CDCL nicht chronologisch ist.

Konfliktgesteuertes Klausellernen funktioniert wie folgt.

1. Wählen Sie eine Variable aus und weisen Sie True oder False zu. Dies wird als Entscheidungszustand bezeichnet. Merken Sie sich die Aufgabe.
2. Wenden Sie die Boolesche Beschränkungsausbreitung (Einheitenausbreitung) an.
3. Erstellen Sie den Implikationsgraphen.
4. Bei Konflikten
   1. Finden Sie den Schnitt im Implikationsgraphen, der zum Konflikt geführt hat
   2. Leiten Sie eine neue Klausel ab, die die Negation der Zuweisungen ist, die zum Konflikt geführt haben
   3. Nicht chronologisch zurückverfolgen ("Zurücksprung") auf die entsprechende Entscheidungsebene, wo die zuerst zugewiesene am Konflikt beteiligte Variable zugewiesen wurde
5. Andernfalls fahren Sie mit Schritt 1 fort, bis alle Variablenwerte zugewiesen sind.

Beispiel

Ein visuelles Beispiel für den CDCL-Algorithmus:

• 

  Wählen Sie zunächst eine Verzweigungsvariable, nämlich x1 . Ein gelber Kreis bedeutet eine willkürliche Entscheidung.

• 

  Wenden Sie nun die Einheitenausbreitung an, was ergibt, dass x4 1 sein muss (dh wahr). Ein grauer Kreis bedeutet eine erzwungene Variablenzuweisung bei der Einheitenausbreitung. Der resultierende Graph wird Implikationsgraph genannt .

• 

  Wählen Sie willkürlich eine andere Verzweigungsvariable, x3 .

• 

  Wenden Sie die Einheitspropagation an und finden Sie den neuen Implikationsgraphen.

• 

  Hier werden die Variablen x8 und x12 gezwungen, 0 bzw. 1 zu sein.

• 

  Wählen Sie eine andere Verzweigungsvariable, x2 .

• 

  Implikationsdiagramm finden.

• 

  Wählen Sie eine andere Verzweigungsvariable, x7 .

• 

  Implikationsdiagramm finden.

• 

  Konflikt gefunden!

• 

  Finden Sie den Schnitt, der zu diesem Konflikt geführt hat. Finden Sie im Schnitt eine widersprüchliche Bedingung.

• 

  Nehmen Sie die Negation dieser Bedingung und machen Sie daraus eine Klausel.

• 

  Fügen Sie dem Problem die Konfliktklausel hinzu.

• 

  Nicht-chronologischer Rücksprung zur entsprechenden Entscheidungsebene, die in diesem Fall die zweithöchste Entscheidungsebene der Literale in der gelernten Klausel ist.

• 

  Zurückspringen und Variablenwerte entsprechend setzen.

Vollständigkeit

DPLL ist ein solider und vollständiger Algorithmus für SAT. CDCL-SAT-Solver implementieren DPLL, können jedoch neue Klauseln lernen und nicht chronologisch zurückverfolgen. Das Lernen von Klauseln mit Konfliktanalyse hat keinen Einfluss auf die Solidität oder Vollständigkeit. Die Konfliktanalyse identifiziert neue Klauseln unter Verwendung der Auflösungsoperation. Daher kann jede gelernte Klausel aus den ursprünglichen Klauseln und anderen gelernten Klauseln durch eine Folge von Auflösungsschritten abgeleitet werden. Wenn cN die neue gelernte Klausel ist, dann ist ϕ genau dann erfüllbar, wenn auch ϕ ∪ {cN} erfüllbar ist. Darüber hinaus beeinflusst der modifizierte Rückverfolgungsschritt auch nicht die Korrektheit oder Vollständigkeit, da Rückverfolgungsinformationen von jeder neuen gelernten Klausel erhalten werden.

Anwendungen

Die Hauptanwendung des CDCL-Algorithmus liegt in verschiedenen SAT-Solvern, einschließlich:

• MiniSAT
• Zchaff SAT
• Z3
• Glucose
• Viele SAT usw.

Der CDCL-Algorithmus hat SAT-Löser so leistungsfähig gemacht, dass sie in mehreren realen Anwendungsbereichen wie KI-Planung, Bioinformatik, Softwaretestmustergenerierung, Softwarepaketabhängigkeiten, Hardware- und Softwaremodellprüfung und Kryptographie effektiv eingesetzt werden.

Verwandte Algorithmen

Zu CDCL verwandte Algorithmen sind der zuvor beschriebene DP- und DPLL-Algorithmus. Der DP-Algorithmus verwendet eine Auflösungswiderlegung und weist ein potenzielles Speicherzugriffsproblem auf. Während der DPLL-Algorithmus für zufällig generierte Instanzen in Ordnung ist, ist er für Instanzen, die in praktischen Anwendungen generiert werden, schlecht. CDCL ist ein leistungsfähigerer Ansatz zur Lösung solcher Probleme, da die Anwendung von CDCL im Vergleich zu DPLL weniger Zustandsraumsuche bietet .

• 

  DPLL: kein Lernen und chronologisches Backtracking.

• 

  CDCL: konfliktgetriebenes Klausellernen und nicht-chronologisches Backtracking.

zitierte Werke

Verweise

• Martin Davis; Hilary Putnam (1960). „Ein Rechenverfahren für die Quantifizierungstheorie“. J. ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID  31888376 .
• Martin Davis; George Logemann; Donald Loveland (Juli 1962). „Ein Maschinenprogramm zum Beweisen von Theoremen“. Mitteilungen des ACM . 5 (7): 394–397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID  15866917 .
• Matthew W. Moskewicz; Conor F. Madigan; Ying-Zhao; Lintao Zhang; Sharad Malik (2001). "Chaff: Entwicklung eines effizienten SAT-Solvers" (PDF) . Proz. 38. Ann. Konferenz für Designautomatisierung (DAC) . S. 530–535.
• Lintao Zhang; Conor F. Madigan; Matthew H. Moskewicz; Sharad Malik (2001). "Effizientes konfliktgesteuertes Lernen in einem Booleschen Erfüllbarkeitslöser" (PDF) . Proz. IEEE/ACM-Int. Konf. zum Thema Computer-Aided Design (ICCAD) . S. 279–285.
• Präsentation – "SAT-Solving: From Davis-Putnam to Zchaff and Beyond" von Lintao Zhang. (Mehrere Bilder stammen aus seiner Präsentation)