Offene oder interaktive Einschränkungszufriedenheit

17

In der Vergangenheit habe ich Koordinationsmodelle implementiert, bei denen SAT und die reguläre Beschränkungszufriedenheit das zentrale Arbeitspferd in ihren Motoren waren. In diesem Arbeitsbereich möchte ich die Modelle interaktiver gestalten. Der beste Weg, dies zu tun, besteht darin, den Constraint-Solver so zu öffnen, dass er keine Black Box mehr ist.

Daher bin ich daran interessiert, mehr über die Constraint-Zufriedenheit zu erfahren, wenn die Constraints externe Variablen , Prädikate und Funktionen haben , dh die Constraint-Sprache kann Prädikate wie die nur sein können zufrieden, indem ein Agent außerhalb des Lösers konsultiert wird, und dann nur, wenn geschliffen ist. Ein Szenario, in dem dies nützlich ist, ist immer dann, wenn einem externen Entscheidungsprozess entspricht, der nicht in den Constraint Solver integriert werden kann. Solche Constraint-Löser können als offen (da Constraints nicht vollständig bekannt sind) oder interaktiv bezeichnet werdenP(x)xP (Da eine Interaktion erforderlich ist, um die Bedingungen zu erfüllen).

Ich würde gerne beides wissen:

  • theoretische Forschung in dieser Richtung durchgeführt
  • Tools oder Bibliotheken, die Constraint-Löser implementieren, die die Interaktion mit der Außenwelt während des Constraint-Lösungsprozesses ermöglichen.
sat lo.logic csp Dave Clarke
quelle

Antworten:

9

Die bisherigen Arbeiten zu offenen und interaktiven Randbedingungen überzeugen mich insgesamt nicht.

Ein Versuch, die Nachvollziehbarkeitsfragen zu untersuchen, war:

Dieses Papier lässt jedoch einige wichtige Fragen offen. Der Ansatz über Propagatoren in diesem Artikel steht in engem Zusammenhang mit vorhandenen Implementierungen von Integritätsregelungslösern.

Ich denke, die Arbeit an SMT (Erfüllbarkeitsmodulo-Theorien) ist auch eng mit Ihrer Frage verbunden. SMT-Theorien werden häufig durch Probleme bei der Verifizierung von Software und Hardware motiviert, es gibt jedoch Theorien mit AI-Charakter. Ich freue mich auf mehr Anwendungen, die mit SMT als Kerntechnologie erstellt wurden, und auf mehr Arbeit bei Einschränkungen, bei denen Ideen von SMT angewendet werden.

András Salamon
quelle
1
Das Papier sieht auf jeden Fall interessant aus. Ich hätte nie gedacht, dass SMT-Löser das tun, was ich brauche. Es ist sicherlich eine Möglichkeit, diese Gegend zu erkunden.
Dave Clarke
Der letzte Kommentar verwirrt mich. SMT-Solver beziehen sich auf Logik und Theorien, nicht auf bestimmte Prädikate. Leute können gerne neue Theorien und Benchmarks beisteuern. Ich weiß, dass die MathSAT-Entwickler KI- und Planungsprobleme untersucht haben.
Vijay D
@ Vijay D: Sie haben Recht, dieser Satz ist übermäßig voreingenommen und ich werde ihn überarbeiten. Eine effiziente Implementierung von INJECTIVE als SMT-Theorie wurde 2010 von Banković und Marić veröffentlicht ( argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf ).
András Salamon
7

Beim Lesen Ihrer Frage stimme ich auch darin überein, dass die Modulo-Theorien zur Zufriedenheit eng mit Ihren Bedürfnissen zusammenhängen. Ich würde vorschlagen, das Buch Decision Procedures - An Algorithmic Point of View zu lesen .

