私はZ3（目的関数）を経由してMaxSMT Z3

Question

加重チュートリアルと、次の例に出くわした：私はZ3の出力を理解していない

(declare-const a Bool) 
(declare-const b Bool) 
(declare-const c Bool) 
(assert-soft a :weight 1 :id A) 
(assert-soft b :weight 2 :id B) 
(assert-soft c :weight 3 :id A) 
(assert (= a c)) 
(assert (not (and a b))) 
(check-sat) 
(get-model) 

：

A |-> 0 
    B |-> 2 
    sat 
    (model (define-fun c() Bool true) 
    (define-fun b() Bool false) 
    (define-fun a() Bool true)) 

私の理解では、ということです加重MaxSMTはブール式の加重合計を最大化しようとします。したがって、aとcの両方が真でbは偽であるので、A | - > 4とB | - > 0となるはずです。

Answer 1

assert-softコールでは、その目標を満たさないことを選択した場合に発生する「ペナルティ」の値です。したがって、この割り当てでは、Z3はaおよびcをtrueとしてピックしているため、第1および第3の制約が満たされているため、ペナルティは発生しません。これは、このグループのすべてのソフト制約が満たされているので、A |-> 0を意味します。もちろん

は、trueはfalseするbを必要とするaとcを選んで、問題satを作るために、したがって、あなたはそれが制約グループに失敗したため2のペナルティを計上します。

z3はすべての規則的なassert制約を満たさなければならないことに注意してください。それに加えて、制約条件の「多くの」条件を満たすようにして、満たされていない場合のペナルティを最小限に抑えます。

このpaperには、Z3の最適化機能の優れた説明があります。