#z3 #z3py
Вопрос:
Найдите минимальную сумму элементов с одним элементом из каждой строки. Я думаю, что ответ -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
Комментарии:
1. Можете ли вы объяснить, как вы пришли к -214?
Ответ №1:
Ваша кодировка не совсем верна. Если вы вставите в свою программу следующую строку:
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
, что это будет ответом.)