求最小总和

Question

从每一行中找出一个元素的最小元素总和。我认为答案是 -214，但 z3py returns 不满意。怎么了？

from z3 import Solver, Int, ForAll, Or

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, y, row in zip(xs, ys, ARR):
    s.add(Or(*[x == val for val in row]))
    s.add(Or(*[y == val for val in row]))

s.add(ForAll(ys, sum(xs) <= sum(ys)))
print(s.check()) # unsat

Answer 1

您的编码不太正确。如果您在程序中加入以下行：

print(s.sexpr())

除其他外，您会看到它会打印：

(assert (forall ((y_0 Int) (y_1 Int) (y_2 Int) (y_3 Int) (y_4 Int))
  (<= (+ 0 x_0 x_1 x_2 x_3 x_4) (+ 0 y_0 y_1 y_2 y_3 y_4))))

这就是unsat的原因。这是一个量化公式，因此它表示只有当公式为真时才可满足 对于所有 值 y_0 .. y_4。这显然不是真的，因此 unsat 结果。

您应该使用 z3 的优化引擎来代替此公式。从每一行中选择一个变量，将它们相加，然后 minimize 结果。像这样：

from z3 import *

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],
]

o = Optimize()
es = [Int(f"e_{i}") for i, row in enumerate(ARR)]
for e, row in zip (es, ARR):
    o.add(Or(*[e == val for val in row]))

minTotal = Int("minTotal")
o.add(minTotal == sum(es))
o.minimize(minTotal)

print(o.check())
print(o.model())

当我运行这个时，我得到：

sat
[e_0 = 12,
 e_3 = -99,
 e_2 = -59,
 e_1 = -92,
 e_4 = -92,
 minTotal = -330]

也就是说，求解器从第一行选择 12，从第二行选择 -92，从第三行选择 -59，从第四行选择 -99，然后 -92 从最后一行开始；最小总和 -330.

很容易看出这是正确的解决方案，因为求解器从每一行中选择最小元素，因此它们的总和也将是最小的。（我不确定您为什么期望 -214 是答案。）

求最小总和

Find minimum sum

z3

z3py