1

I have a problem in QF_LRA, which is solved surprisingly quickly by MathSAT5 (unsat, < 5 minutes) but Z3 does not seem to make much progress (no result even after 7 days). Could this be fixed by some settings in Z3?

It contains many clauses of (roughly) these 5 types:

(assert (or (< p47a2 p8a2) (< (+ p47a0 p47a2) (+ p8a0 p8a2)) (< (+ p47a0 p47a2 p47a3) (+ p8a0 p8a2 p8a3)) (and (= p47a2 p8a2) (= (+ p47a0 p47a2) (+ p8a0 p8a2)) (= (+ p47a0 p47a2 p47a3) (+ p8a0 p8a2 p8a3)))))
(assert (= 1.0 (+ p3887a0 p3887a1 p3887a2 p3887a3)))
(assert (>= p1715a0 0.0))    
(assert (= p133a2 p133a1))
(assert (or (= p379a1 0.0) (= p379a2 0.0)))

The complete problem instance can be downloaded from here in SMT2 format.

Key for solving it with MathSAT was the setting

preprocessor.simplification=8

which enables global rewriting rules (in addition to the application track settings of the SMT 2015 competition).

Is there anything similar in Z3 that I could try? Or any preprocessing / optimization of the encoding you would advise me to perform? I am relatively new to SMT; hence any help/guidance would be highly appreciated.

In the first place it would be great to get Z3 to solve this instance. As a next step I would also like to extract an unsat core, if that is important for your tipps.

Many thanks in advance!!

cgeist
  • 13
  • 3

1 Answers1

1

Replace (check-sat) with

(check-sat-using (then simplify solve-eqs (! smt :case_split 0 :relevancy 0 :auto_config false :restart_strategy 2)) :print_model true)

Z3 solves it in a minute. However, you can find better configuration here.

mmpourhashem
  • 91
  • 1
  • 6
  • Excellent answer! Many thanks!! I had a look at the tutorial and (help-tactic), but still find it difficult to find my own configuration. Is there a more detailed tutorial? – cgeist Jan 14 '16 at 18:26
  • BTW: even with core extraction enabled, the solving time is just below 3 minutes, which is great. Thanks again! – cgeist Jan 14 '16 at 18:27
  • Take a look at ["The Strategy Challenge in SMT Solving"](http://link.springer.com/chapter/10.1007/978-3-642-36675-8_2) paper by Leonardo de Moura et. al. In order to find the best configuration, it is better to compile Z3 in debug mode and check what Z3 is exactly doing after each step (simplifying, solving equations, ...). Check Leonardo's answer [here](http://stackoverflow.com/questions/13102789/printing-internal-solver-formulas-in-z3/13103031#13103031). – mmpourhashem Jan 15 '16 at 14:09