当我玩 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不稳定分支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 不应该最大化目标 (+ x y) 吗?
问候, 约翰
最佳答案
默认情况下,Z3 一次解决一个目标,并找到按字典顺序排列的最佳解决方案。首先,它试图满足来自“第一”的尽可能多的软约束。与软约束关联的权重是对不满足约束的惩罚。也就是说,它不是奖励,因此最大惩罚是 4 (= 1 + 3),并且有可能满足这两个约束,从而惩罚为 0。 这是其他 max-sat 求解器和格式中使用的约定。 也许会令人困惑,因为它暗示最小化惩罚。
由于目标一次解决一个,很明显其他软约束都无法满足,因此 nuz 返回“第二”和“第三”的最大惩罚。
对于(最大化(+ x y))目标,“第一个”的等式限制了 x 和 y 的值。
关于optimization - NUZ : Use of soft-assertions with weights and ids,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30796941/