Z3 在 Python 中未显示无界优化的无穷大

Question

我是 Z3 的新手，尝试找到 here 中的示例，实现 python 中的示例。当我尝试“无限目标”部分中的示例时，我得到看似随机的整数值（不是 'oo'）。对于以下代码：

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 的输出吗？

我在 Pycharm 2021.2.1 上使用 python 3.9，Z3 版本 4.8.15。

Answer 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 时没有意义；因为目标不是正确的整数值。

Z3 在 Python 中未显示无界优化的无穷大

Z3 Not Showing Infinity on Unbounded Optimization in Python

python

z3

z3py