Constraint-Zufriedenheitsproblem (CSP) vs. Erfüllbarkeitsmodulo-Theorie (SMT); mit einer Coda zur Constraint-Programmierung

Traut sich jemand zu klären, in welchem ​​Verhältnis diese Fachrichtungen zueinander stehen, oder gibt er vielleicht auf der Ebene der Probleme eine konkretere Antwort? Wie welche beinhaltet welche unter der Annahme einiger weithin akzeptierter Formulierungen. Wenn ich das richtig verstanden habe, betreten Sie beim Wechsel von SAT zu SMT im Grunde genommen den Bereich CSP. Umgekehrt, wenn Sie CSP auf Booleaner beschränken, sprechen Sie im Grunde genommen von SAT und vielleicht ein paar verwandten Problemen wie #SAT. Ich denke, dies ist klar (z. B. Kolaitis und Vardis Kapitel "Ein logischer Ansatz zur Erfüllung von Beschränkungen" in der Theorie des endlichen Modells und ihrer Anwendungen)von Grädel et al.), aber was mir weniger klar ist, ist, wann die Beschränkungen "modulo a theory" sind und wann nicht? Bedeutet SMT immer, dass die Theorie nur Gleichheit verwendet und Ungleichheitsbeschränkungen immer im weiteren Bereich der CSP liegen? Soweit ich das beurteilen kann, kann man häufig Slack-Variablen einführen , so dass der Unterschied [falls vorhanden] weniger als offensichtlich ist.

Das relativ aktuelle "Satisfiability Handbook" (IOP Press 2009) fasst sowohl SMT- als auch CSP-Probleme unter seinem umfassenden "Erfüllbarkeits" -Rahmen zusammen, hilft mir jedoch aufgrund seiner Struktur (Kapitel von verschiedenen Autoren) nicht wirklich, dies herauszufinden .

Ich hoffe, dass die Terminologie weniger verwirrend wird, wenn Sie von Constraint- Programmierung sprechen , die (analog zum Begriff "mathematische Programmierung") hoffentlich die Minimierung / Maximierung einer objektiven Funktion beinhaltet. Der Wikipedia-Artikel zur Constraint-Programmierung ist leider so vage, dass ich nicht genau sagen kann, ob dies tatsächlich passiert. Aus den Essentials of Constraint Programming von Frühwirth und Abdennadher (S. 56) kann ich entnehmen, dass ein "Constraint Solver" in der Regel mehr als nur eine Erfüllbarkeitsprüfung bietet, wobei Vereinfachung usw. in der Praxis wichtig ist.

Obwohl dies kaum eine aktuelle CS-theoretische Forschungsfrage ist, erwarte ich auf der CS.SE-Site für Studenten, die ich unter https://cs.stackexchange.com/questions/14946/distinguish- gesehen habe, keine guten Antworten auf diese Frage. Entscheidungsprozedur gegen smt-Löser gegen Theorembeweiser gegen Beschränkungssol (der viele Wörter enthält, aber leider nicht das, was ich für eine echte Antwort halte).

SAT, CP, SMT und (ein Großteil) ASP haben alle die gleichen kombinatorischen Optimierungsprobleme. Sie begegnen diesen Problemen jedoch aus unterschiedlichen Blickwinkeln und mit unterschiedlichen Werkzeugkästen. Diese Unterschiede bestehen hauptsächlich darin, wie jeder Ansatz Informationen über die Erkundung des Suchraums strukturiert. Meine Arbeitsanalogie ist, dass SAT Maschinencode ist, während die anderen höhere Sprachen sind.

$x_1 \lor \overline{x_2} \lor x_3$$\{(x_1,0),(x_2,1),(x_3,0)\}$$x_1$$x_3$$x_2$$x_1 \lor \overline{x_2} \lor x_3 \lor x_4$$x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$

Eine Annäherung an die Klauselstruktur wird beibehalten, um die Menge der Lösungen einzugrenzen und festzustellen, ob diese Menge leer ist. Während der Suche stellen sich einige Teilzuweisungen möglicherweise als nicht in einer Lösung enthalten heraus (selbst wenn sie die einzelnen Bedingungen in der Instanz erfüllen). Diese werden als Nogoods bezeichnet , ein Begriff, der von ("Mr GNU") Stallman und Sussman eingeführt wurde$x \le 5$$x = 5$. Daher gibt es keine einzige allgemeine Klauselstruktur, sondern eine, die mit jeder Auswahl der Darstellung verbunden ist, je nachdem, was die Singletons (Literale) der Klauselstruktur darstellen.

