Z3最大化API:可能的错误？

Question

我目前正在使用Z3的最大化API (opt分支)，我偶然发现了以下一个bug：

每当我给它任何无界问题时，它只会返回OPT，并在结果模型中给出零(例如，最大化Real('x')，而模型上没有约束)。

Python示例：

from z3 import *

context = main_ctx()
x = Real('x')
optimize_context = Z3_mk_optimize(context.ctx)
Z3_optimize_assert(context.ctx, optimize_context, (x >= 0).ast)

Z3_optimize_maximize(context.ctx, optimize_context, x.ast)
out = Z3_optimize_check(context.ctx, optimize_context)
print out

我得到out的值是1 (OPT)，而它似乎应该是-1。

Answer 1

谢谢你尝试这个实验分支。这些天来，开发仍然相当频繁，但大多数特性都相当稳定，请您试用它们。

回答你的问题。有一种使用来自Z3的优化特性的原生方法。套用您的例子，下面是相关的内容：

from z3 import *

x = Real('x')
opt = Optimize()
opt.add(x >= 0)
h = opt.maximize(x)
print opt.check()
print opt.upper(h) 
print opt.model()

运行它时，您将看到以下输出：

sat
oo
[x = 0]

第一行说断言是可满足的。第二行在满意性调用下打印句柄"h“的值。

句柄的值保存一个表达式，该表达式满足对opt.max/opt.Minimum的调用声明的最大化/最小化标准。在本例中，表达式为"oo“。这有点像“黑客”，因为你可以猜到"oo“意味着无穷大。如果将此值解释回Z3，则不会得到无穷大。(我在这里限制Z3的使用，在这里我们不公开非标准数字，Z3的另一部分包含非标准数字，但这是另一个故事)。

注意，opt.maximize调用返回句柄"h"，该句柄稍后用于查询什么是最优值。最后一行是满足约束条件的模型。当目标有界时，模型将是您所期望的，但在这种情况下，目标是无界的。没有有限的最佳值。

例如，尝试：

x = Real('x')
opt = Optimize()
opt.add(x >= 0)
opt.add(x <= 10)
h = opt.maximize(x)
print opt.check()
print opt.upper(h) 
print opt.model()

这一次，您得到了一个设置x= 10的模型，这也是最大值。

你也可以尝试：

x = Real('x')
opt = Optimize()
opt.add(x >= 0)
opt.add(x < 10)
h = opt.maximize(x)
print opt.check()
print opt.upper(h) 
print opt.model()

现在的产出是：

sat
10 + -1*epsilon
[x = 9]

epsilon是指一个非标准数(无限小).你可以把它设得很小。同样，模型只使用标准数字，因此它选择一些数字，在本例中是9。