CODEWITHSUNDEEP
optimizationz3
George Karpenkov
George Karpenkov

Reputation: 2124

Z3 maximization API: possible bug?

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

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 example: 

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

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

Upvotes: 1

Views: 365

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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.

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]

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

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

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.

Try for example instead: 

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

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

You could also try:

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

The output is now:

sat
10 + -1*epsilon
[x = 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.

Upvotes: 2

Related Questions