SAT-Algorithmen, die nicht auf DPLL basieren

Antworten:

21

Die Auflösungssuche (nur das Anwenden der Auflösungsregel mit einigen guten Heuristiken) ist eine weitere mögliche Strategie für SAT-Löser. Theoretisch ist es exponentiell leistungsfähiger (dh es gibt Probleme, für die es exponentiell kürzere Beweise gibt) als DPLL (das nur die Baumauflösung ausführt, obwohl Sie es mit nogood learning erweitern können, um seine Leistung zu steigern - ob das es so leistungsfähig macht wie die allgemeine Auflösung noch ist) offen, soweit ich weiß), aber ich kenne keine tatsächliche Implementierung, die eine bessere Leistung erbringt.

Wenn Sie sich nicht auf die vollständige Suche beschränken, ist WalkSat ein lokaler Suchlöser, mit dem Sie zufriedenstellende Lösungen finden und die DPLL-basierte Suche in vielen Fällen übertreffen können. Man kann es jedoch nicht verwenden, um Unzufriedenheit zu beweisen, wenn man nicht alle fehlgeschlagenen Zuweisungen zwischenspeichert, was zu einem exponentiellen Speicherbedarf führen würde.

Bearbeiten: Hinzufügen vergessen - Schnittebenen können ebenfalls verwendet werden (durch Reduzieren von SAT auf ein ganzzahliges Programm). Insbesondere Gomory-Schnitte reichen aus, um ein ganzzahliges Programm optimal zu lösen. Auch im schlimmsten Fall kann eine Exponentialzahl erforderlich sein. Ich denke, Arora & Baraks Computational Complexity-Buch enthält noch ein paar Beispiele für Beweissysteme, die man theoretisch für eine Art SAT-Lösung verwenden könnte. Auch hier habe ich keine schnelle Implementierung außer DPLL-basierten oder lokalen Suchmethoden gesehen.

Opt
quelle
9
Es hat sich gezeigt, dass DPLL mit Klausellernen (oder Nogood Learning, wie Sie es nennen) und Neustarten der allgemeinen Auflösung entspricht.
Jan Johannsen
1
@JanJohannsen, ist das das Papier, auf das Sie sich beziehen? arxiv.org/abs/1107.0044
Radu GRIGore
5
Ja, es gibt auch eine Verbesserung in folgendem Artikel: Knot Pipatsrisawat und Adnan Darwiche. Über die Möglichkeiten von SAT-Lösern zum Lernen von Klauseln als Auflösungsmotoren. Artificial Intelligence 175 (2), 2011, S. 512–525. dx.doi.org/10.1016/j.artint.2010.10.002
Jan Johannsen
3
Während das Papier von Beame et al. verknüpft von Radu Grigore zeigt, dass die allgemeine Auflösung von einem DPLL-Algorithmus mit einer bestimmten, künstlichen Lernstrategie p-simuliert wird. Das obige Papier zeigt sie für natürliche Lernstrategien, die tatsächlich verwendet werden.
Jan Johannsen,
12

Die Umfrageausbreitung ist ein weiterer Algorithmus, der bei einigen Arten von SAT-Problemen, insbesondere bei zufälligen SAT-Instanzen, erfolgreich eingesetzt wurde. Wie WalkSAT kann es nicht verwendet werden, um Unzufriedenheit zu beweisen, aber es basiert auf sehr unterschiedlichen Ideen (Message-Passing-Algorithmen) von WalkSAT.

Timothy Chow
quelle
10

Es gibt SAT-Löser, die auf der lokalen Suche basieren. Siehe zum Beispiel dieses Papier zur Erläuterung.

Ilyaraz
quelle
7

Man kann auch sagen, dass alle CSP-Löser auch SAT-Löser sind. Soweit ich weiß, werden im CSP zwei Methoden verwendet:

  • Umfassende DFS mit Beschneidung des Suchraums und Überprüfung der Bogenkonsistenz, möglicherweise mithilfe von Rasur, um sicherzustellen, dass die Konsistenz so schnell wie möglich erhalten bleibt.
  • Lokale Methoden (Tabusuche, simuliertes Tempern)
