Für welche Quantoren ist SMT vollständig?

Question

Ich habe mir verschiedene SMT-Löser angesehen, hauptsächlich Z3, CVC4 und VeriT. Sie alle haben vage Beschreibungen ihrer Fähigkeit, SMT-Probleme mit Quantifizierern zu lösen. Ihre Dokumentation basiert hauptsächlich auf Beispielen (Z3) oder besteht aus wissenschaftlichen Arbeiten, die mögliche Änderungen beschreiben, die möglicherweise tatsächlich umgesetzt werden.

Ich weiß, dass es entscheidbar Fragmente von Logik erster Ordnung, wie zum Beispiel:

• endlichwertige begrenzt quantifiers
• monadische Logik erster Ordnung

Was würde Ich mag an Wissen ist, welche (wenn überhaupt) Klassen von FOL die verschiedenen SMT-Löser sind, die garantiert vollständig sind? Woher weiß ich, ob ein Problem, das ich sehe, in den Fragmenten liegt, für die sie vollständig sind?

Answer 1

Es gibt zwei Kategorien quantifizierter Formeln, für die CVC4 vollständig ist.

(1) Quantifizierte Formeln mit endlichen Domänen.

CVC4 ist Finite-Modell-vollständig auf Quantifizierer über nicht interpretierte Sortierungen, was bedeutet, dass, wenn es ein Modell gibt, in dem alle nicht interpretierten Sortierungen als endlich interpretiert werden, CVC4 es schließlich finden wird. Weitere Einzelheiten können Sie dieses Papier:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
, die die Tagungsunterlagen hier fasst zusammen:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Beachten Sie, dass diese Techniken mit einer Theorie von CVC4 unterstützt kombinieren. Unter der Voraussetzung, dass die Theorie entscheidbar ist und die Quantifizierung keine (unendlich) interpretierten Sorten beinhaltet, bleibt die Vollständigkeitsgarantie für endliche Modelle bestehen.

Der Ansatz ist auch für bestimmte Fragmente wie das Bernays-Schoenfinkel-Ramsey-Fragment (EPR) reflektionsvollständig, was bedeutet, dass CVC4 für jedes unerfüllbare Problem in diesem Fragment schließlich "ungesättigt" antworten wird.

Wenn Sie an dieser Funktion interessiert sind, verwendet CVC4 standardmäßig nicht das endliche Modell für ein Eingabeproblem. Die Befehlszeilenoption "--finite-model-find" aktiviert diese Techniken.

(2) Quantifizierte Formeln in einigen Theorien, die Quantifizierer eliminieren.

Zum Beispiel ist CVC4 vollständig für (reine) quantifizierte lineare Arithmetik. Details dazu finden Sie das Papier sehen:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
, die auf einer früheren Konferenz Papier baut:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf

Dies ist im Geiste zu anderen Ansätzen, zum Beispiel in Z3:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf

Answer 2

Bei das Risiko, die Frage nicht hilfreich zu beantworten, gibt es Gründe, warum dieses Material schwer zu finden ist.

Die Verbindung zwischen der Entscheidungsfähigkeit und "kann tatsächlich mein spezifisches Problem in einer Menge von Zeit lösen, die ich warten will" ist nicht so stark. Oft sind Beispiele, Benchmarks und experimentelle Ergebnisse ein besserer Indikator (und werden daher vorgestellt).

Auch die meisten Löser machen eine Menge heuristische Umschreiben und Problembearbeitung vor dem Versuch zu lösen. Daher sind klassische, syntaktische Wege, um entscheidungsfähige Fragmente auszudrücken, nicht immer anwendbar, da andere Probleme in entscheidbare umgeschrieben werden können (hoffentlich nicht umgekehrt, aber ich kann nicht versprechen, dass es nie passiert!).

Schließlich verwenden viele Löser heuristische Semi-Decision-Prozeduren, die gut funktionieren, aber in etwas formaler als Code schwer zu beschreiben sind. So gibt es Dinge, die vielleicht in keinem bekannten entscheidbaren Fragment vorkommen, für die aber Antworten gefunden werden können.