z3opt python - 최소화 사각형

Question

사각형과 관련된 문제를 최소화하기 위해 z3을 사용하는 것이 좋습니다. 나는 (파이썬 3 z3opt)이 간단한 예제를 작성할 때 :

unknown 
(incomplete (theory arithmetic)) 
-1*oo 
[b = 0, cost = 30, a = 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()) 

체크는 "알 수없는"를 반환 z3의? 당신이 비선형 목적을 최적화하려고하는 반면

Answer 1

모두 νZ - An Optimizing SMT Solver 및 νZ - Maximal Satisfaction with Z3 명시 적, 선형 산술 최적화가 지원되는지 언급.

비선형 목표이 사소한 기능이 아니기 때문에 작성자가 언급 한 것 같습니다.

---

해결 방법. 예를 들어, 의 비용이 인 경우 문제 해결 방법을 사용할 수 있습니다. 이는 양수 및 독립적 인 가중치의 합으로 나타납니다. 따라서,

(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 그것은별로 도움이되지 않을 수도 있습니다.