CODEWITHSUNDEEP
z3
simon1505475
simon1505475

Reputation: 675

What is the importance of the order of the assertions in Z3?

I have two files whose content is identical except for the order in which I placed the assertions: in one file, the assertions are placed in the reverse order of the other. The first file (po-9.z3) is declared unsatifiable by Z3 in less than a second while the other (po.z3) cannot be verified within a minute.

What could be the reason for this difference? I assumed that placing the assertions that will be involved in the verification earlier in the file would improve performances. However, the one that passes verification (po-9.z3) has most of the relevent / problem specific assertions at the bottom of the file. Also, in po.z3, while the theorem to be proved and the assumptions are at the top of the file, one important assertion (a first order formulation for a lambda expression) is put at the bottom of the file. When I bring it to the top, po.z3 verifies within less than a second.

What would be the best order for me to produce the assertions in a z3 smt2 file?

Upvotes: 3

Views: 544

Answers (1)

sean
sean

Reputation: 1832

What could be the reason for this difference?

SMT solvers implement DPLL(T) algorithm, which is a combination of (a variant of) the DPLL procedure and decision procedures.

Performance of DPLL is heavily affected by the choice of variables for branching. There are the cases of which the running time is constant or exponential depending on variable selection.

If the two formulas are logically equivalent (you need to double-check), then I think the only possibility is that, the different order in the two formulas leads to different order in variable selection, which eventually leads to difference in performance.

Upvotes: 5

Related Questions