Symmetry breaking for Z3 — in the context of the UFBV logic (new version)

Question

(This is my second try to get help. If the question/approach do not make sense or not clear, please just let me know. I would also be pleased about any small hint or reference, which can help me to understand the behaviour of Z3 with my SBAs)

I am working on bounded verification of relational specification using the UFBV Z3 logic. The current problem I am investigating, needs the falsification of all possible models (because of a negative use of a reachability predicate), which kills the solver performance in higher bounds.

Because only a part of the possible models are indeed interesting (not isomorphic to others), I am trying to introduce symmetry breaking techniques (known in the SAT area).

However the use of what I call symmetry breaking axioms can improve the performance of Z3 in some cases, but the general, behaviour of the solver becomes instable.

One of my approaches (I think the most promising one), bases on breaking the symmetry on relations w.r.t. their domains. It introduces of each domains D of a relation R and each atom a \in D axioms, which enforce an order on the binary representation of R^{M} and R^{M[a+1/a]}, where M is a model for the specification. For homogeneous relations the axioms are relaxed.

Let be R \subset AxA a relation. My relaxed symmetry breaking axioms for R look like this:

;; SBA(R, A)_upToDiag
(assert
 (forall ( (ai A) (aj A) )
  (=>
   (bvult ai aj)
   (=>
    (forall ((x A))
     (=>
       (bvult x aj)
       (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
     )
    )
    (=>
     (R ai aj)
     (R (bvadd  ai  (_ bv1 n)) aj)
)))))    

;; SBA(R, A)_diag
(assert
 (forall ( (ai A) )
  (=>
   (forall ((x A))
    (=>
      (bvult x ai)
      (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
    )
   )
   (=>
    (R ai ai)
    (R (bvadd  ai  (_ bv1 n)) (bvadd  ai  (_ bv1 n)))
)))) 

My problem is, that the effect of using this SBAs is not stable/consistent. It differs from bound to bound and form specification to another. Also the use of all or only one of the SBAs affects the performance.

In the SAT context the success of the so-called symmetry breaking predicate (SBP) approach bases on the backtracking capability of the SAT solver, which (somehow) guaranty, that if the solver back track, it will then prune the search space using, amongst others, the SBPs.

• What is the differences (if any) in the context of Z3?
• How can I enforce the solve to use these axioms to prune the search space (when it back track)?
• Would the use of (quantifier) patterns for my SBAs helps?

Regards,

Aboubakr Achraf El Ghazi

Answer 1

In Z3 3.2, there are two main engines for handling quantified formulas: E-matching and MBQI (model based quantifier instantiation). E-matching is only effective in unsatisfiable formulas. Z3 will not be able to show that a formula is satisfiable using this engine. MBQI is more expensive, but it can show that several classes of formulas (containing quantifiers) are satisfiable. The Z3 guide describes these two engines (and other options). To use Z3 effectively on nontrivial problems, it is very useful to understand how these two engines work.

Symmetry breaking is usually very effective way to reduce the search space. It is hard to pinpoint exactly what is going on in your problem. I can see the following explanations for the non stable behavior:

• MBQI is having a hard time creating a model that satisfies the SBAs. Although the SBAs prune the search space, if the problem is satisfiable, Z3 will try to build an interpretation (model) that satisfies them. So, in this case, the SBA is just overhead. This is particularly true, if the input formula is very easy to satisfy, but becomes hard when you add the SBAs. You can confirm this hypothesis by using the option MBQI_TRACE=true. Z3 will display messages such as: [mbqi] failed k!18. Where k![line-number] is the quantifier id. You can assign your own ids using the tag :qid. Here is an example:

  (assert (forall ((x T) (y T)) (! (=> (and (subtype x y) (subtype y x)) (= x y)) :qid antisymmetry)))

BTW, you can disable the MBQI module using MBQI=false.

In future versions of Z3, we are planning to add an option to disable MBQI for some quantified formulas. This feature may be useful for SBAs.

• Another explanation is that E-matching is creating too many instances of the SBAs. You can confirm that using the option QI_PROFILE=true. Z3 will dump information such as:

[quantifier_instances] antisymmetry : 12 : 1 : 2.00

The first number is the number of generated instances. If that is the source of the problem, one solution is to assign restrictive patterns for the SBAs that are generating too many instances. For example, Z3 will use (R ai aj) as a pattern for SBA(R, A)_upToDiag. This kind of pattern may create a quadratic number of instances. Another experiment consists in disabling E-matching. Example, the option

AUTO_CONFIG=false EMATCHING=false MBQI=true

You may also try to disable relevancy propagation in the configuration above, option: RELEVANCY=0.

Finally, another option is to generate the instances of the SBAs that you believe are useful, and remove the quantified formulas.