Quantifizierer und Muster (QBF-Formel)

Question

Ich versuche, ein QBF in Smt-Lib 2-Syntax für z3 zu kodieren. Laufende z3 führt zu einer Warnung

WARNUNG: failed ein Muster für quantifier finden (quantifier ID: k 14)

und die Erfüllbarkeit Ergebnis "unbekannt".

Der Code ist wie folgt:

(declare-fun R (Bool Bool Bool Bool) Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool)) 
     (forall ((x1 Bool)) 
     (R x1 x2 x3 y) 
    ) 
    ) 
) 
) 
(check-sat) 

ich die Warnung losgeworden durch den Code

Umschreiben

(set-option :auto-config false) 
(set-option :mbqi false) 
(declare-fun R (Bool Bool Bool Bool) Bool) 
(declare-fun x1() Bool) 
(declare-fun x2() Bool) 
(declare-fun x3() Bool) 
(declare-fun y() Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (! 
    (exists ((y Bool)) 
    (! 
     (forall ((x1 Bool)) 
     (! 
     (R x1 x2 x3 y) 
     :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
) 
) 
(check-sat) 

Das Ergebnis für die Sat-Abfrage bleibt jedoch „unbekannt“.

Ich vermute, dass ich die Muster richtig bekommen muss? Wie gebe ich sie für verschachtelte Quantifizierer an? Einfachere Beispiele mit Quantifizierern scheinen jedoch ohne Musterannotation zu funktionieren.

Die Antwort auf What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) " und die z3 Anleitung hat mir leider nicht viel geholfen.

Answer 1

Diese Warnmeldung kann ignoriert werden. Es informiert Sie nur, dass die E-Matching-Engine diese quantifizierte Formel nicht verarbeiten kann.

E-Abgleich zeigt nur an, dass ein Problem unerfüllbar ist. Da Ihr Beispiel erfüllbar ist, wird die E-Anpassung nicht sehr nützlich sein. Das heißt, Z3 kann sat nicht mit der E-Matching-Engine zurückgeben. Die modellbasierte Quantifiziererinstanz (MBQI) ist die einzige Maschine in Z3, die zeigen kann, dass Probleme, die Quantifizierer enthalten, erfüllbar sind.

Mit der Standardkonfiguration gibt Z3 für Ihr Beispiel sat zurück. Es gibt unknown zurück, weil Sie das MBQI-Modul deaktiviert haben. Die MBQI-Engine garantiert, dass Z3 eine Entscheidungsprozedur für viele Fragmente ist (siehe http://rise4fun.com/Z3/tutorial/guide). Es ist jedoch im Allgemeinen sehr teuer und sollte deaktiviert werden, wenn schnelle und angenäherte Antworten ausreichend sind. In diesem Fall kann unknown als probably sat gelesen werden. Verifizierungswerkzeuge wie VCC deaktivieren das MBQI-Modul, da es nicht in der Lage ist, über die von ihnen erzeugten Formeln zu entscheiden. Das heißt, die von VCC erzeugten Formeln befinden sich nicht in irgendeinem der Fragmente, die durch die MBQI-Maschine bestimmt werden können. Wir sagen, dass ein Fragment durch Z3 entschieden werden kann, wenn für irgendeine Formel in dem Fragment Z3 sat oder unsat zurückgegeben wird (d. H. Es gibt unknown nicht zurück). Natürlich geht dieser Anspruch davon aus, dass wir über unbegrenzte Ressourcen verfügen. Das heißt, Z3 kann auch fehlschlagen (d. H. unknown zurückgeben) für entscheidbare Fragmente, wenn kein Speicher mehr zur Verfügung steht, oder es wurde vom Benutzer eine Zeitüberschreitung festgelegt.

Schließlich hat Z3 3.2 eine bug in der MBQI-Engine. Der Fehler wurde behoben und hat keine Auswirkungen auf dein Problem. Wenn Sie brauchen, kann ich Ihnen eine Vorabversion von Z3 4.0 geben, die den Bugfix enthält.