每行选取一个元素求最小和，z3py返回unsat的问题排查

代码逻辑错误原因 #

核心问题出在ForAll量词的使用规则：

• 你之前给ys添加的「每个y_i必须属于对应行元素」的约束，仅对作为自由变量的ys生效。而ForAll(ys, sum(xs) <= sum(ys))中的ys是独立的全称量化变量，不受求解器之前添加的任何约束限制，可以取任意整数值。
• 显然可以构造出sum(ys)无限小于sum(xs)的情况（比如所有y_i都取极小的负整数），这个约束永远不可能满足，因此求解器直接返回unsat。

另外你手动计算的最小和-214有误，该数组每行取最小元素相加的结果为12 + (-92) + (-59) + (-99) + (-92) = -330。

修正方案 #

方案1：使用Optimize类直接求最小值（推荐） #

找最小和的场景不需要用量词，直接用z3提供的优化器求解即可，写法更简洁不易出错：

from z3 import Int, Or, Optimize

ARR = [
    [36, 12, 90, 88, 82],
    [-92, 50, 40, 31, 43],
    [81, 28, -26, 8, -59],
    [18, -99, -70, -33, 58],
    [44, -33, 24, -92, -68],
]

opt = Optimize()
xs = [Int(f"x_{i}") for i, row in enumerate(ARR)]
for x, row in zip(xs, ARR):
    opt.add(Or(*[x == val for val in row]))

# 声明优化目标：最小化元素和
opt.minimize(sum(xs))
print(opt.check())
model = opt.model()
print("选取元素：", [model[x].as_long() for x in xs])
print("最小和：", sum(model[x].as_long() for x in xs))

运行输出：

sat
选取元素： [12, -92, -59, -99, -92]
最小和： -330

方案2：保留全称量词的正确写法 #

如果你一定要用量词逻辑来证明当前xs的和是全局最小，需要把ys的取值约束写到全称量词的蕴含条件内：

from z3 import Solver, Int, ForAll, Or, Implies, And

ARR = [
    [36, 12, 90, 88, 82],
    [-92, 50, 40, 31, 43],
    [81, 28, -26, 8, -59],
    [18, -99, -70, -33, 58],
    [44, -33, 24, -92, -68],
]

s = Solver()
xs = [Int(f"x_{i}") for i, row in enumerate(ARR)]
ys = [Int(f"y_{i}") for i, row in enumerate(ARR)]
for x, row in zip(xs, ARR):
    s.add(Or(*[x == val for val in row]))

# 将y的取值约束放到全称量词的蕴含条件中
y_constraints = And(*[Or(*[y == val for val in row]) for y, row in zip(ys, ARR)])
s.add(ForAll(ys, Implies(y_constraints, sum(xs) <= sum(ys))))
print(s.check())
model = s.model()
print("选取元素：", [model[x].as_long() for x in xs])
print("最小和：", sum(model[x].as_long() for x in xs))

该代码可正常返回sat，运行结果和方案1一致。

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