Z3 Optimize软约束疑问：为何a的取值不符合概率最优？

问题描述 #

当代码中only_2设为True时，a被赋值为True；设为False时，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])

问题根源 #

1. 软约束权重逻辑错误：
   原代码使用exp(-p)和exp(-(1-p))作为软约束权重，无法正确映射概率的似然性。正确的做法是使用负对数似然作为惩罚权重：

   • 当变量x取True（概率p），惩罚应为-log(p)（违反Not(x)约束的代价）
   • 当变量x取False（概率1-p），惩罚应为-log(1-p)（违反x约束的代价）
     这样最小化总惩罚等价于最大化变量赋值的联合概率，符合“选择概率最高组合”的目标。

2. 对约束目标的误解：
   由于Xor(a,b)硬约束，必须在(a=True,b=False)和(a=False,b=True)两个组合中选择，不能单独看a的边缘概率。需要比较这两个组合的联合概率，而非a或b的单独概率。

修正后的代码 #

from z3 import *
from math import log

only_2 = False

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:
    # x为True时，违反Not(x)，代价为负对数概率
    s.add_soft(Not(x), -log(p))
    # x为False时，违反x，代价为负对数概率
    s.add_soft(x, -log(1-p))

# 简化等价约束写法
s.add(a == And(*all_as))
s.add(b == And(*all_bs))
s.add(Xor(a, b))

assert s.check() == sat
model = s.model()
print(f"a = {model[a]}")
print(f"b = {model[b]}")
# 打印所有变量赋值，便于验证
for var in [a1,a2,a3,b1,b2,b3]:
    print(f"{var} = {model[var]}")

说明 #

• 修正后的权重计算正确映射了概率与惩罚的关系，总惩罚最小化对应联合概率最大化。
• 当only_2=False时，(a=True,b=False)组合的最优赋值（a1,a2,a3=True；b1,b2=True,b3=False）联合概率高于(a=False,b=True)的最优组合，因此Z3会选择a=True，符合预期。
• 若需优先考虑a的边缘概率而非联合概率，需调整硬约束或优化目标，但这会违背Xor(a,b)的原始约束逻辑。

内容的提问来源于stack exchange，提问作者namin