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?


Answer: Both [νZ - An Optimizing SMT Solver](https://www.microsoft.com/en-
us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf) and [νZ - Maximal
Satisfaction with Z3](https://www.microsoft.com/en-us/research/wp-
content/uploads/2016/02/nbjorner-scss2014.pdf) 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.

