Understanding effects of produce-proofs, field names, and intermediate check-sat's on performance

Question

For the below code, I have observed very fast results that seem to be caused/affected by three unusual aspects:

When using (set-option :produce-proof true), the final UNSAT is very fast. Without this option, the final check-sat does not terminate.
When using an intermediate check-sat and assertion (all push/popped) the performance of the final check-sat is very fast. Without intermediate check-sat commands, the final check-sat does not terminate.
After renaming datatype fields the performance of the final check-sat is abysmal (termination takes 30x longer).

Can someone explain the behavior in these cases? Is it just that the combination of options results in the correct facts being retained to answer the final SAT quickly? How does the field name for an unused constructor factor in to the solver's performance?

The code related to this question follows. Embedded in the code are comments with extra context and a rehashing of the questions.

;;;;;;;;;;;;;;;;;;;;;;;;;;;; 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)

David Monniaux David Monniaux · Accepted Answer · 2013-07-23T09:41:53

In SMT solvers, some aspects, most notably literal selection, are "random" - that is, if there is no better way of choosing, the system uses a random number. By changing the way things are named, or whether or not a proof is logged, you may change the pattern of how random numbers are used, resulting in the solver going into a more appropriate or inappropriate direction.

I note that you use quantified axioms. In general, when faced with such axioms, Z3 will use an incomplete approach known as "quantifier instanciation" - that is, if it has ∀x F(x), it will try F(x) for various values of x it thinks are interesting. The selection of these values is heuristic and (I haven't checked) probably dependent on random choice.

I'd suggest trying your examples with varying random_seed and see what happens.

Understanding effects of produce-proofs, field names, and intermediate check-sat's on performance

1 Answers