Rezeptbuch für SAT-Kodierungen?

16

SAT-Löser lösen immer effizienter große Instanzen und werden in verschiedenen Zusammenhängen als Back-End eingesetzt. Jedes Mal, wenn jemand sie zur Lösung eines Problems in einem bestimmten Bereich verwenden möchte, muss er / sie eine Ad-hoc-Codierung entwickeln, die nicht nur die richtigen Lösungen bietet, sondern auch die Einschränkungen (auch überflüssig) in eine Form bringt Das hilft den Heuristiken der Löser dabei, eine Lösung schneller zu finden.

Viele solcher Kodierungen scheinen mir sehr verbreitet zu sein, zum Beispiel: Es wird behauptet, dass eine endliche Menge von Knoten als Baum oder als DAG verknüpft ist oder eine Liste sortiert ist ...

Gibt es ein Repository / Rezeptbuch mit allgemeinen Kodierungen für allgemeine Probleme mit optimierten Lösungen?

Bordaigorl
quelle
1. Diese Frage sieht sehr nützlich aus, kann aber auch über die Bühne gehen. Ich denke, es ist eine bessere Frage, wenn Sie sich auf eine einzelne Domain konzentrieren (ja, dies kann mehrere Fragen beinhalten, eine pro Domain - aber stellen Sie sicher, dass Sie einige Nachforschungen anstellen, bevor Sie uns fragen und zeigen, was Sie getan haben).
DW
2. Welche Nachforschungen haben Sie angestellt? Haben Sie sich SAT-Frontends wie STP, Alloy und Minion angesehen? Haben Sie sich cs.stackexchange.com/q/12087/755 , cs.stackexchange.com/q/13188/755 , cs.stackexchange.com/a/6522/755 , cs.stackexchange.com/a/12153/ angesehen ? 755 ? bei den fragen tagged sat-löser oder erfüllbarkeit ?
DW
Ja, die Frage ist vielleicht etwas weit gefasst. @DW danke für die Links, von denen einige direkt relevant sind. Ich hätte erwähnen sollen, dass ich weder an der Lösung eines bestimmten Problems noch an allgemeinen Methoden für effizientere Codierungen interessiert bin. Der Ausdruck "Best Practices", den ich verwendet habe, ist wahrscheinlich irreführend. Ich interessiere mich für ein Rezeptbuch =)
Bordaigorl
In Bezug auf den Bereich würde ich (Hyper-) Graphentheorie sagen, aber dies ist wahrscheinlich immer noch sehr weit
gefasst
Siehe auch verwandte Frage cs.stackexchange.com/q/12087
András Salamon

Antworten:

9

Ich habe vor einigen Jahren eine Umfrage gelesen, die relevant zu sein scheint: " Successful SAT Encoding Techniques " von Magnus Björk.

Abstrakt:

In diesem Artikel werden bewährte Verfahren für SAT-Codierungen anhand von Interviews mit einer Reihe bekannter SAT-Experten beschrieben. Ziel ist es, das Vertrauen in verschiedene Kodierungsstrategien zu bestimmen, indem analysiert wird, ob unter den Experten ein Konsens besteht oder nicht, und SAT-Benutzern verborgenes Wissen zugänglich zu machen.

Es besteht Konsens darüber, dass Codierungstechniken in der Regel einen dramatischen Einfluss auf die Effizienz des SAT-Lösers haben, dass die Suche nach einer guten Codierung häufig viel Arbeit erfordert und dass die Größe einer Codierung nur sehr wenig mit der Schwierigkeit zusammenhängt, eine Lösung zu finden . Zu den Themen, bei denen die Befragten anderer Meinung sind, gehört die Möglichkeit, Arithmetik in SAT-Probleme einzubeziehen und Probleme als Klauseln oder Schaltungen zu formulieren.

Der Artikel beschreibt eine Reihe von Strategien, die in verschiedenen Situationen nützlich sind, z. B. verschiedene Arten der Darstellung von Zahlen und die Verwendung von Inkrementalität.

Kyle Jones
quelle
4

Es ist immer eine gute Idee, zuerst das Handbuch der Zufriedenheit [1] zu lesen (ich denke, es ist nicht frei verfügbar, sorry). Hier trägt Kapitel 2 den Titel "CNF-Codierungen". Zumindest bietet das Buch Literaturhinweise zum Stand der Technik zum Zeitpunkt des Schreibens, und Sie können Ihre Suche durch sie erweitern.

