Find minimum sum

Question

Find the minimum sum of elements with one element from each row. I think the answer is -214, but z3py returns unsat. What is wrong?

from z3 import Solver, Int, ForAll, Or

ARR = [
    [36, 12, 90, 88, 82],
    [-92, 50, 40, 31, 43],
    [81, 28, -26, 8, -59],
    [18, -99, -70, -33, 58],
    [44, -33, 24, -92, -68],
]

s = Solver()
xs = [Int(f"x_{i}") for i, row in enumerate(ARR)]
ys = [Int(f"y_{i}") for i, row in enumerate(ARR)]
for x, y, row in zip(xs, ys, ARR):
    s.add(Or(*[x == val for val in row]))
    s.add(Or(*[y == val for val in row]))

s.add(ForAll(ys, sum(xs) <= sum(ys)))
print(s.check()) # unsat

Answer 1

Your encoding isn't quite correct. If you stick the following line in your program:

print(s.sexpr())

You'll see that it prints, amongst other things:

(assert (forall ((y_0 Int) (y_1 Int) (y_2 Int) (y_3 Int) (y_4 Int))
  (<= (+ 0 x_0 x_1 x_2 x_3 x_4) (+ 0 y_0 y_1 y_2 y_3 y_4))))

And this is the reason why it is unsat. This is a quantified formula, and thus it says it is only satisfiable if the formula is true for all values y_0 .. y_4. This is obviously not true, and hence the unsat result.

Instead of this formulation, you should use z3's optimization engine. Pick one variable from each row, add them, and minimize that result. Something like this:

from z3 import *

ARR = [
    [36, 12, 90, 88, 82],
    [-92, 50, 40, 31, 43],
    [81, 28, -26, 8, -59],
    [18, -99, -70, -33, 58],
    [44, -33, 24, -92, -68],
]

o = Optimize()
es = [Int(f"e_{i}") for i, row in enumerate(ARR)]
for e, row in zip (es, ARR):
    o.add(Or(*[e == val for val in row]))

minTotal = Int("minTotal")
o.add(minTotal == sum(es))
o.minimize(minTotal)

print(o.check())
print(o.model())

When I run this, I get:

sat
[e_0 = 12,
 e_3 = -99,
 e_2 = -59,
 e_1 = -92,
 e_4 = -92,
 minTotal = -330]

That is, solver picks 12 from the first row, -92 from the second, -59 from the third, -99 from the fourth, and -92 from the last row; for a minimum sum of -330.

It's easy to see that this is the correct solution since the solver picks minimum element from each row, and thus their sum will be minimal as well. (I'm not sure why you were expecting -214 to be the answer.)