Z3通过索引而不是值进行优化

Question

非常尊重@alias的答案:(找到最小和)我想解决类似的难题。拥有4家代理商，4种作品。每个代理都对某个价格起作用(参见代码中的initial矩阵)。我需要找到agent对特定工作的最优分配。下面的代码几乎是从上面提到的答案复制粘贴过来的:

initial = (  # Row - agent, Column - work
(7, 7, 3, 6),
(4, 9, 5, 4),
(5, 5, 4, 5),
(6, 4, 7, 2)
)
opt = Optimize()    
agent = [Int(f"a_{i}") for i, _ in enumerate(initial)]
opt.add(And(*(a != b for a, b in itertools.combinations(agent, 2))))
for w, row in zip(agent, initial):
opt.add(Or(*[w == val for val in row]))
minTotal = Int("minTotal")
opt.add(minTotal == sum(agent))
opt.minimize(minTotal)
print(opt.check())
print(opt.model())

数学正确答案:[a_2 = 4, a_1 = 5, a_3 = 2, a_0 = 3, minTotal = 14]不适合我，因为我需要得到代理的索引。现在，我的问题-如何重新编写代码来优化索引而不是值?我试图利用Array，但不知道如何最小化多个总和。

Answer 1

您可以简单地跟踪索引并遍历每一行以选择相应的元素。注意，itertools.combinations可以被Distinct代替。我们还添加了额外的检查，以确保索引在1和4之间，以确保没有越界访问:

from z3 import *
initial = (  # Row - agent, Column - work
(7, 7, 3, 6),
(4, 9, 5, 4),
(5, 5, 4, 5),
(6, 4, 7, 2)
)
opt = Optimize()
def choose(i, vs):
if vs:
return If(i == 1, vs[0], choose(i-1, vs[1:]))
else:
return 0
agent = [Int(f"a_{i}") for i, _ in enumerate(initial)]
opt.add(Distinct(*agent))
for a, row in zip(agent, initial):
opt.add(a >= 1)
opt.add(a <= 4)
opt.add(Or(*[choose(a, row) == val for val in row]))
minTotal = Int("minTotal")
opt.add(minTotal == sum(choose(a, row) for a, row in zip (agent, initial)))
opt.minimize(minTotal)
print(opt.check())
print(opt.model())

这个打印:

sat
[a_1 = 1, a_0 = 3, a_2 = 2, a_3 = 4, minTotal = 14]

我相信这就是你要找的。

注意z3还支持数组，您可以使用它来解决这个问题。然而，在SMTLib中，数组不是"有界的";就像编程语言一样。它们由域类型的所有元素索引。因此，这样做不会给您带来太多好处，而上面的公式似乎是最直接的。