I don't know if this is an issue or I'm doing something wrong

Jul 10, 2014 at 10:24 AM
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:
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun 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))
(check-sat)
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.
Jul 14, 2014 at 8:42 AM
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 slow-down 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 !!