z3优化和软约束

Question

以下代码当

a

为

True

时将

only_2

设置为

True

，否则将

a

设置为

False

。我不明白，因为如果我们最小化软约束，我们应该总是选择概率最高的

a

。我缺少什么？如何最大限度地减少所有软约束？

from z3 import *
from math import exp

only_2 = True

pa1 = 0.8
pa2 = 0.8
pa3 = 0.2
pb1 = 0.7
pb2 = 0.8
pb3 = 0.2

a = Bool('a')
b = Bool('b')
a1 = Bool('a1')
a2 = Bool('a2')
a3 = Bool('a3')
b1 = Bool('b1')
b2 = Bool('b2')
b3 = Bool('b3')

all_xps = [(a1,pa1), (b1,pb1), (a2,pa2), (b2,pb2), (a3,pa3), (b3,pb3)]
all_as = [a1, a2, a3]
all_bs = [b1, b2, b3]

if only_2:
    all_xps = all_xps[0:-2]
    all_as = all_as[0:-1]
    all_bs = all_bs[0:-1]

s = Optimize()
for (x,p) in all_xps:
    s.add_soft(Not(x), exp(-p))
    s.add_soft(x, exp(-(1-p)))
s.add(Implies(And(*all_as), a))
s.add(Implies(Not(And(*all_as)), Not(a)))
s.add(Implies(And(*all_bs), b))
s.add(Implies(Not(And(*all_bs)), Not(b)))
s.add(Xor(a, b))

assert s.check() == sat
model = s.model()
print(model[a])

Answer 1

我发现：a3/b3 约束较小，因此它可能会失败其中任何一个，而不是落入更大的不平等约束。