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

我试图解决的问题很简单（我猜:)），但是因为我是 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,...]
]

我的目标是对列的值求和，然后发现所有总和的最大值，然后最小化该值并再次执行此操作，直到无法最小化所有列的总和的最大值......

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

提前致谢！

标签： z3z3py

最初，我以为您是在尝试解决某个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)