Как я могу минимизировать максимальную сумму моих столбцов?

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

Функция мин (макс ()):

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)