z3opt python - Quadrat minimieren

Question

Ich überlegte, z3 zu verwenden, um Probleme mit Quadraten zu minimieren. Aber wenn ich dieses einfache Beispiel (z3opt in Python 3) schreiben:

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

Die Kontrolle gibt „unbekannt“:

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

Bin ich das Problem in der falschen Art und Weise definiert, oder ist dies eine intrinsische Einschränkung von z3?

Answer 1

Sowohl νZ - An Optimizing SMT Solver und νZ - Maximal Satisfaction with Z3 ausdrücklich erwähnen, dass Linear Arithmetic Optimierung wird unterstützt, während Sie ein nichtlinearen Ziel zu optimieren versuchen.

Ich denke, die Autoren würden es erwähnen, wenn nichtlineare Objektive unterstützt wurden, da es kein Nebenmerkmal ist.

---

Abhilfe. In Ihrem Beispiel können Sie offensichtlich eine Problemumgehung verwenden, um dieses Problem zu überwinden, da Kosten durch die Summe von zwei positiven und unabhängigen Summanden , z. drehen Sie das Problem in ein Problem lexicographic Optimierung, in dem Sie zuerst a minimieren und dann 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) 

und

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

bekommen, aber ich denke, das ist ein für ein größeres Problem minimal Beispiel ist, so es könnte nicht viel helfen.