Quantifizierer Vs Non-Quantifier

Question

Ich habe eine Frage zu Quantifier.

Angenommen, dass ich ein Array haben, und ich will Array-Index 0, 1 und 2 sind für dieses Array berechnen -

(declare-const cpuA (Array Int Int)) 
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1))) 

Oder sonst kann ich die Verwendung derselben forall konstruieren, wie angegeben -

Jetzt möchte ich den Unterschied zwischen zwei von ihnen verstehen. Die erste Methode wird schnell ausgeführt und liefert ein einfaches und lesbares Modell. Im Gegensatz dazu ist die Code-Größe mit der zweiten Option sehr gering, aber das Programm benötigt Zeit für die Ausführung. Und auch die Lösung ist komplex.

Ich möchte die zweite Methode verwenden, da mein Code kleiner wird. Ich möchte jedoch ein lesbares einfaches Modell finden.

Answer 1

Quantifizierer Argumentation ist in der Regel sehr teuer. In Ihrem Beispiel entspricht die quantifizierte Formel den drei angegebenen Aussagen. Das ist jedoch nicht so, wie Z3 Ihre Formel entscheidet/löst. Z3 löst Ihre Formel mit einer Methode namens Model-Based Quantifier Instantiation (MBQI). Diese Technik kann viele Fragmente entscheiden (siehe http://rise4fun.com/Z3/tutorial/guide). Es wirkt hauptsächlich auf die in diesem Handbuch beschriebenen Fragmente. Es unterstützt nicht interpretierte Funktionen, Arithmetik und Bit-Vektor-Theorien. Es hat auch begrenzte Unterstützung für Arrays und Datentypen. Dies ist ausreichend, um Ihr Beispiel zu lösen. Das von Z3 produzierte Modell scheint komplizierter, weil die gleiche Maschine verwendet wird, um kompliziertere Fragmente zu entscheiden. Das Modell sollte als ein kleines funktionales Programm erscheinen. Sie können weitere Informationen, wie dieser Ansatz funktioniert in den folgenden Artikeln:

• Complete instantiation for quantified SMT formulas

• Efficiently Solving Quantified Bit-Vector Formula

Beachten Sie, dass, Array Theorie zur Darstellung/Modellierung unbeschränkten vor allem nützlich ist oder große Arrays. Das heißt, die tatsächliche Größe des Arrays ist nicht bekannt oder zu groß. Mit "groß" meine ich, dass die Anzahl der Array-Zugriffe (d. H. selects) in Ihrer Formel viel kleiner ist als die tatsächliche Größe des Arrays. Wir sollten uns fragen: "Brauchen wir wirklich Arrays zum Modellieren/Lösen von Problem X?". Sie können die folgenden Alternativen berücksichtigen:

• (Nicht interpretierte) Funktionen anstelle von Arrays. Ihr Beispiel kann codiert werden auch als:

  (deklarieren-fun CPUA (Int) Int)

  (behaupten (oder (= (CPUA 0) 0) (= (CPUA 0) 1)))
  (assert (oder (= (CPUA 1) 0) (= (CPUA 1) 1)))
  (assert (oder (= (CPUA 2) 0) (= (CPUA 2) 1)))

• Programmatische API. Wir haben viele Beispiele gesehen, bei denen Arrays (und Funktionen) verwendet werden, um eine kompakte Codierung bereitzustellen. Eine kompakte und elegante Codierung ist nicht unbedingt einfacher zu lösen. Eigentlich ist es normalerweise umgekehrt.Mit einer programmatischen API für Z3 können Sie das Beste aus beiden Welten (Leistung und Kompaktheit) erreichen. Im folgenden Link habe ich Ihr Beispiel mit einer "Variable" für jede Position des "Arrays" codiert. Makros/Funktionen werden verwendet, um Abhängigkeiten zu codieren, wie zum Beispiel: Ein Ausdruck ist ein 0 oder 1.