Я новичок в Z3 и пробую примеры, найденные здесь, реализуя примеры в python. Когда я пробую примеры из раздела «Неограниченные цели», я получаю кажущиеся случайными целочисленные значения (не «оо»). Для следующего кода:
x, y = Ints('x y')
opt = Optimize()
opt.add(x < 2)
opt.add((y - x) > 1)
opt.maximize(x + y)
print(opt.check())
print(opt.model())
Я получаю вывод:
sat
[y = 5, x = 1]
Но проблема не ограничена, я ожидаю, что она даст мне y, равную бесконечности. Более простой пример:
x, y, profit = Ints('x y profit')
opt = Optimize()
opt.add(profit == 2*x + y)
opt.maximize(profit)
print(opt.check())
print(opt.model())
Этот пример дает мне:
sat
[x = 0, y = 0, profit = 0]
Мой вопрос: почему я не получаю бесконечность здесь? Я делаю что-то не так или это результат, который я должен ожидать от Z3 с python, когда я даю ему неограниченную проблему оптимизации?
Я использую Python 3.9 на Pycharm 2021.2.1, Z3 версии 4.8.15.
Вы не совсем правильно используете API. Вместо этого вы должны использовать функцию value
для цели оптимизации. Например, ваш второй запрос закодирован как:
from z3 import *
x, y, profit = Ints('x y profit')
opt = Optimize()
opt.add(profit == 2*x + y)
maxProfit = opt.maximize(profit)
print(opt.check())
print("maxProfit = ", maxProfit.value())
Это печатает:
sat
maxProfit = oo
Обратите внимание, что когда результатом оптимизации является oo
, то значения модели для x
/y
/profit
и т. д. не имеют значения. (Они больше не являются целыми числами.) Если результат оптимизации является конечным значением, вы можете посмотреть на opt.model()
, чтобы выяснить, какое назначение ваших переменных достигло оптимальной цели. Итак, значения x
/y
и profit
, которые вы получаете в своем примере, хотя и напечатаны как 0
, не имеют смысла; поскольку цель не является правильным целочисленным значением.