nuZ：使用带有权重和 ID 的软断言

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)
)

我不太明白输出结果。我知道第一步的重量是最大化的。

当权重相等时，nuZ 不应该最大化 objective (+ x y) 吗？

此致，约翰

Answer 1

默认情况下，Z3 一次解决 objective 一个问题，并找到字典顺序的最佳解决方案。首先，它尝试满足来自 "first" 的尽可能多的软约束。与软约束关联的权重是惩罚不满足约束。也就是说，它不是award，所以最大的penalty是4（=1+3），有可能同时满足两个约束使得penalty为0。这是其他 max-sat 求解器和格式中使用的约定。可能会造成混淆，因为它暗示要尽量减少处罚。

由于 objective 一次解决一个问题，因此很明显 none 其他软约束可以得到满足，因此 nuz returns 的最大惩罚"second" 和 "third".

对于 (maximize (+ x y)) objective，来自 "first" 的等式限制了 x 和 y 的值。

nuZ：使用带有权重和 ID 的软断言

nuZ: Use of soft-assertions with weights and ids

optimization

z3