Starten von SAT-Solver-Papieren

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.

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

• Boolesche Zufriedenheit: Von der theoretischen Härte zum praktischen Erfolg , Sharad Malik, Lintao Zhang, Mitteilungen der ACM, 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.

• Ein Rechenverfahren für die Quantifizierungstheorie , Martin Davis, Hilary Putnam, Zeitschrift der ACM, 1960.
• Ein Maschinenprogramm zum Beweis von Theoremen , Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.

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.

• Auf der Suche nach effizienten booleschen Lösern für die Zufriedenheit haben Lintao Zhang, Sharad Malik und Joint Paper für CAV und CADE 2002 eingeladen.
• Handbuch der Zufriedenheit , herausgegeben von Armin Biere, Marijn Heule, Hans van Maaren und Toby Walsh, 2009
• Anatomie und empirische Bewertung moderner SAT-Löser , Karem Sakallah, Joao Marques-Silva, Bulletin des EATCS, 2011.

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.

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.

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.

$n$$m$$n$$m$

$n$$m$

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.