如何最小化列的总和的最大值？

Question

我试图解决的问题很简单（我猜:)），但因为我是z3的新手，我总是遇到编译错误。

我的问题：

[ [var_0_1, var_0_2, var_0_3,...]
, [var_1_1, var_1_2, var_1_3,...]
, [var_2_1, var_2_2, var_2_3,...]
]

我的目标是对列的值求和，然后发现所有总和的最大值，然后将该值最小化并再次执行此操作，直到最大限度地减少所有列的总和的最大值为止...

我希望你理解我的问题因为我的英语不是很好:)

提前致谢！

Answer 1

最初，我认为你试图解决一些minmax()问题，因为你说你想要解决

minimize(max(sum(var01,Var11,Var21),sum(var02,Var12,Var22), etc...))

在评论中。然而，进一步的要求启发表明它不可能是minmax()的一个例子，所以我放弃了这个想法，并没有进一步考虑它。

---

现在，您自己发布的解决方案是伪装的maxmin()的一个实例。我不确定这是否真的解决了你的初始问题。但是，如果是这种情况，那么我建议您尝试使用以下编码而不是基于ite的解决方案[参考：tacas15，tacas15_extended]。

（注意：cost应该是与cost_i相同类型的新变量，它是为解决maxmin()目标而宣布的。其他所有cost_i都是从目标降级为简单术语）

我相信这种方法有一定的机会比另一种更好。

---

编辑：a = 0的源代码示例：

goal = Real("cost")
for y in zip(*time):
    s.add(sum(y) <= goal)
result = s.minimize(goal)

如果你想复制a = 50的情况：

goal = Real("cost")
for y in zip(*time):
    s.add(sum(y) <= goal)
s.add(50 <= goal)
result = s.minimize(goal)

Answer 2

函数min（max（））：

def maxi(a,b):
  return If(a>=b,a,b)

a = 0
for y in zip(*time): #time is a list with many rows and columns
  z = sum(y)         #z receives the sum of the columns
  a = maxi(a,z)     

o.minimize(a)