z3opt python - 最小化正方形

Question

私は、正方形を含む問題を最小限に抑えるためにz3の使用を検討していました。私はこの単純な例（Pythonの3のz3opt）書くときしかし：

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は、明示的に、リニア算術演算の最適化がサポートされていることに言及します。

ノンリニアの目標がマイナーな機能ではないため、サポートされていた場合は、著者が言及していると思います。

---

回避策。あなたの例では、のコストがであるため、この問題を回避するには回避策を使用することができます。これは2つの和の合計で与えられます。正と独立の加算はです。したがって、

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

を取得しかし、私は、これは大きな問題のため最小限例です推測：あなたが最初aを最小限にして、bする辞書最適化問題に問題を回しますそれはあまり役に立たないかもしれません。