Блог

Найдите минимальную сумму элементов с одним элементом из каждой строки. Я думаю, что ответ -214, но z3py возвращается неудовлетворенным. Что случилось?

 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) lt;= sum(ys))) print(s.check()) # unsat  

Ваша кодировка не совсем верна. Если вы вставите в свою программу следующую строку:

 print(s.sexpr())  

Вы увидите, что он печатает, среди прочего:

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

И именно по этой причине это так unsat . Это количественная формула, и, следовательно, она говорит, что она выполнима только в том случае, если формула верна для всех значений y_0 … y_4 . Это, очевидно, не так, и, следовательно unsat , результат.

Вместо этой формулировки вы должны использовать механизм оптимизации z3. Выберите по одной переменной из каждой строки, добавьте их и minimize получите результат. Что-то вроде этого:

 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())  

Когда я запускаю это, я получаю:

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

То есть решатель выбирает 12 из первой строки, -92 из второй, -59 из третьей, -99 из четвертой и -92 из последней строки; за минимальную сумму -330 .

Легко видеть, что это правильное решение, так как решатель выбирает минимальный элемент из каждой строки, и, следовательно, их сумма также будет минимальной. (Я не уверен, почему вы ожидали -214 , что это будет ответом.)