Verständnis Auswirkungen von Produkten-Proofs, Feldnamen und Zwischen Check-sat des auf Leistung

Question

Für den Code unten, ich habe sehr schnell Ergebnisse beobachtet, die offenbar durch drei ungewöhnliche Aspekte verursacht/betroffen sein:

• Wenn mit (set-option :produce-proof true) ist das endgültige UNSAT sehr schnell. Ohne diese Option endet das abschließende check-sat nicht.
• Bei Verwendung eines Zwischen-Check-Sat und Assertion (alle Push/Popped) ist die Leistung der letzten Check-Sat sehr schnell. Ohne zwischenzeitliche check-sat-Befehle wird der finale check-sat nicht beendet.
• Nach umbenennen Datentyp Felder die Leistung der letzten Check-Sat ist miserabel (Kündigung dauert 30x länger).

Kann jemand das Verhalten in diesen Fällen erklären? Ist es nur, dass die Kombination von Optionen dazu führt, dass die richtigen Fakten beibehalten werden, um den endgültigen SAT schnell zu beantworten? Wie wirkt sich der Feldname für einen nicht verwendeten Konstruktor auf die Leistung des Solvers aus?

Der Code für diese Frage folgt. Eingebettet in den Code sind Kommentare mit zusätzlichem Kontext und eine erneute Zusammenfassung der Fragen.

;;;;;;;;;;;;;;;;;;;;;;;;;;;; Configuration ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

;; E-matching won't terminate on our queries, so turn it off 
(set-option :smt.ematching false) 
(set-option :smt.mbqi true) 

;; In lieu of an initial test, produce-proofs true is a huge benefit to 
;; the performance of the final check-sat 
(set-option :produce-proofs true) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Raw data ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

;; Our syntactic representation of 'Bits' 
;; Removing 'Raw2345', or renaming it to 'Raw2', causes ~30x more computation time. 
(declare-datatypes() ((Bits zero (Xor (left Bits) (right Bits)) (Raw (raw Int)) (Raw2345 (raw2 Int))))) 

;; Predicates over data 
(declare-fun secret(Bits) Bool) 
(declare-fun known(Bits) Bool) 

;; The existence of this first test is a significant benefit to the performance 
;; of the final check-sat (despite the push/pop). 
(push) 
(echo " There exists x and y that remain secret even when xor can cancel") 
(echo " (NB rules regarding AC theories are missing)") 
(assert (exists ((x Bits) (y Bits) (xA Bits) (xB Bits) (xC Bits) (yA Bits) (yB Bits) (yC Bits)) 
    (and (= x (Xor xA (Xor xB xC))) 
      (= y (Xor yA (Xor yB yC))) 
      (secret x) 
      (secret y) 
      (known xA) 
      (known xB) 
      (known xC) 
      (known yA) 
      (known yB) 
      (known yC) 
      (not (known x)) 
      (not (known y)) 
     ))) 
(check-sat) 
(pop) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;; Theory of xor ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

;; Axioms for 'Xor', expressed in terms of what the attacker knows 
(assert (forall ((y Bits) (x Bits))    ;nilpotence 
      (! (=> (known (Xor y (Xor x x))) 
       (known y)) :weight 0))) 
(assert (forall ((x Bits))      ;identity 
      (! (=> (known (Xor x zero)) 
       (known x)) :weight 0)))   ;commutativity 
(assert (forall ((x Bits) 
       (y Bits)) 
      (! (=> (known (Xor x y)) 
       (known (Xor y x))) :weight 1))) 
(assert (forall ((x Bits)    ;associativity (1) 
       (y Bits) 
       (z Bits)) 
      (! (=> (known (Xor x (Xor y z))) 
       (known (Xor (Xor x y) z))) :weight 1))) 
(assert (forall ((x Bits)    ;associativity (2) 
       (y Bits) 
       (z Bits)) 
      (! (=> (known (Xor (Xor x y) z)) 
       (known (Xor x (Xor y z)))) :weight 2))) 

;; Assume knowledge of xor 
(assert (known zero)) 
(assert (forall ((x Bits) 
       (y Bits)) 
      (! (=> (and (known x) 
        (known y)) 
       (known (Xor x y))) :weight 4))) 

;; The below test now seems needed for decent performance - odd since 
;; formulations prior to this pretty one for stackoverflow didn't include 
;; this particular check-sat. 
(echo " Z3 has properly discarded the pushed/popped assertion.") 
(echo " Our problem remains SAT") 
(check-sat) 

;; Simple test 
(push) 
(assert 
    (exists ((a Bits) 
      (b Bits) 
      (c Bits) 
      (ra Bits) 
      (rb Bits) 
      (rc Bits)) 

     ; Our real problem: 
     (and (secret (Xor a (Xor b c))) 
      (known (Xor a (Xor ra rc))) 
      (known (Xor b (Xor rb ra))) 
      (known (Xor c (Xor rc rb))) 
      ))) 

(echo " Can Z3 use XOR rewriting lifted within uninterpreted functions") 
(echo "  (should get UNSAT)") 
(assert 
    (not (exists ((a Bits)) 
    (and (secret a) (known a))))) 
;; Skolemize must be turned off for performance reasons 
;; NTS: What is Z3 doing instead about existentials? 
(set-option :nnf.skolemize false) 
;; NST: Presumably, performing a depth three par-then helps 
;; because it aligns well with the depth of our asserts, but 
;; a smarter approach will be needed later. 
(check-sat-using (par-then (par-then smt smt) smt)) 
(pop) 

Answer 1

In SMT-Solver, einige Aspekte, insbesondere wörtliche Auswahl, sind „random“ - das heißt, wenn es keine bessere Art und Weise der Wahl ist, verwendet das System eine Zufallszahl. Indem Sie die Art und Weise ändern, in der die Dinge benannt werden, oder ob ein Beweis protokolliert wird, können Sie das Muster der Verwendung von Zufallszahlen ändern, was dazu führt, dass der Löser in eine geeignetere oder unangemessenere Richtung geht.

Ich bemerke, dass Sie quantifizierte Axiome verwenden. Im Allgemeinen wird Z3, wenn es mit solchen Axiomen konfrontiert wird, einen unvollständigen Ansatz verwenden, der als "Quantifier-Instanziierung" bekannt ist - das heißt, wenn es Fx F (x) hat, wird es F (x) für verschiedene Werte von x versuchen, die es sind interessant. Die Auswahl dieser Werte ist heuristisch und (ich habe nicht überprüft) wahrscheinlich abhängig von der zufälligen Auswahl.

Ich würde vorschlagen, versuchen Sie Ihre Beispiele mit verschiedenen random_seed und sehen, was passiert.