malejpavouk
quelle
4

Monte Carlo Tree Search (MCTS) hat kürzlich einige beeindruckende Ergebnisse bei Spielen wie Go erzielt. Die grobe Grundidee ist die Verschachtelung von Zufallssimulationen mit der Baumsuche. Es ist leicht und einfach zu implementieren. Die von mir verlinkte Research Hub-Seite enthält viele Beispiele, Artikel und auch Code.

Previti et al. [1] haben einige vorläufige Untersuchungen zu MCTS für SAT durchgeführt. Sie nennen den MCTS-basierten Suchalgorithmus UCTSAT ("Upper Confidence Bound auf Bäume SAT angewendet", wenn Sie so wollen). Sie verglichen die Leistung von DPLL und UCTSAT auf Instanzen aus dem SATLIB-Repository mit dem Ziel, festzustellen, ob UCTSAT signifikant kleinere Suchbäume als DPLL erzeugen würde.

Für einheitliche zufällige 3-SAT- und Flat-Graph-Färbungen unterschiedlicher Größe gab es keine signifikanten Unterschiede. UCTSAT schnitt jedoch in realen Situationen besser ab. Die durchschnittliche Baumgröße (in Bezug auf die Anzahl der Knoten) für vier verschiedene SSA-Fehleranalyseinstanzen lag bei DPLL bei mehreren Tausend, während sie bei UCTSAT immer unter 200 lag.

[1] Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf und Bart Selman. "Monte-Carlo-UCT-Suche nach boolescher Erfüllbarkeit." In AI * IA 2011: Künstliche Intelligenz um den Menschen und darüber hinaus, S. 177-188. Springer Berlin Heidelberg, 2011.

Juho
quelle
-4

DPLL spezifiziert die Reihenfolge der variablen Besuche nicht streng und es gibt eine Menge interessanter Untersuchungen, die sich mit optimalen Angriffsstrategien für die variable Reihenfolge befassen. Ein Teil davon ist in der Variablenauswahllogik von SAT-Algorithmen enthalten. In gewisser Hinsicht sind einige dieser Untersuchungen vorläufig, da sie zeigen, dass unterschiedliche variable Angriffsreihenfolgen zu unterschiedlicher sequentieller Beschränkung führen (die in hohem Maße mit der Instanzenhärte korreliert), und die effektivsten Heuristiken oder Strategien zu entwickeln scheinen, um diese anscheinend entscheidende Einsicht zu nutzen in den frühen Stadien der Forschung.

vzn
quelle
4
Verstehen Sie, dass ich nach Algorithmen gefragt habe , die nicht auf DPLL basieren ?
Anonym
2
Verstehst du, was "basiert" bedeutet? Ich habe dir gesagt : Benutze meine Fragen nicht, um zu kommentieren, worauf du Lust hast!
Anonym
7
Sie selbst sagen, dass sie DPLL-basiert sind. Für mich ist das so, als würde man sagen, dass verschiedene Pivot-Regeln für Simplex einen Algorithmus ergeben, der kein Simplex-Algorithmus ist
Sasho Nikolov,
7
Ich stimme Sasho zu. Auch die Forschung zu Heuristiken variabler Ordnung befindet sich definitiv nicht in einem frühen Stadium. Die Wichtigkeit wurde vor langer Zeit erkannt (stellen Sie sich die Folgen eines perfekten Orakels vor) und es wurde viel Zeit darauf verwendet, sie zu analysieren. Wert Bestell Heuristik interessanter geworden in CSP - Solver, und aus irgendeinem Grund, ich glaube nicht , die Forschung an ihnen war wie für variable Anordnung boomt.
Juho
4
Genauer gesagt geht die anfängliche Forschung zu Heuristiken variabler Ordnung auf die 70er Jahre zurück. Bei Interesse kann ich die relevanten Referenzen für Sie ausgraben.
Juho