Z3 не показывает бесконечность при неограниченной оптимизации в Python

Я новичок в 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.

Почему в Python есть оператор "pass"?
Почему в Python есть оператор "pass"?
Оператор pass в Python - это простая концепция, которую могут быстро освоить даже новички без опыта программирования.
Некоторые методы, о которых вы не знали, что они существуют в Python
Некоторые методы, о которых вы не знали, что они существуют в Python
Python - самый известный и самый простой в изучении язык в наши дни. Имея широкий спектр применения в области машинного обучения, Data Science,...
Основы Python Часть I
Основы Python Часть I
Вы когда-нибудь задумывались, почему в программах на Python вы видите приведенный ниже код?
LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа
LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа
Алиса и Боб имеют неориентированный граф из n узлов и трех типов ребер:
Оптимизация кода с помощью тернарного оператора Python
Оптимизация кода с помощью тернарного оператора Python
И последнее, что мы хотели бы показать вам, прежде чем двигаться дальше, это
Советы по эффективной веб-разработке с помощью Python
Советы по эффективной веб-разработке с помощью Python
Как веб-разработчик, Python может стать мощным инструментом для создания эффективных и масштабируемых веб-приложений.
0
0
34
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Вы не совсем правильно используете 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, не имеют смысла; поскольку цель не является правильным целочисленным значением.

Другие вопросы по теме