Constraint Programming (CP) war traditionell eine KI-Disziplin mit Schwerpunkt auf Zeitplanung, Zeitplanung und kombinatorischen Problemen und spielt daher eine zentrale Rolle für Variablen, die mehr als nur zwei Werte annehmen können (in der Regel jedoch nur endlich viele). CP hat auf effiziente Suche Wert gelegt und hat, motiviert durch die traditionellen Anwendungen, der all-different(Injektivitäts-) Einschränkung eine zentrale Rolle eingeräumt, aber auch effiziente Propagatoren für viele andere Arten von Einschränkungen entwickelt. Die formalen Definitionen von CP gibt es seit mindestens Montanaris Aufsatz " Networks of Constraints " von 1974mit Vorläufern, die noch früher zurückreichen. Diese Gewichtung der Geschichte könnte dazu beigetragen haben, dass CP in den letzten zehn Jahren hinter anderen Ansätzen der Rohperformance zurückblieb. CP verwaltet klassisch eine Approximation des Komplements der Klauselstruktur über eine Reihe von aktiven Domänen für die Variablen. Ziel ist es, Werte aus den aktiven Domänen zu entfernen, die Klauselstruktur zu untersuchen, indem versucht wird, Variablen Kandidatenwerte zuzuweisen, und bei Bedarf ein Backtracking durchzuführen.

