Чи є спосіб максимізувати суму за допомогою мінімальних записів зі списку? - z3, z3py

Я намагаюся знайти мінімальну кількість записів у списку або векторі, які становлять максимальну суму. Чи є спосіб його знайти? Я намагаюся наступним чином, але не успіхом:

D=[[Real("d%s%s" % (i+1,j+1)) for j in range(input)] for i in range (input)]
dr=[D[i][j]== randint(1,5) for i in range (input) for j in range (input)]

G=[[Real("g%s%s" % (i+1,j+1)) for j in range(input)] for i in range (input)]
ge=[G[i][j]==randint(1,5) for i in range (input) for j in range (input)]

dSum = [Real("dSum%s" % (i+1)) for i in range(input)]
gSum = [Real("gSum%s" % (i+1)) for i in range(input)]



benefit = [B[i]==If(dSum[i]>=gSum[i],(dSum[i]-gSum[i]),(gSum[i]-dSum[i])) for i in range(input)]

opt = Optimize()
opt.add(dr)
opt.add(ge)
opt.add([dSum[i]==sum(D[i]) for i in range(input)])
opt.add([gSum[i]==sum(G[i]) for i in range(input)])
opt.add(benefit)
opt.add(sumVal==sum(B))

ось тут мені потрібна допомога:

opt.minimize(B(i) i in range (len(benefit))) #is it wrong?
opt.maximize(sumVal)

Відповіді:

Я думаю, ви могли мати на увазі:

for i in range(len(benefit)):
opt.minimize(B[i])

Однак на ваше запитання "не можна правильно відповісти в його поточному стані з кількох причин:

1) Які ви є вільними зміннимимаксимізація / мінімізація? Мені здається, що всі змінні у вашій моделі повністю обмежені певними постійними значеннями за вашими визначеннями D і G.

2) Як ви очікуєте, що Z3 поводиться, коли ви просите його одночасно максимізувати sumVal і мінімізувати B[i]? Що коли sumVal не є максимальним, коли B[i] мінімальний чи навпаки?

3) Ви не визначили B[i] або sumVal, вам чогось такого не вистачає ?:

B=[Real("b%s" % (i+1)) for i in range (input)]
sumVal = Real("sumVal")