3

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?

simon1505475
  • 675
  • 3
  • 9

1 Answers1

5

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.

sean
  • 1,632
  • 2
  • 15
  • 34
  • Thanks, that's good to know. Is there any way of predicting the effect that the order will have? In other words, since I generate the z3 files, how could I choose the order of the assertions so as to maximize the chances that z3 won't timeout too often on easy input? – simon1505475 Jun 24 '14 at 07:24
  • 1
    Variable selection is a heuristic, and often includes randomness. So I don't how to make your formula easier for z3. You may want to look at the function `solver::next_var()` in http://z3.codeplex.com/SourceControl/latest#src/sat/sat_solver.cpp , to see how the heuristic works. – sean Jun 24 '14 at 22:09
  • Can you please help me to find the mapping between the numbers (0 to `num_vars()`) and the "name" of variables? Actually, I am trying to change the similar code in smt_case_split_queue.cpp . – mmpourhashem Feb 12 '16 at 14:07