Führen Sie alle Lösungen eines SAT-Problems auf

11

Alle mir bekannten # SAT-Löser, z. B. RelSat, C2D, geben nur die Anzahl der erfüllbaren Instanzen zurück. Aber ich möchte jede dieser Instanzen kennen?

Gibt es einen solchen # SAT-Solver oder wie sollte ich einen verfügbaren # SAT-Solver ändern, um dies zu tun?

Vielen Dank.

lo.logic sat software qsp
quelle
7
Dies wird oft als "SAT-Löser für alle Lösungen" bezeichnet, scheint jedoch nicht von der Stange zu sein. Die Referenzen, die ich finden kann, beziehen sich auf Änderungen an MiniSAT und anderen Lösern, normalerweise durch Hinzufügen von Blockierungsklauseln, um eine Lösung auszuschließen, wenn sie gefunden wird. Auf der anderen Seite unterstützen die meisten Constraint Solver die generierte Generierung aller Lösungen.
András Salamon
Ein Ansatz ist eine CNF → DNF-Konvertierung, für die es viel Literatur gibt
vzn

Antworten:

13

Sie suchen einen SAT-Löser für ALL-SAT oder alle Lösungen. Dies ist ein anderes Problem als #SAT. Sie müssen nicht alle Lösungen aufzählen, um sie zu zählen.

Ich kenne kein Tool, das Ihr Problem löst, da die Leute diese Algorithmen zusätzlich zu vorhandenen SAT-Solvern hinzufügen, diese Erweiterungen jedoch selten zu veröffentlichen scheinen. Im Folgenden finden Sie zwei Artikel, die Ihnen beim Ändern eines CDCL-Lösers zur Implementierung von ALL-SAT helfen sollen.

Speichereffizienter SAT-Löser für alle Lösungen und seine Anwendung auf die Erreichbarkeit , O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004

Hier ist ein kürzlich veröffentlichter Artikel über arXiv.

Erweiterung moderner SAT-Löser zur Aufzählung aller Modelle , Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013

Sie können versuchen, diese Autoren für ihre Implementierung zu kontaktieren.

Vijay D.
quelle
Für das zweite Papier müssen Sie nur auf die erste Version v1 klicken, um sie anzuzeigen.
Tayfun Pay
Dieses aktuelle Papier scheint verwandt zu sein: Homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf
Kaveh
1
@Kaveh, ich glaube, das OP fragt nach einem ALLSAT-Solver oder nach einer Möglichkeit, einen # SAT-Solver in einen ALLSAT-Solver zu verwandeln. Dies ist ein Artikel über Untergrenzen für #SAT. Ich bin nicht sicher, ob es dem OP hilft.
Vijay D
2

Ich habe auf einer VLSI-Konferenz ein neueres (2014) Papier über All-SAT gefunden, das sich also definitiv an der praktischen Seite orientiert (was hier im Einklang mit der Frage des OP zu stehen scheint, wenn auch weniger mit cstheory.SE im Allgemeinen):

  • "All-SAT unter Verwendung minimaler Blockierungsklauseln" von Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik und VLSI Design 2014. doi: 10.1109 / VLSID.2014.22 .

Für diejenigen ohne IEEE-Abonnement gibt es eine kostenlose Kopie auf der Princeton-Webseite von Subramanyan . (Er verwendet einen Filesharing-Dienst, um Kopien seiner Papiere zu speichern / zu verteilen, und ich bin mir nicht sicher, wie stabil diese URLs sind, daher dieser Kreisverkehr-Link.)

Der Kern dieses Papiers scheint zu sein:

Unser Beitrag, der Non-Disjoint-Dec-Algorithmus, generiert extrem kurze Blockierungsklauseln, die keine der implizierten Variablen im Solver enthalten. Beachten Sie, dass normalerweise die Mehrheit der Variablen in einem zufriedenstellenden Zeitraum impliziert ist. Kurze Blockierungsklauseln sind für die Leistung des Lösers sehr vorteilhaft, wie die Bewertung zeigt.

Ihre Implementierung baut auf MiniSat auf. Der Quellcode für ihre Erweiterung scheint jedoch nicht öffentlich verfügbar zu sein. Leider scheint dies eine Gewohnheit auf dem Gebiet von All-SAT zu sein, so dass Papiere in diesem Bereich, die experimentelle Ergebnisse enthalten, nur einen mehr oder weniger einfach zu schlagenden Strohmann-Algorithmus aufstellen und selten direkt verglichen werden können (experimentell) Ergebnisse) mit jedem anderen veröffentlichten Algorithmus für All-SAT. Das Papier von Jabbour et al. von Vijay D erwähnt ist auch von dieser Art.

Da ich es in der anderen Antwort nicht erwähnt sehe (aber nur im Kommentar von András Salamon), wurde die [ziemlich beliebte] Sperrklausel-Technik eingeführt in:

Fizz
quelle