z3opt python -- minimizing square

Question

I was considering using z3 to minimize problems involving squares. But when I write this simple example (z3opt in python 3) :

from z3 import * a = Real('a') b = Real('b') cost = Real('cost') opt = Optimize() opt.add(a + b == 3) opt.add(And(a >= 0, a <= 10)) opt.add(And(b >= 0, b <= 10)) opt.add(cost == a * 10.0 + b ** 2.0) h = opt.minimize(cost) print(opt.check()) print(opt.reason_unknown()) print(opt.lower(h)) print(opt.model())

The check returns "unknown":

unknown (incomplete (theory arithmetic)) -1*oo [b = 0, cost = 30, a = 3]

Am I defining the problem in the wrong way or is this an intrinsic limitation of z3?

Patrick Trentin · Accepted Answer · 2016-07-15 08:46:25Z

Both νZ - An Optimizing SMT Solver and νZ - Maximal Satisfaction with Z3 explicitly mention that Linear Arithmetic Optimization is supported, whereas you are trying to optimise a non-linear objective.

I guess the authors would mention it if non-linear objectives were supported, since it is not a minor feature.

Workaround. In your example you can obviously use a workaround to get past this issue since cost is given by the sum of two positive and independent addends, e.g. turn the problem into a lexicographic optimization problem in which you first minimize a and then b:

(declare-fun a () Real) (declare-fun b () Real) (declare-fun cost () Real) (assert (= (+ a b) 3)) (assert (<= 0 a)) (assert (<= a 10)) (assert (<= 0 b)) (assert (<= b 10)) (assert (= cost (+ (* 10 a) (* b b)))) (minimize a) (minimize b) (check-sat) (get-model)

and get

sat (objectives (a 0) (b 3) ) (model (define-fun b () Real 3.0) (define-fun cost () Real 9.0) (define-fun a () Real 0.0) )

But I guess this is a minimal example for a larger problem, thus it might not be of much help.

Would you have a suggestion as to an alternative to z3 that could solve this? I was using it for its convenient interface (automatically building large systems of equations, of which most are linear) but find that I cannot get around this problem.
To the best of my knowledge, I don't know of any SMT solver that provides direct optimization procedures of non-linear objectives at the present time. I regret to say that my knowledge in related fields is not deep enough to suggest you some other tool to solve this problem. @GeromePistre

Collectives™ on Stack Overflow

z3opt python -- minimizing square

1 Answer 1

2 Comments

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

2 Comments

Related