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明确提到线性算术优化支持，而你试图优化非线性目标。

我想作者会提及它，如果支持非线性目标，因为它不是一个小功能。

---

解决方法。在您的示例中，显然可以使用解决方法来解决此问题，因为成本由两个正数和独立加数（例如，把这个问题变成一个字典优化问题在您第一次减少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) 
) 

但我想这是一个更大的问题小例子，从而它可能没有太大的帮助。