Satisfiability Modulo Theorien (SMT) kamen aus der Verifikations-Community. Jede Theorie in einem SMT-Solver bildet eine implizite Darstellung von möglicherweise unendlich vielen SAT-Klauseln. Die mit SMT verwendeten Theorien und die in CP verwendeten Einschränkungen spiegeln ihre unterschiedlichen historischen Anwendungen wider. Die meisten Theorien, die SMT in Betracht zieht, haben mit ganzzahligen Arrays, echten geschlossenen Feldern, linearen Ordnungen und dergleichen zu tun. Diese ergeben sich aus der statischen Analyse von Programmen (bei der computergestützten Verifikation) oder bei der Formalisierung von mathematischen Beweisen (bei der automatisierten Argumentation). Im Gegensatz dazu ist bei der Zeitplanung und Terminierung die Einschränkung der Injektivität von zentraler Bedeutung, und obwohl dies das Standard- SMTLIB- seit ihrer im Jahr 2003 eine Einschränkung hatte (über dasdistinct Symbol ist, wurden bis 2010 nur SMT-Solver implementiertdistinctüber einen naiven Algorithmus. Zu diesem Zeitpunkt wurde die Matching-Technik aus dem Standard-CP-Propagator für all-differentportiert, was sich in großem Maße auf große Listen von Variablen auswirkte. siehe Ein Alldifferent Constraint Solver in SMT von Banković und Marić, SMT 2010. Darüber hinaus sind die meisten CP-Propagatoren für Probleme mit endlichen Domänen ausgelegt, wohingegen Standard-SMT-Theorien sich mit unendlichen Domänen (Ganzzahlen und neueren Realzahlen) ab Werk befassen. SMT verwendet eine SAT-Instanz als Näherungswert für die Klauselstruktur und extrahiert gegebenenfalls Nogood-Klauseln aus den Theorien. Eine gute Übersicht ist Erfüllbarkeit Modulo Theories: Einführung und Anwendung von De Moura und Bjorner, doi: 10.1145 / 1995376.1995394.

Anrufbeantworterprogrammierung ( ASP) ist aus der Logikprogrammierung hervorgegangen. Aufgrund seiner Konzentration auf die Lösung des allgemeineren Problems der Suche nach einem stabilen Modell und auch weil es eine universelle und existenzielle Quantifizierung ermöglicht, war ASP für viele Jahre nicht wettbewerbsfähig mit CP oder SMT.

Formal ist SAT ein CSP für Boolesche Domänen, aber der Fokus in SAT auf das Lernen von Klauseln, gute Heuristiken für die Konflikterkennung und schnelle Wege zum Zurückverfolgen unterscheidet sich erheblich von dem traditionellen CSP-Fokus auf Propagatoren, Konsistenz und Heuristiken für die variable Reihenfolge. SAT ist normalerweise sehr effizient, aber für viele Probleme ist ein großer Aufwand erforderlich, um das Problem zuerst als SAT-Instanz auszudrücken. Die Verwendung eines Paradigmas auf höherer Ebene wie CP kann einen natürlicheren Ausdruck des Problems ermöglichen, und dann kann entweder die CP-Instanz von Hand in SAT übersetzt werden, oder ein Tool kann sich um die Übersetzung kümmern. Eine schöne Übersicht über die Hauptmerkmale von SAT finden Sie unter Über moderne Klausel-Lern- Erfüllungslöser von Pipatsrisawat und Darwiche, doi: 10.1007 / s10817-009-9156-3 .

Gehen wir nun von den allgemeinen zu den heutigen Besonderheiten über.

In den letzten zehn Jahren haben sich einige CP-Mitarbeiter auf die Lazy-Clause-Generierung (LCG) konzentriert. Dies ist im Wesentlichen eine Möglichkeit, CP-Propagatoren mithilfe flexiblerer SMT-ähnlicher Techniken anstelle der eher starren Abstraktion aktiver Domänen miteinander zu verbinden. Dies ist nützlich, da es eine lange Geschichte veröffentlichter CP-Propagatoren gibt, um viele Arten von Problemen effizient darzustellen und zu lösen. (Ein ähnlicher Effekt würde natürlich durch gemeinsame Anstrengungen zur Implementierung neuer Theorien für SMT-Löser erzielt.) LCG weist eine Leistung auf, die häufig mit SMT konkurriert und bei einigen Problemen möglicherweise überlegen ist. Ein kurzer Überblick ist Stuckeys CPAIOR 2010-Artikel Lazy Clause Generation: Kombination der Möglichkeiten der SAT- und CP- (und MIP-?) Lösung , doi: 10.1007 / 978-3-642-13520-0_3. Es lohnt sich auch, das Positionspapier von Garcia de la Banda, Stuckey, Van Hentenryck und Wallace zu lesen, in dem eine CP-zentrierte Vision der Zukunft der Optimierungstechnologie dargestellt wird. Doi: 10.1007 / s10601-013-9149-z .

Soweit ich das beurteilen kann, scheint sich der Schwerpunkt der jüngsten SMT-Forschung weitgehend auf Anwendungen in formalen Methoden und in der formalisierten Mathematik verlagert zu haben. Ein Beispiel ist die Rekonstruktion von Proofs, die von SMT-Solvern in Proofsystemen wie Isabelle / HOL gefunden wurden, indem Isabelle / HOL-Taktiken erstellt werden, um Inferenzregeln in SMT-Proof-Traces widerzuspiegeln. Siehe Fast LCF-Style Proof Reconstruction für Z3 von Böhmer und Weber auf der ITP 2010.

Die besten ASP-Löser wurden in den letzten Jahren entwickelt, um mit CP-, SMT- und SAT-Lösern konkurrenzfähig zu werden. Ich bin nur vage mit den Implementierungsdetails vertraut, die es Lösern ermöglicht haben clasp, wettbewerbsfähig zu sein, und kann diese daher nicht wirklich mit SMT und CP vergleichen, aber clasp wirbt ausdrücklich dafür, dass der Schwerpunkt auf dem Erlernen von Nogoods liegt.

Das Überschreiten der traditionellen Grenzen zwischen diesen Formalismen ist die Übersetzung von abstrakteren Problemdarstellungen in effizient umsetzbare Formalismen auf niedrigerer Ebene. Einige der führenden ASP- und CP-Löser übersetzen ihre Eingaben jetzt explizit in eine SAT-Instanz, die dann mit einem handelsüblichen SAT-Löser gelöst wird. In CP verwendet der Assistent zur Modellierung von Einschränkungen für Savile-Zeilen Compiler-Entwurfstechniken, um Probleme, die in der Sprache Essence auf mittlerer Ebene ausgedrückt werden, in einen Formalismus auf niedrigerer Ebene zu übersetzen, der für Eingaben in CP-Löser wie Minion oder MiniZinc geeignet ist . Savile Row arbeitete ursprünglich mit einer CP-Darstellung als Low-Level-Formalismus, führte jedoch SAT als Ziel in Version 1.6.2 ein. Außerdem die noch übergeordnete Sprachessenzkann jetzt automatisch mit dem Zauberwerkzeug in Essence 'übersetzt werden . Gleichzeitig werden SAT-only-Solver mit niedriger Stufe wie Lingeling jedes Jahr weiterentwickelt, zuletzt durch abwechselndes Lernen von Klauseln und In-Processing-Phasen. siehe die kurze Übersicht Was gibt es Neues in den SAT- und ASP-Wettbewerben von Heule und Schaub im AAAI 2015?

Die Analogie zur Geschichte der Programmiersprachen erscheint daher angebracht. SAT wird zu einer Art "Maschinencode", der auf ein einfaches Modell der Erforschung der Klauseln in der Klauselstruktur abzielt. Die abstrakten Paradigmen werden immer mehr zu höheren Computersprachen, mit ihren eigenen unterschiedlichen Methoden und Anwendungen, mit denen sie sich gut auseinandersetzen können. Schließlich ähnelt die immer dichter werdende Ansammlung von Verknüpfungen zwischen diesen verschiedenen Ebenen allmählich dem Ökosystem der Compiler-Optimierung.