performance - Z3 real arithmetic and statistics

Question

Given a problem that is encoded using Z3's reals, which of the statistics that Z3 /smt2 /st produces might be helpful in order to judge if the reals engine "has problems/does lots of work"?

In my case, I have two mostly equivalent encodings of the problem, both using reals. The "small" difference in the encoding, however, makes a big difference in runtime, namely, that encoding A takes 2:30min and encoding B 13min. The Z3 statistics show that conflicts and quant-instantiations are mostly equivalent, but others are not, for example grobner, pivots and nonlinear-horner.

The two different statistics are available as a gist.

EDIT (to address Leo's comment):

The SMT2-encoding generated by both versions is ~30k lines and the assertions where reals are used are sprinkled all over the code. The main difference is that encoding B uses lots of underspecified real-typed constants from the range 0.0 to 1.0 that are bounded by inequalities, e.g. 0.0 < r1 < 1.0 or 0.0 < r3 < 0.75 - r1 - r2, whereas in encoding A lots of these underspecified constants have been replaced with fixed real values from the same range, e.g., 0.1 or 0.75 - 0.01. Both encodings use non-linear real arithmetic, e.g. r1 * (1.0 - r2).

A few random examples from the two encodings are available as a gist. All occurring variables are underspecified reals as described above.

PS: Does introducing aliases for fixed real values, e.g.,

(define-sort $Perms () Real)
(declare-const $Perms.$Full $Perms)
(declare-const $Perms.$None $Perms)
(assert (= $Perms.Zero 0.0))
(assert (= $Perms.Write 1.0))

inflict significant performance penalties?

Answer 1

The new nonlinear arithmetic solver is only used on problems that contain only arithmetic. Since your problem uses quantifiers, the new nonlinear solver will not be used. Thus, Z3 will use the old approach based on a combination of: Simplex (pivots stat), Groebner Basis (groebner stat), and Interval Propagation (horner stat). This is not a complete method. Moreover, based on the fragments you posted in gist, Groebner basis will not be very effective. This method is usually effective on problems that contain a lot of equalities. So, it is probably just overhead. You can disable it by using option NL_ARITH_GB=false. Of course, this is just a guess based on the problem fragment you posted.

The differences between encoding A and B are substantial. Encoding A is essentially a linear problem, since several constants were fixed to real values. Z3 was always complete for linear arithmetic problems. So, this should explain the difference in performance.

Regarding your question about aliases, the preferred way to introduce aliases is:

(define-const $Perms.$Zero $Perms 0.0)
(define-const $Perms.$Write $Perms 1.0)

Z3 also contains a preprocessor that eliminates variables using linear equations. This preprocessor is disabled by default in problems that contain quantifiers. This design decision is motivated by program verification tools that make extensive use of triggers/patterns in quantifiers. The variable elimination process may modify the careful designed triggers/patterns, and affect the total run-time. You can use the new tactic/strategy framework in Z3 to force it to apply this preprocessor. You can replace the command

(check-sat)

with

(check-sat-using (then simplify solve-eqs smt))

This strategy is telling Z3 to execute the simplifier, then solve equations (and eliminate variables) and then execute the default solver engine smt. You can find more about tactics and strategies in the following tutorial.