z3opt python - минимизирующий квадрат

Question

Я рассматривал возможность использования z3 для минимизации проблем, связанных с квадратами. Но когда я пишу этот простой пример (z3opt в 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()) 

Проверка возвращает «неизвестный»:

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

ли я определение проблемы в неправильном направлении, или это внутреннее ограничение z3?

Answer 1

νZ - An Optimizing SMT Solver Как и νZ - Maximal Satisfaction with Z3 явно указать, что Linear Арифметика Оптимизация поддерживается, в то время как вы пытаетесь оптимизировать нелинейную задачу.

Я думаю, авторы упомянут об этом, если были поддержаны нелинейные цели , поскольку это не второстепенная функция.

---

Обход проблемы. В вашем примере вы, очевидно, можете использовать обходное решение, чтобы преодолеть эту проблему, поскольку стоимость задается суммой двух положительных и независимых добавок, например. превратить проблему в лексикографической задачи оптимизации, в которой вы первый минимизировать a, а затем 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) 

и получить

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) 
) 

Но я предполагаю, что это минимальный пример для большей проблемы, таким образом, это может быть не очень полезно.