gophersat
1.0.0
Dies ist Gophersat, ein rein in Go geschriebener SAT- und Pseudo-Boolean-Löser. Gophersat wurde vom CRIL (Centre de Recherche en Informatique de Lens) an der Artois University & CNRS entwickelt. Es wird unter der MIT-Lizenz veröffentlicht. Gophersat ist ziemlich effizient, dh bei typischen SAT-Benchmarks läuft es etwa zwei- bis fünfmal langsamer als Solver der Spitzenklasse (nämlich Glucose oder Minisat), von denen es stark inspiriert ist. Es kann auch MAXSAT-Probleme sowie pseudo-boolesche Entscheidungs- und Optimierungsprobleme lösen.
Die letzte stabile Version von Gophersat ist Version 1.4. Es enthält die optionale Lösungsstrategie für Schnittebenen.
Bei manchen Problemen, wie zum Beispiel dem berühmten Schubladenproblem, dauert es sehr lange, sie mit rein logischem Denken zu lösen.
Das Taubenlochproblem kann folgendermaßen ausgedrückt werden: Ist es möglich, n Tauben in m Taubenlöcher zu stecken, wobei m = n-1 ist, ohne mehrere Tauben in dasselbe Loch zu stecken und alle Tauben in ein Loch zu stecken? Die Antwort liegt auf der Hand: Wenn Sie 4 Tauben in 3 Löchern haben, können Sie sie nicht alle in ein anderes Loch setzen. Aber wie beweist man das? Ein SAT- oder PB-Löser beweist dies, indem er alle möglichen Kombinationen ausprobiert, und die Anzahl der möglichen Kombinationen wächst exponentiell. Daher ist der Versuch, das Problem mit n=20 zu lösen, in der Praxis nicht durchführbar, obwohl es für das Problem eine offensichtliche Antwort gibt.
Einige PB-Löser implementieren eine alternative Strategie: die Schnittebenen-Strategie. Es wird in diesem Dokument nicht im Detail beschrieben, aber diese Strategie kann bei einigen Problemen äußerst effizient sein, wie zum Beispiel beim Schubladenproblem, das nicht effizient durch rein logisches Denken gelöst werden kann, bei den meisten Problemen jedoch langsamer ist.
Es ist jetzt möglich, die Schnittebenen mit Gophersat zu verwenden. Verwenden Sie einfach die Befehlszeilenoption -cp . Anstatt also anzurufen:
gophersat problem.opb
Rufen Sie einfach an:
gophersat -cp problem.opb
Die letzte stabile Version von Gophersat ist Version 1.3. Es handelt sich um ein kleines Update, das die Möglichkeit bietet, bei der Bearbeitung von MAXSAT-Problemen auf den zugrunde liegenden Solver zuzugreifen.
Gophersat Version 1.2 bietet eine Möglichkeit, UNSAT-Instanzen zu verstehen, sowohl durch die Bereitstellung von RUP-Zertifikaten, wenn ein Problem UNSAT ist, als auch durch die Möglichkeit, nicht erfüllbare Teilmengen der Formel zu extrahieren. Außerdem wurden einige Fehler behoben und die Unterstützung für die inkrementelle SAT-Lösung verbessert.
Um mehr über diese Funktionen zu erfahren, können Sie sich das Tutorial zu UNSAT-Zertifikaten und MUSes ansehen.
Um ein Zertifikat mit der ausführbaren Gophersat-Datei zu generieren, rufen Sie einfach Folgendes auf:
gophersat -certified problem.cnf
Das Zertifikat wird dann auf der Standardausgabe in der RUP-Notation ausgedruckt. Das Zertifikat wird im Handumdrehen generiert. Beachten Sie daher, dass ein teilweises, nutzloses Zertifikat generiert wird, selbst wenn das Problem tatsächlich behebbar ist. Dies ist in der Community gängige Praxis, und obwohl die generierten Klauseln nutzloser Lärm sind, stellt dies in der Praxis kein Problem dar.
Um einen MUS aus einer UNSAT-Instanz zu extrahieren, rufen Sie einfach Folgendes auf:
gophersat -mus problem.cnf
Der MUS wird dann auf der Standardausgabe gedruckt. Wenn das Problem nicht UNSAT ist, wird eine Fehlermeldung angezeigt.
Im Moment stehen diese Funktionen nur für reine SAT-Probleme (also nicht für pseudo-boolesche Probleme) zur Verfügung.
Seit seiner Version 1.1 enthält Gophersat einen neuen, effizienteren Kernlöser für reine SAT-Probleme und ein Paket für MAXSAT-Probleme. Es enthält außerdem eine neue API zur Optimierung und Modellzählung, bei der neue Modelle in Kanäle geschrieben werden, sobald sie gefunden werden.
Seit Version 1.0 gilt die API von Gophersat als stabil, was bedeutet, dass die API bis zu einem größeren Versionswechsel garantiert abwärtskompatibel bleibt. Mit anderen Worten: Wenn Ihr Programm mit Version 1.0 von Gophersat funktioniert, funktioniert es immer noch mit Version 1.1 oder höher, aber nicht unbedingt mit Versionen über 2.0.
Beachten Sie, dass wir mit „funktioniert immer noch“ nur „wird kompiliert und die gleiche Ausgabe erzeugen“ meinen, nicht „wird in Bezug auf Speicher oder Zeit die gleiche Leistung erbringen“. Dies ist ein wichtiger Unterschied: Bei kleineren Versions-Upgrades können neue Heuristiken oder Datentypen eingeführt werden, was bedeutet, dass bestimmte Probleme schneller oder langsamer als zuvor gelöst werden können.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat kann als eigenständiger Solver (zum Lesen von DIMACS CNF-Dateien) oder als Bibliothek in jedem Go-Programm verwendet werden.
Um eine DIMACS-Datei zu lösen, können Sie gophersat mit der folgenden Syntax aufrufen:
gophersat --verbose file.cnf
Dabei ist --verbose ein optionaler Parameter, der dafür sorgt, dass der Löser während des Lösungsprozesses Informationen anzeigt.
Gophersat ist auch in der Lage, allgemeinere boolesche Formeln zu lesen und zu lösen, nicht nur Probleme, die im benutzerfreundlichen DIMACS-Format dargestellt werden. Es befasst sich auch nativ mit Kardinalitätsbeschränkungen, d. h. Klauseln, die mindestens n Literale wahr haben müssen, mit n > 1.
Gophersat kann als eigenständiger Solver (Lesen von OPB-Dateien) oder als Bibliothek in jedem Go-Programm verwendet werden.
Um ein pseudoboolesches Problem (sei es ein Entscheidungs- oder ein Optimierungsproblem) zu lösen, können Sie gophersat mit der folgenden Syntax aufrufen:
gophersat --verbose file.opb
Dabei ist --verbose ein optionaler Parameter, der dafür sorgt, dass der Löser während des Lösungsprozesses Informationen anzeigt.
Im Moment kann es nur die sogenannten DEC-SMALLINT-LIN-Probleme und OPT-SMALLINT-LIN lösen, also Entscheidungsprobleme (gibt es eine Lösung oder nicht) für lineare Einschränkungen (eine Summe gewichteter Literale) auf kleine ganze Zahlen (n < 2^30) oder Optimierungsprobleme (was ist die beste Lösung, Minimierung einer gegebenen Kostenfunktion) für lineare Einschränkungen für kleine ganze Zahlen.
Dank des maxsat Pakets kann Gophersat nun MAXSAT-Probleme lösen.
Um ein gewichtetes MAXSAT-Problem zu lösen, können Sie gophersat mit der folgenden Syntax aufrufen:
gophersat --verbose file.wcnf
Dabei ist --verbose ein optionaler Parameter, der dafür sorgt, dass der Löser während des Lösungsprozesses Informationen anzeigt. Die Datei soll im (WCNF-Format)[http://www.maxsat.udl.cat/08/index.php?disp=requirements] dargestellt werden.
SAT, das für Boolean Satisfiability Problem steht, ist das kanonische NP-vollständige Problem, also ein Problem, für das es keine bekannte Lösung gibt, das im schlimmsten Fall keine exponentielle Zeit benötigt. Kurz gesagt: Ein SAT-Löser versucht, für eine gegebene Aussagenformel eine Zuweisung für alle ihre Variablen zu finden, die sie wahr macht, sofern eine solche Zuweisung existiert.
Während es trivial ist, einen SAT-Löser mithilfe eines naiven Algorithmus zu implementieren, wäre eine solche Implementierung in der Praxis sehr ineffizient. Gophersat implementiert modernste Funktionen und ist daher recht effizient, sodass es in der Praxis in Go-Programmen einsetzbar ist, die eine effiziente Inferenz-Engine benötigen.
Obwohl dies aus praktischen Gründen nicht immer die beste Entscheidung ist, kann jedes NP-vollständige Problem als SAT-Problem übersetzt und von Gophersat gelöst werden. Zu diesen Problemen gehören das Traveling Salesman Problem, die Constraint-Programmierung, das Knapsack-Problem, die Planung, die Modellprüfung, die Software-Korrektheitsprüfung usw.
Mehr zum SAT-Problem finden Sie im Wikipedia-Artikel über SAT.
Informationen darüber, wie Sie Ihre eigenen booleschen Formeln darstellen, damit sie von Gophersat verwendet werden können, finden Sie auch im Tutorial „SAT für Noobs“.
MAXSAT ist das Optimierungsäquivalent des SAT-Entscheidungsproblems. Während ein reiner SAT-Löser entweder ein Modell zurückgibt, das alle Klauseln erfüllt, oder UNSAT, wenn kein solches Modell existiert, gibt ein MAXSAT-Löser ein Modell zurück, das so viele Klauseln wie möglich erfüllt.
Es gibt Erweiterungen zu MAXSAT.
Teilweiser MAXSAT bedeutet, dass, obwohl wir so viele Klauseln wie möglich erfüllen wollen, einige Klauseln (sogenannte harte Klauseln ) erfüllt sein müssen , egal was passiert. Ein partielles MAXSAT-Problem kann somit für unerfüllbar erklärt werden.
Beispielsweise ist die Erstellung eines Stundenplans für eine Schule ein Teilproblem von MAXSAT: Es gibt sowohl weiche (wir wollen zum Beispiel so wenig Unterricht wie möglich haben, die nach 16 Uhr beginnen) als auch harte (zwei Lehrer können nicht an zwei verschiedenen Orten sein). gleichzeitig) Einschränkungen.
Gewichteter MAXSAT bedeutet, dass Klauseln mit Kosten verbunden sind: Obwohl optional, werden einige Klauseln als wichtiger erachtet als andere. Wenn beispielsweise Klausel C1 Kosten von 3 hat und Klauseln C2 und C3 beide Kosten von 1 haben, wird eine Lösung, die C1, aber weder C2 noch C3 erfüllt, als besser angesehen als eine Lösung, die sowohl C2 als auch C3, aber nicht C1, alle anderen erfüllt die Dinge sind gleich.
Teilgewichteter MAXSAT bedeutet, dass das Problem sowohl weiche als auch harte Klauseln enthält und weiche Klauseln gewichtet sind. In dieser Hinsicht ist „reines“ MAXSAT ein Sonderfall des allgemeineren teilweise gewichteten MAXSAT: Ein „reines“ MAXSAT-Problem ist ein teilweise gewichtetes MAXSAT-Problem, bei dem alle Klauseln weiche Klauseln sind, die einer Gewichtung von 1 zugeordnet sind.
Pseudo-boolesche Probleme sind in gewisser Weise eine Verallgemeinerung von SAT-Problemen: Jeder Satzsatz kann als einzelne pseudo-boolesche Einschränkung geschrieben werden, aber die Darstellung einer pseudo-booleschen Einschränkung kann eine exponentielle Anzahl von Satzsätzen erfordern.
Ein (linearer) pseudoboolescher Ausdruck ist ein Ausdruck wie:
w1 l1 + w2 x2 + ... + wn xn ≥ y
Dabei sind y und alle wi ganzzahlige Konstanten und alle li boolesche Literale.
Beispielsweise, dass der folgende Ausdruck wahr ist
2 ¬x1 + x2 + x3 ≥ 3
Die boolesche Variable x1 muss falsch sein und mindestens eine der Variablen x2 und x3 muss wahr sein. Dies entspricht der Satzformel
¬x1 ∧ (x2 ∨ x3)
Pseudoboolesche Ausdrücke sind eine Verallgemeinerung von Satzsätzen: jeder Satz
x1 ∨ x2 ∨ ... ∨ xn
kann umgeschrieben werden als
x1 + x2 + ... + xn ≥ 1
Die Beschreibung eines pseudo-booleschen Problems kann exponentiell kleiner sein als die seines propositionalen Gegenstücks, aber die Lösung eines pseudo-booleschen Problems ist immer noch NP-vollständig.
Gophersat löst sowohl Entscheidungsprobleme (gibt es überhaupt eine Lösung für das Problem) als auch Optimierungsprobleme. Ein Optimierungsproblem ist ein pseudoboolesches Problem, das mit einer Kostenfunktion verknüpft ist, also einer Summe von Termen, die minimiert werden müssen. Anstatt nur zu versuchen, ein Modell zu finden, das die gegebenen Einschränkungen erfüllt, wird gophersat dann versuchen, ein Modell zu finden, das garantiert sowohl die Einschränkungen erfüllt als auch die Kostenfunktion minimiert.
Während der Suche nach diesen optimalen Lösungen stellt Gophersat suboptimale Lösungen bereit (d. h. Lösungen, die alle Einschränkungen lösen, aber noch nicht garantiert optimal sind), sobald es sie findet, sodass der Benutzer in einer bestimmten Zeit entweder eine suboptimale Lösung erhalten kann begrenzen oder länger auf die garantiert optimale Lösung warten.
Jein. Es ist viel schneller als naive Implementierungen, schnell genug, um für reale Probleme verwendet zu werden, aber langsamer als hochoptimierte Spitzenlöser auf dem neuesten Stand der Technik.
Gophersat hat nicht das Ziel, der schnellste verfügbare SAT/PB-Löser zu sein. Ziel ist es, Gophern Zugriff auf SAT- und PB-Technologien zu ermöglichen, ohne auf Schnittstellen zu Lösern zurückgreifen zu müssen, die in anderen Sprachen (normalerweise C/C++) geschrieben sind.
In manchen Fällen ist jedoch die Schnittstelle zu einem in einer anderen Sprache geschriebenen Solver die beste Wahl für Ihre Anwendung. Wenn Sie viele kleine Probleme lösen müssen, ist Gophersat die schnellste Alternative. Bei größeren Problemen, wenn Sie auf Kosten der Lösungszeit möglichst wenig Abhängigkeiten haben möchten, ist Gophersat ebenfalls gut geeignet. Wenn Sie schwierige Probleme lösen müssen und kein Problem damit haben, cgo oder ein externes Programm zu verwenden, ist Gophersat wahrscheinlich nicht die beste Option.
Es gibt noch einige andere SAT-Löser in Go, hauptsächlich Go-Sat und Gini. Die Leistung von Gini ist der von Gophersat ziemlich ebenbürtig, wenn auch laut den von uns durchgeführten Tests im Durchschnitt etwas langsamer.
Gophersat bietet auch coole Funktionen, die bei anderen Lösern nicht immer verfügbar sind (z. B. ein benutzerfreundliches Eingabeformat), sodass es als Werkzeug zur Beschreibung und Lösung NP-schwerer Probleme verwendet werden kann, die leicht auf ein SAT/PB reduziert werden können Problem.
Nein. Das bf Paket (für „boolesche Formel“) bietet die Möglichkeit, beliebige boolesche Formeln in CNF zu übersetzen.
Dies wird als Modellzählung bezeichnet, und ja, dafür gibt es eine Funktion: solver.Solver.CountModels .
Sie können Modelle auch über die Befehlszeile zählen
gophersat --count filename
Dabei kann der Dateiname eine .opb- oder eine .cnf-Datei sein.
