
Hi, I've post this under "Issues", but as this is the first time I use this forum, I don't know if it's ok there...
Hi, I'm using Z3 version "[version 4.3.1  64 bit]" and it seems to get stuck with this simple smt2 problem:
(declarefun x0 () Int)
(declarefun x1 () Int)
(declarefun x2 () Int)
(assert (> (+ (* 21 x0) (* 67 x1) (* 10 x2) ) 85))
(assert (> (+ (* 91 x0) (* 86 x1) (* 27 x2) ) 6))
(assert (< (+ (* 14 x0) (* 20 x1) (* 3 x2) ) 94))
(assert (= (+ (* 89 x0) (* 25 x1) (* 86 x2) ) 32))
(assert (< (+ (* 99 x0) (* 12 x1) (* 38 x2) ) 96))
(checksat)
Is this a bug?.
Thanks.


Coordinator
Jul 13, 2014 at 12:12 AM

This was also posted as Issue #122 if I'm not mistaken. It looks like this is simply a hard problem, at least for Z3.
Of course, it's fine to post such things either as discussions or issues. Here in the discussions section people other than the Z3 team are invited to comment too.



Hi, thanks for your answer :).
I'm generating random linear problems and I'm seeing that when number of variables is greater than the number of assertions, z3 takes a long time to solve the query. I know just a little bit about simplex and Gomory cuts and I don't understand why this happens.
Does anybody know if this slowdown is because of the intrinsic complexity of this problems (more variables than assertions + integer problem), or if it's something particular of Z3 implementation?. Do you know where can I find more information about this behavior?.
Thanks !!