Darüber hinaus finden Sie hier und hier zwei aktuelle Folien zur SAT-Vorverarbeitung. Die Folien geben einen kurzen Überblick über die Vorverarbeitungstechniken sowie weitere Referenzen. Die Idee ist, anstatt zu versuchen, das Problem auf effiziente Weise "manuell" zu modellieren, es einfach auf die einfachste Weise zu modellieren.


[1] Biere, Armin, Marijn Heule und Hans van Maaren, Hrsg. Handbuch der Erfüllbarkeit. Vol. 185. IOS Press, 2009.

Juho
quelle
3

Dies ist keine direkte Antwort, sondern ein immer enger verwandterer Aspekt: ​​Ein Teil davon wird durch ein relativ neues Forschungsgebiet abgedeckt, das als SMT, Satisfiability Modulo Theories, bekannt ist . Die Grundidee besteht darin, Problemkodierungen (z. B. Ganzzahlarithmetik, Diagramme usw.) in den SAT-Löser zu integrieren, aber auch das zusätzliche Wissen, das aus dieser Kopplung resultiert, zu nutzen, um fortschrittlichere Lösungsalgorithmen zu erstellen. Hier ist eine Umfrage. Wie bereits erwähnt, können sie wesentlich effizienter sein als die Kombination eines Ad-hoc-Codierungsmechanismus mit Standard-SAT-Lösern.

  • Satisfiability Modulo Theories: Ein Appetizer / Leonardo de Moura und Nikolaj Bjørner

    Modulo-Theorien zur Erfüllbarkeit (Satisfiability Modulo Theories, SMT) dienen der Überprüfung der Erfüllbarkeit logischer Formeln anhand einer oder mehrerer Theorien. Das Problem beruht auf einer Kombination einiger der grundlegendsten Bereiche der Informatik. Es kombiniert das Problem der Booleschen Erfüllbarkeit mit Domänen, wie sie in der konvexen Optimierung und der Manipulation symbolischer Systeme untersucht wurden. Es stützt sich auch auf die produktivsten Probleme der symbolischen Logik des vergangenen Jahrhunderts: das Entscheidungsproblem, die Vollständigkeit und Unvollständigkeit der logischen Theorien und schließlich die Komplexitätstheorie. Das Problem der modularen Kombination von Spezialalgorithmen für jede Domäne ist so tiefgreifend und faszinierend wie die Suche nach neuen Algorithmen, die im Kontext einer Kombination besonders gut funktionieren. SMT spielt auch eine sehr nützliche Rolle in der Softwareentwicklung. Moderne Software, Hardwareanalyse und modellbasierte Tools sind zunehmend komplexe und facettenreiche Softwaresysteme. Im Kern handelt es sich jedoch immer um eine Komponente, die symbolische Logik zur Beschreibung von Zuständen und Transformationen zwischen ihnen verwendet. Ein gut abgestimmter SMT-Solver, der die neuesten Durchbrüche berücksichtigt, skaliert normalerweise Größenordnungen über benutzerdefinierte Ad-hoc-Solver hinaus.

vzn
quelle
Das ist ein sehr guter Punkt. Aber auch wenn Sie einen SMT-Löser verwenden, gibt es einen rein SAT-basierten Teil der Suche, der von erfolgreichen "Rezepten" profitieren kann ...
Bordaigorl,
Es ist nicht ganz richtig zu sagen, dass es sich um einen "rein SAT-basierten Teil der Suche" handelt, da (wie angegeben / meines Verständnisses) die spezielle bekannte / konstruierte Struktur der generierten Instanzen in ihren Heuristiken verwendet, die ein "Vanille" -Löser nicht verwenden würde "erkenne". mit anderen Worten, es (dh die Kombination ) ist nicht auf Bestandteile (dh Encoder plus Solver) oder lediglich ein anderes standardisiertes Codierungssystem "reduzierbar / trennbar".
vzn
Aha. Ich werde mehr darüber lesen, danke!
Bordaigorl
sicher. Beachten Sie auch , dass die Programmierung des Antwortsatzes etwas ähnlich ist.
vzn