CODEWITHSUNDEEP
z3
cgeist
cgeist

Reputation: 13

Speeding up Z3 on specific QF_LRA instances

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!!

Upvotes: 1

Views: 181

Answers (1)

mmpourhashem
mmpourhashem

Reputation: 91

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.

Upvotes: 1

Related Questions