#SAT Solver herunterladen

21

Könnte jemand bitte auf eine oder mehrere Websites verweisen, auf denen eine funktionierende Implementierung eines #SAT-Lösers heruntergeladen werden kann? Mich interessieren diejenigen, die die genaue Anzahl der Lösungen zurückgeben, keine Annäherung.

ds.algorithms sat software Giorgio Camerani
quelle
2
Hallo Walter, deine Frage steht kurz vor der Grenze zu dem, was für diese Site offiziell "zum Thema" wäre. Wenn Sie diese Frage jedoch nirgendwo anders stellen können und wir sie beantworten können, ist sie vielleicht nicht so schlimm ... (Da sich die Site noch in der Entwicklung befindet, sind wir offener als andere Sites.) Seien Sie versichert Dass der Sinn dieses Kommentars nicht darin besteht, "zu schelten" oder "zu warnen", ist nur ein freundlicher Hinweis.
Ryan Williams
Hallo Ryan, danke für deine Nachricht. Es tut mir leid, wenn diese Frage in der Nähe der Grenze ist. Ich habe im Internet gesucht und nichts gefunden: nur einige SAT-Löser, aber keine # SAT-Löser. Deshalb habe ich hier gefragt. Natürlich weiß ich, dass ich meinen eigenen Code schreiben kann, der einen SAT-Löser als Engine zum Zählen von Lösungen verwendet, aber ich habe nach etwas gesucht, das bereits erstellt und einsatzbereit ist.
Giorgio Camerani
12
Ich möchte nicht zustimmen. Ich denke, solche Fragen liegen im Rahmen und sollten es auch sein!
Suresh Venkat
Ich stimme dem Umfang zu. Zu Ihrer Information, es ist nicht zu praktisch, einen # SAT-Solver aus einem SAT-Solver zu erstellen, es sei denn, man hat den Quellcode und selbst in diesem Fall ist es nicht so praktisch, mit Ausnahme von sehr kleinen Formeln, da es zu einer sehr schlechten exponentiellen Explosion kommt. normalerweise sind spezielle Techniken erforderlich, die nur für #SAT und nicht für SAT gelten ...
vzn

Antworten:

16

Sie können dies mit SAT4J tun , indem Sie einfach alle Modelle durchlaufen : http://www.sat4j.org/howto.php#models . Ich stelle mir vor, dass die meisten SAT-Löser diese Fähigkeit haben.

Dave Clarke
quelle
Hallo supercooldave, danke für deinen Hinweis. Ich wusste nicht, dass SAT4J diese Fähigkeit besitzt.
Giorgio Camerani
16

Sie können auch den #SAT-Solver "sharpSAT" ( Website , Github ) verwenden, um die Anzahl der erfüllenden Zuordnungen von CNF-Formeln zu ermitteln.

Holger
quelle
11

Eine Möglichkeit besteht darin, eine BDD-Bibliothek wie JavaBDD zu verwenden . Alle diese Bibliotheken haben entweder eine Funktion, die Lösungen schnell zählt, oder sie machen es zumindest einfach, eine solche Funktion zu schreiben. Der Nachteil ist jedoch, dass das Erstellen der BDD in vielen Fällen langsam ist und möglicherweise viel Speicher benötigt.

mnO(mn)∼m+n

Radu GRIGore
quelle
7

Verwandte Themen: Bester SAT-Solver .

MS Dousti
quelle
1
Vielen Dank, Sadeq. Das von Ihnen angegebene Thema scheint theoretisch orientiert zu sein. Es werden mehrere Artikel zum Verringern der Obergrenze aufgelistet. Es ist sehr interessant, aber ich habe nach einer gebrauchsfertigen Implementierung gesucht.
Giorgio Camerani
2
Sie sind herzlich willkommen. Unter den dort genannten Links gab es einen rein praktischen: satcompetition.org . Ich denke, Sie können dort sehr gute Implementierungen finden.
MS Dousti
7

Das beste was ich gefunden habe ist "c2d compiler". http://reasoning.cs.ucla.edu/c2d/

Es wird d-DNNF verwendet und Sie benötigen die Option -count .

Leon Leon
quelle
c2d löst viel mehr CNFs als Sharpsat. Für Spielzeug Zwecke setzte sich der „relsat“ Löser auch tun wird.
Leon Leon
7

Der hier angegebene MBound Solver http://www.cs.cornell.edu/~sabhar/ kann Modellzählungen mit probabilistischen Garantien liefern. Es ist viel schneller als alle Lösungen aufzuzählen.

Opt
quelle
5

Ich habe einen kleinen Modell / Prime Implicant Enumerator geschrieben . Dies kann bereits für die Modellzählung mit der Modellaufzählung verwendet werden, aber das ist nicht sehr praktisch. Wenn irgendjemand Interesse hat, kann ich es erweitern, so dass es Modelle von Hauptimplikanten zählt.

Mikolas
quelle
2

Die Website BeyondNP enthält eine gute Bestandsaufnahme der vorhandenen Tools zur Lösung von #SAT (und anderer damit zusammenhängender schwerer Probleme bei CNF-Formeln). Möglicherweise finden Sie auch eine Liste von Tools für die ungefähre Modellzählung und Wissenskompilierung (die Aufgabe, den CNF in eine hoffentlich prägnante Datenstruktur umzuwandeln, die häufig die polynomiale Zeitmodellzählung unterstützt).

Unter Umständen finden Sie auch eine Liste von Tools für die Vorverarbeitung von CNF-Formeln, die hilfreich sein können, um die Leistung von Modellzählern und verschiedenen Benchmarks zu verbessern .

holf
quelle