Ich untersuche verschiedene SAT-Löser und versuche zu verstehen, wie sie funktionieren und warum sie auf bestimmte Weise entworfen wurden. (Aber ich bin im Moment nicht an einer Universität und kenne niemanden, der Professor ist. Also poste ich hier in der Hoffnung, dass mir jemand helfen kann. Ich würde es wirklich schätzen.)
In Chaff wird BCP (Boolean Constraint Propagation) anders als die ursprüngliche DPLL implementiert : Es werden zwei Literale gleichzeitig betrachtet (eine Technik, die sich geringfügig von der ursprünglich in SATO: An Efficient Propositional Prover vorgeschlagenen unterscheidet ). Spreu: Entwicklung eines effizienten SAT-Lösers . In diesem Artikel wird jedoch keine reine wörtliche Eliminierung erwähnt.
In Die Komplexität der reinen wörtlichen Eliminierung schrieb Jan Johannsen
Die derzeit besten Implementierungen von DLL-SAT-Solvern wie Chaff oder BerkMin opfern diese Heuristik, um die Effizienz der Einheitenausbreitung zu steigern.
wobei "diese Heuristik" sich auf die reine wörtliche Eliminierung bezieht. Mein Verständnis dessen, was reine wörtliche Eliminierung bewirkt, ist, dass es
- sucht nach allen einpolaren (oder reinen) Literalen
- weist ihnen einen booleschen Wert zu, so dass jeder ergibt
True - In diesem Fall können wir jetzt alle Klauseln löschen, die sie enthalten
Hier ist meine Frage:
Wie ist das Opfer notwendig? Gibt es einen guten Grund, warum es in DPLL-basierten Algorithmen wie Chaff keine reine wörtliche Eliminierung gibt? Können wir nicht einfach in jeder Entscheidungsebene eine reine wörtliche Eliminierung durchführen (oder zumindest zu Beginn vor der Verzweigung)?
quelle
Antworten:
Löser, die den Zwei-Beobachtungs-Literal-Algorithmus verwenden, um die Einheitenausbreitung zu implementieren, verfolgen nicht, welche Klauseln (implizit) gelöscht wurden, um die durch die aktuelle Teilzuweisung implizierte Unterformel zu erzeugen. Wenn Solver diese Informationen nicht nachverfolgen, können sie vermeiden, die meisten Klauseln während der Zuweisung zu berühren und keine der Klauseln während des Zurückverfolgens zu berühren . Um herauszufinden, welche Variablen derzeit in der Formel rein sind, müssen diese erheblichen Effizienzgewinne verloren gehen. In der Zwischenzeit deutet nichts darauf hin, dass eine reine wörtliche Entfernung zu Konflikten führt oder Aufgaben früh genug erfüllt, um die hohen Kosten für die Nachverfolgung auszugleichen.
Löser, die vor dem Starten des Suchvorgangs eine Formelvereinfachung durchführen, umfassen im Allgemeinen die reine Literalentfernung, da dies als Vorverarbeitungsschritt recht billig ist und möglicherweise viele Klauseln entfernen kann.
quelle