Giorgio Camerani
quelle
Inwieweit ist das Buch The Calculus of Computation: Entscheidungsverfahren mit Verifizierungsanträgen von Aaron R. Bradley und Zohar Manna verwandt / sinnvoll? Ich weiß, wo eine Kopie davon zu Fuß erreichbar ist.
Dave Clarke
@ Dave: Haftungsausschluss: Meine persönliche Erfahrung mit SMT steht erst am Anfang ;-) Ich habe mir gerade das Inhaltsverzeichnis dieses Buches angesehen. Es scheint einen großen Schnittpunkt zwischen ihm und dem, den ich angegeben habe, zu geben. In letzterem Fall wird das, was Sie hier als externe Funktionen bezeichnen, dort als nicht interpretierte Funktionen bezeichnet und ausführlich behandelt. Ich konnte keine nicht interpretierten Funktionen im Inhaltsverzeichnis von Entscheidungsverfahren mit Verifizierungsanträgen finden . Es scheint jedoch ein sehr gutes Buch zu sein, und vielleicht kann es sich als nützlich erweisen.
Giorgio Camerani
@ Dave: In diesen Tagen lese ich Entscheidungsverfahren - eine algorithmische Sichtweise . Ich habe das Kapitel über nicht interpretierte Funktionen noch nicht erreicht , aber wenn ich mich nicht irre, werden Formeln mit nicht interpretierten Funktionen in Formeln in der Theorie der Gleichheit umgewandelt. Es ist der Fall, dass die Theorie der Gleichheit in Entscheidungsverfahren mit Überprüfungsanträgen (Kapitel 9) behandelt wird.
Giorgio Camerani
1
Ich denke, Amazon ruft an.
Dave Clarke
@ Dave: OK, ausgezeichnet! ;-)
Giorgio Camerani
7

P(x)

Evgenij Thorstensen
quelle
4

Ich bin ein bisschen verwirrt über den Begriff interaktiv. Ich melde mich bei den anderen und füge hinzu, dass ein SMT-Löser hilfreich sein könnte. Als Ergänzung zu Walter Bishops Kommentar stehen Folien für das Buch Decision Procedures (Kroening and Strichman) zur Verfügung. John Harrisons gründliche Behandlung im Handbuch der praktischen Logik und des automatisierten Denkens könnte Sie ebenfalls interessieren. Beispielcode ist online verfügbar.

Philipp Ruemmers Prinzessin unterstützt die Arithmetik mit nicht interpretierten Prädikaten, die zu dem passen könnten, was Sie unter offen verstehen. Es ist in Scala geschrieben, verwendet E-Matching für die Handhabung der Quantifizierung und stellt Interpolanten bereit.

Vijay D
quelle
0

Was ist mit Tools, wenn Sie sich für Prolog als Sprache Ihrer Wahl entscheiden, kann ich einige Implementierungsansätze vorschlagen:

  • GNU Prolog mit ist eine C-Programmierbibliothek. Sie können C-Funktionen aus Prolog und Prolog aus C aufrufen. Dies eröffnet Ihnen viele Möglichkeiten, die Funktionalität zu erweitern. Pro: Gnu Prolog ist einer der schnellsten frei verfügbaren Prolog-Compiler. Hinweis: Einige Leute beschweren sich über das Fehlen einiger eingebauter Prädikate. Tatsächlich können die meisten von ihnen implementiert werden. Schauen Sie sich die Prolog-Kompatibilitätsebenen @SO an
  • SWI-Prolog verfügt über eine interessante Programmierbibliothek, einschließlich Netzwerkkommunikation, Unterstützung von Protokollpuffern usw. Und ist sehr beliebt.
  • XSB-Prolog Einige Leute behaupten, es sei das interessanteste Projekt in Bezug auf Interoperabilität - einschließlich: Datenbankschnittstellen usw.

Prolog ist eine Programmiersprache, die für viele Arten von Lösern geeignet ist (und die meisten von ihnen haben ihre Löser für endliche Domänen).

Grzegorz Wierzowiecki
quelle