Z3最大化API:可能存在错误? [英] Z3 maximization API: possible bug?

问题描述

我目前正在使用Z3的最大化API(选择分支)，但偶然发现了以下错误:

I'm currently playing with the maximization API for Z3 (opt branch), and I've stumbled upon a following bug:

每当我给它一个无穷大的问题时，它都会简单地返回我OPT并在结果模型中给出零(例如，最大化Real('x')且对该模型没有约束).

Whenever I give it any unbounded problem, it simply returns me OPT and gives zero in the resulting model (e.g. maximize Real('x') with no constraints on the model).

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.

And I get the value of out to be 1 (OPT), while it seems like it should be -1.

推荐答案

感谢您试用此实验分支. 这些天，开发工作仍在进行中，但大多数功能都相当稳定，欢迎您试用一下.

Thanks for trying out this experimental branch. Development is still churning quite a bit these days, but most of the features are reasonably stable and you are invited to try them out.

回答您的问题.有一种本机方式可以使用Z3中的优化功能. 为了说明您的示例，以下是相关的内容:

To answer your question. There is a native way to use the optimization features from Z3. To paraphrase your example, here is what is relevant:

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()

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

When running it, you will see the following output:

sat
oo
[x = 0]

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

The first line says that the assertions are satisfiable. The second line prints the value of the handle "h" under the satisfiabilty call.

句柄的值包含一个满足opt/maximize/opt.minimize调用所声明的最大化/最小化条件的表达式. 在这种情况下，表达式为"oo".这有点像"hack"，因为您将不得不猜测"oo"的含义是无穷大.如果将此值解释回Z3，则不会无穷大. (我在这里限制不使用非标准数字的Z3的使用，Z3的另一部分包含非标准数字，但这是另一回事.)

The value of the handle holds an expression that meets the maximization/minimization criteria declared by the call to opt.maximize/opt.minimize. In this case the expression is "oo". It is somewhat of a "hack" because it is going to be up to you to guess that "oo" means infinity. If you interpret this value back to Z3, you will not get infinity. (I am here restricting the use of Z3 where we don't expose non-standard numbers, there is another part of Z3 that includes non-standard numbers, but that is another story).

请注意，opt.maximize调用返回句柄"h"， 后来用于查询最佳值. 最后一行是满足约束条件的某些模型. 当目标受到限制时，模型将是 您所期望的，但是在这种情况下，目标是无限的. 没有无限的最佳价值.

Note that the opt.maximize call returns the handle "h", which is later used to query what was the optimal value. The last line is some model satisfying the constraints. When the objective is bounded, the model will be what you expect, but in this case the objective is unbounded. There is no finite best value.

尝试例如:

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的模型，这也是最大值.

This time you get a model that sets x = 10, and this is also the maximal value.

您也可以尝试:

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]

ε表示非标准数字(无穷小).您可以将其设置为任意小. 再次，该模型仅使用标准数字，因此它选择了一些数字，在这种情况下为9.

epsilon refers to a non-standard number (infinitesimal). You can set it arbitrarily small. Again the model uses only standard numbers, so it picks some number, in this case 9.

这篇关于Z3最大化API:可能存在错误?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！