search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.28k stars 1.48k forks source link

z3 Optimise class not able to maximize functions like x**2 or x*x #633

Closed aviralkumar2907 closed 8 years ago

aviralkumar2907 commented 8 years ago

I have written the following code. I want to maximize a given function based on some constraints, But the code I have written doesn't seem to work. The output follows the code.

from z3 import * x = Real('x'); o = Optimize(); o.add(x >= -3.0) o.add(x <= 2.0) y = Real('y') y = x_x h = o.maximize(x_x) print o print o.check() print o.reason_unknown() print o.model() print o.upper(h)

The output is shown below.

(declare-fun x () Real) (assert (>= x (- 3.0))) (assert (<= x 2.0)) (maximize (* x x)) (check-sat)

unknown (incomplete (theory arithmetic)) [x = 0] oo

Please help me put with this issue. I couldn't find any proper documentation regarding any restrictions on the functions which the maximize function can maximize. Thanks,

cheshire commented 8 years ago

@aviralkumar2907 As the error message says, the nonlinear solver module in Z3 is incomplete, and may or not succeed depending on the exact structure of the problem.

The solving reliably works only for the linear case, for both reals and integers, running simplex and MIP respectively. This information is in fact stated in the official Z3 OPT tutorial (http://rise4fun.com/Z3Opt/tutorial/guide)

NikolajBjorner commented 8 years ago

Quadratic programming and general non-linear constraints are not supported. If we get enough good use cases it may be nice to look into it.

NikolajBjorner commented 8 years ago

Closing as this isn't supported