Vorschlag eines effizienten SAT-Lösers mit guter C++ - Schnittstelle (oder: ist Z3 gut für mich)?

Question

Für ein Projekt, das ich beginne, muss ich einen SAT-Löser verwenden. Ich habe einige von ihnen schon früher benutzt, aber hauptsächlich zum Experimentieren, während hier das Haupthindernis für das Projekt eine gute Leistung ist. Ich versuche, nach Alternativen zu suchen und zu versuchen, zu verstehen, wie jede Alternative in Bezug auf meine spezifischen Anforderungen positioniert ist. Insbesondere gilt Folgendes:

1. Ich werde die erfüllenden Belegungen extrahieren müssen, nicht nur für die Erfüllbarkeit überprüft, und sollte der Solver gestatten Sie mir die gleiche Formel wiederholt zu lösen für verschiedene mögliche erfüllenden Belegungen suchen, schließlich iterieren alle sie, in einer effizienten Art und Weise (zB ohne dass ich eine Klausel hinzufügen und von vorne beginnen muss).

2. Das Projekt sollte noch aktiv gepflegt werden und faire Produktionsqualität, nicht einige Wettbewerb gewonnene Forschungsprojekt seit der Veröffentlichung aufgegeben (siehe picosat).

3. Außerdem, da ich C++ verwende, sollte der Löser eine effiziente und (möglicherweise) gut geschriebene C++ - Schnittstelle bieten.

Der erste Kandidat war ich Z3 betrachtet, aber ich bin durch die docs verwirrt und kann nicht verstehen, wenn Punkt 1 oben unterstützt wird, und wenn es übertrieben gegeben werden könnte, dass ich brauche SAT nur und nicht SMT. Die C++ - Schnittstelle scheint auch sehr einfach zu sein, aber ich kann es nicht ertragen, dass ich die Variablen mit einfachen Strings benennen muss (das paßt sehr schlecht zu meinem umgebenden Algorithmus. Ist das nicht vermeidbar?).

Also können Sie mir einen Vorschlag geben, welchen SAT-Löser Sie verwenden sollen, oder sich durch Zweifel an Z3 ein wenig Licht machen?

Answer 1

Wenn Sie bereit sind, etwas Arbeit in das Reparieren von Build für verschiedene Plattformen zu stecken (oder überhaupt nicht benötigen), beachten Sie, dass es jedoch nicht mehr wirklich gepflegt wird.

Es gibt auch Glucose, die MiniSat-Schnittstelle teilt und relativ aktiv gepflegt wird. Bei SAT-Wettbewerben ist es auch viel besser als MiniSat.

Bevor Sie das eine oder andere auswählen, müssen Sie verstehen, dass, während Glukose im Allgemeinen über MiniSat in SAT-Wettbewerben gewinnt, Ihr Anwendungsfall SAT-Wettbewerbe möglicherweise nicht löst. Als ein Beispiel erzeugt unser Projekt im Allgemeinen erfüllbare Formeln, wobei die Aufgabe darin besteht, eine von (gewöhnlich) vielen SAT-Zuordnungen zu finden, und MiniSat dort in der Regel Glucose übertrifft. OTOH Wenn Ihr Projekt meistens unerfüllbare Formeln oder Formeln mit einer einzigen gefundenen Lösung generiert, wird Glucose wahrscheinlich besser sein, da es für das schnelle Auffinden von UNSAT-Proofs optimiert ist, anstatt SAT-Zuordnungen zu finden.

Ein weiterer Löser, den ich mit der Einbettung Erfahrung hatte, ist CryptoMiniSat. Es hat eine vernünftige C++ - Schnittstelle und wird sehr aktiv gepflegt. Wenn ich ein Problem oder einen Fehler hatte, wurde es normalerweise innerhalb einer Woche behoben. Allerdings bietet es nur selten stabile Versionen. Wenn Sie es also verwenden, werden Sie wahrscheinlich eher von einem bestimmten Hash als von einer richtigen Version leben.

Noch eine Anmerkung: Glucose bietet einen parallelen Löser, aber mit einer ziemlich interessanten Lizenz. CMSat bietet parallele Löser unter MIT-Lizenz. MiniSat hat eine sehr liberale Lizenz, aber keine parallele Option.