The minimum and maximum value of the variable

Question

Let's look at a very simple constraint: solve (x> 0 & x <5)

Can z3 (or any other SMT solver or any other automatic technique) calculate the minimum and maximum values ​​of the variable x that satisfy the given constraint? (In our case, x_min = 1, x_max = 4)

Answer 1

As Leonardo noted, this has been discussed in detail before: Define the upper / lower boundary of variables in an arbitrary propositional formula . Also see: How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT) .

To summarize, you can either use a quantitative formula or go iteratively. Unfortunately, these methods are not equivalent:

• The quantitative approach does not require any iteration and can find global min / max in one call to the solver; at least in theory. However, this leads to more complex formulas. Thus, the backend solver can time out or simply return the "unknown".

• The iterative approach creates simple formulas for the backend solver that you have to deal with, but it can loop forever if there is no optimal value; The simplest example is to find the highest Int value. The quantitative version can solve this problem beautifully, quickly informing you that there is no such value, and the iterative version will continue indefinitely. This can be a problem if you do not know in advance that your limitations have an optimal solution. (Needless to say, a “sufficient” iteration counter is usually difficult to guess and may depend on random factors such as the seed used by the solver.)

Also keep in mind that if there is a special optimization algorithm for the problem domain, it is unlikely that a general-purpose SMT solver can outperform it.

Answer 2

Z3 does not support optimization (maximization / minimization) of objective functions or variables. We plan to add such features, but this will not happen this year. In the current version, we can “optimize” the objective function by solving several problems, where at each iteration we add additional restrictions. We know that we have found the optimum when the problem becomes unsatisfactory. Here is a small Python script that illustrates the idea. script maximizes the value of the X variable. To minimize it, we just need to replace s.add(X > last_model[X]) with s.add(X < last_model[X]) . This script is very naive, it performs a "linear search". It can be improved in many ways, but it demonstrates the basic idea.

You can also try the script online: http://rise4fun.com/Z3Py/KI1

See the following related question: Define upper / lower bounds for variables in an arbitrary propositional formula

 from z3 import * # Given formula F, find the model the maximizes the value of X # using at-most M iterations. def max(F, X, M): s = Solver() s.add(F) last_model = None i = 0 while True: r = s.check() if r == unsat: if last_model != None: return last_model else: return unsat if r == unknown: raise Z3Exception("failed") last_model = s.model() s.add(X > last_model[X]) i = i + 1 if (i > M): raise Z3Exception("maximum not found, maximum number of iterations was reached") x, y = Ints('x y') F = [x > 0, x < 10, x == 2*y] print max(F, x, 10000)