z3opt python -- 最小化平方

Question

我正在考虑使用 z3 来尽量减少涉及正方形的问题。但是当我写这个简单的例子（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())

支票returns"unknown":

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

我是不是以错误的方式定义了问题，或者这是 z3 的固有限制？

Answer 1

两者 νZ - An Optimizing SMT Solver and νZ - Maximal Satisfaction with Z3 都明确提到支持 线性算术优化 ，而您正在尝试优化 非线性 objective 。

我想如果支持非线性objectives，作者会提到它，因为它不是次要功能。

解决方法。 在您的示例中，您显然可以使用解决方法来解决此问题，因为 cost 由两个的总和给出正独立加数，例如将问题转化为字典优化问题，首先最小化 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)
)

但我想这是针对更大问题的最小示例，因此可能没有太大帮助。

z3opt python -- 最小化平方

z3opt python -- minimizing square

python

z3

z3py