Starten von SAT-Solver-Papieren

24

Ich möchte einen ersten SAT-Löser machen. Ich kenne den SAT-Wettbewerb und die SAT-Konferenz, und es gibt einfach so viele Artikel zu diesem Thema. Ich bin ein Starter, ein überwältigter Starter. Wo soll ich anfangen Schließlich möchte ich den Stand der Technik vorantreiben. Ich möchte einen kompetenten Rat, wie ich anfangen soll, damit ich meine Zeit nicht zu früh auf das Nötigste verschwenden kann. Danke vielmals.

Zirui Wang
quelle
6
Haben Sie den DPLL-Algorithmus bereits implementiert? Haben Sie Ihre Implementierung so optimiert und poliert, dass sie extrem schnell läuft?
Jukka Suomela
5
The Handbook of Satisfiability - amazon.co.uk/… (vielleicht in einer Bibliothek nachsehen , die Kosten sind ziemlich hoch).
MGwynne
1
@Jukka: Kommentar -> Antwort?
Suresh Venkat
4
Ich bin mit Jukka nicht einverstanden. Warum das Rad neu erfinden? Es gibt keinen Grund, das, was MiniSAT bereits als Open Source anbietet, zu wiederholen. Wenn Sie an einer Erweiterung des CDCL-Frameworks interessiert sind, zeigt sich Ihre Erweiterung in einer gesteigerten MiniSAT-Leistung. Auch DPLL allein reicht nicht aus. Es wurden viele Verbesserungen vorgenommen. Grundsätzlich folge Mikolas Antwort!
Huck Bennett
1
Siehe auch verwandte Frage cstheory.stackexchange.com/q/1988
András Salamon

Antworten:

18

Einen hervorragenden Einsteigerüberblick gibt der folgende Artikel aus dem Jahr 2009.

Es gibt verschiedene Möglichkeiten, in die technischen Aspekte einzusteigen. Sie können sogar mit dem Originalpapier von Davis-Putnam beginnen. Es ist sehr klar und hat detaillierte Beispiele. Als wir in einem Kurs über SAT-Optimierungen diskutierten, stellten wir fest, dass einige davon möglicherweise bereits vorhanden sind. Die Davis-Logeman-Loveland-Zeitung ist (meiner Meinung nach) weniger aufschlussreich, aber sie ist so kurz, dass Sie sie genauso gut lesen können.

Es gibt möglicherweise Möglichkeiten, sich über die Entwicklungen der nächsten 50 Jahre zu informieren. Ich würde Vorlesungsfolien empfehlen. Wenn Sie nur nach 'DPLL' suchen, werden viele Tutorials angezeigt. Wenn Sie sie durchblättern, wird sich der Nebel sicher auflösen - bis zu einem gewissen Grad. Es gibt auch viele nützliche Umfragen. Die Zhang-Malik-Zeitung ist ein guter Anfang. Das Handbuch der Zufriedenheit enthält mehrere Artikel, die Sie möglicherweise nützlich finden.

Ich unterstütze den Vorschlag von Mikolaos. Der MiniSAT-Code ist sauber und überschaubar. Sie können damit spielen. Es gibt mehrere andere Löser, die Sie ausprobieren können. CryptoMiniSat ist auch ziemlich sauber. Sie sollten auch die Arbeit von Armin Biere konsultieren , der SAT-Löser schreibt und über das Schreiben von SAT-Lösern schreibt.

Vijay D
quelle
17

Ich schlage vor, zunächst zu verstehen, mit welchen Techniken die Löser wirklich fortgeschritten sind. Für diese Techniken würde ich die folgende Übersicht und Analyse vorschlagen .

Dann würde ich empfehlen, den Quellcode von minisat herunterzuladen und dessen Beschreibung zu lesen .

Es mag natürlich individuell sein, aber ich fand es am wertvollsten, den Quellcode zu betrachten.

Mikolas
quelle
9

Wenn Sie von all der Arbeit, die es gibt, überwältigt sind, warum geben Sie dann nicht vor, dass noch niemand an dem Problem gearbeitet hat? Wenn es Ihr Ziel ist, irgendwann einen wettbewerbsfähigen SAT-Löser zu entwickeln, ist der Weg ziemlich lang. Wenn Sie anfangen, nur herumzuspielen, ohne die Lösungen zu überprüfen, haben Sie mehr zu gewinnen als zu verlieren.

nmnm

nm

James King
quelle
9

Beginnen Sie mit einem guten Umfragepapier. Es ist leicht, das Thema Stück für Stück anzugreifen und durch verschiedene Namen in der Literatur für die gleichen Techniken und den gleichen Namen für verschiedene Techniken verwirrt zu werden. Es ist auch einfach, alte algorithmische Schlachten nachzustellen (Ereignislisten vs. Kopf-Schwanz-Listen vs. zwei beobachtete Literale für DPLL-Implementierungen zum Beispiel), wenn Sie nicht wissen, wie der Stand der Technik ist.

Satisfiability Solvers von Gomes et al . al. wird dir die raue Lage des Landes geben.

Die Verbesserung von SAT-Solvern mithilfe modernster Manthey -Techniken bringt Sie der Gegenwart näher.

Kyle Jones
quelle