CODEWITHSUNDEEP
pythonz3z3py
Gerome Pistre
Gerome Pistre

Reputation: 467

z3opt python -- minimizing square

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?

Upvotes: 1

Views: 1479

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

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.

Upvotes: 3

Related Questions