Define the upper / lower boundary of variables in an arbitrary propositional formula

Question

Given an arbitrary propositional PHI formula (linear constraints on some variables), what is the best way to determine the (approximate) upper and lower bounds for each variable?

Some variables may be unlimited. In this case, the algorithm should conclude that for these variables there is no upper / lower boundary.

e.g. PHI = (x = 3 AND y> = 1). The upper and lower bounds for x are 3. The lower bound for y is 1, and y has no upper bound.

This is a very simple example, but is there a solution at all (possibly using the SMT solution)?

Answer 1

This assumes that the SAT / UNSAT area of ​​each variable is continuous.

• Use the SMT solver to verify the solution of the formula. If there is no solution, this means no upper / lower boundaries, so stop.
• For each variable in the formula, perform two binary searches over the domain of the variable, one looking for the lower bound, the other for the upper bound. The initial value in the search for each variable is the value of the variable in the solution found in step 1. Use the SMT solver to check each search value for feasibility and methodically copy the boundaries for each variable.

Pseudo-code for search functions, assuming whole domain variables:

lower_bound(variable, start, formula) { lo = -inf; hi = start; last_sat = start; incr = 1; do { variable = (lo + hi) / 2; if (SMT(formula) == UNSAT) { lo = variable + incr; } else { last_sat = variable; hi = variable - incr; } } while (lo <= hi); return last_sat; } 

and

 upper_bound(variable, start, formula) { lo = start; hi = +inf; last_sat = start; do { variable = (lo + hi) / 2; if (SMT(formula) == SAT) { last_sat = variable; lo = variable + incr; } else { hi = variable - incr; } } while (lo <= hi); return last_sat; } 

-inf / + inf - the smallest / largest values ​​represented in the area of ​​each variable. If lower_bound returns -inf, then the variable has no lower bound. If upper_bound returns + inf, then the variable does not have an upper bound.

Answer 2

In practice, most of these optimization tasks require a kind of iterative-to-maximum / minimum external driver from their SMT solver. Quantitative approaches are also possible that can take advantage of the specific capabilities of SMT solvers, but in practice, such constraints are too complex for the main solver. See this discussion in particular: How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT)

Having said that, most high-level language bindings include the necessary mechanism to simplify your life. For example, if you use the Haskell SBV library for script z3, you can:

 Prelude> import Data.SBV Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) Just [3,1] Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) Nothing Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) Just [3,1] Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) Just [3,1] 

The first result of the state x = 3, y = 1 maximizes x relative to the predicate x == 3 && y> = 1. The second result says that there is no value that maximizes y relative to the same predicate. The third call says x = 3, y = 1 minimizes the predicate with respect to x. The fourth call says x = 3, y = 1 minimizes the predicate in y. (For more details see http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34 .)

You can also use the Iterative option (instead of Quantified) so that the library performs iterative optimization instead of using quantifiers. These two methods are not equivalent, since the latter can get stuck in local minima / maxima, but iterative approaches can solve problems when the quantitative version is too much to process the SMT solver.