nuZ：模型怎么说

Question

在玩 nuZ 时我偶然发现了这个：

(declare-fun x () Int)
(declare-fun y () Int)

(assert-soft (= x 1) :weight 1 :id first)
(assert-soft (= y 4) :weight 3 :id first)

(assert-soft (= x 2) :weight 1 :id second)
(assert-soft (= y 5) :weight 3 :id second)

(assert-soft (= x 3) :weight 1 :id third)
(assert-soft (= y 6) :weight 3 :id third)

(maximize (+ x y))

(check-sat)
(get-model)

给我这个结果（使用 Z3 unstable branch 4.4.0）：

first |-> 0
second |-> 4
third |-> 4
(+ x y) |-> 5
sat
(model
  (define-fun x () Int
    1)
  (define-fun y () Int
    4)
)

这里的“|->”是什么意思？

当提到软断言的id时，可能意味着放弃一些软断言的代价。当提到 objective 时，它看起来像是优化的结果。

还有更多吗？

此致，约翰

Answer 1

没有更多内容了。对于软约束，“|->”右边的数字给出如下。

假设我们断言（首先断言软 F1 :weight w1 :id ）（断言软 F2 :weight w2 :id first） (assert-soft F3 :weight w3 :id first)

并假设 M 是模型最大分配将真值分配给 F1、F2、F3 中的变量，因此我们可以将 M 中的公式计算为 0（假）或 1（真）。

那么|->右边就是数字：

     M(not(F1))*w1 + M(not(F2))*w2 + M(not(F3))*w3

MaxSat 解决方案最小化这个总和，或者双重最大化这个总和：

     M(F1)*w1 + M(F2)*w2 + M(F3)*w3

（未打印）。

nuZ：模型怎么说

nuZ: What does the model say

optimization

z3