Determine upper/lower bound for variables in an arbitrary propositional formula [closed]

Question

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

Some variables may be unbounded. In this case, an algorithm should conclude that there's no upper/lower bound for those variables.

e.g., PHI = (x=3 AND y>=1). The upper and lower bound for x are both 3. The lower bound for y is 1, and y does not have an upper bound.

This is a very simple example, but is there a solution in general (perhaps using SMT solver)?

Aleen

This paper answers exactly this question: cs.utoronto.ca/~aws/papers/popl14.pdf The bounds are systematically discovered through an iterative sampling approach. Unbounded variables are also discovered in the process. – Aleen

This question appears to be off-topic because it is about determining the bounds of a formula. – Earthnut

Answer 1

This assumes the SAT/UNSAT domain of each variable is continuous.

1. Use an SMT solver to check for a solution to the formula. If there's no solution then that means no upper/lower bounds, so stop.
2. For each variable in the formula, conduct two binary searches over the domain of the variable, one searching for the lower bound, the other for the upper bound. The starting value in the search for each variable is the value for the variable in the solution found in step 1. Use the SMT solver to probe each search value for satisfiability and methodically bracket the bounds for each variable.

Pseudo code for the search functions, assuming integer 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 are the smallest/largest values representable in the domain of each variable. If lower_bound returns -inf then the variable has no lower bound. If upper_bound returns +inf then the variable has no upper bound.

Cohabit

Answer 2

In practice most of such optimization problems require some sort of iterate-until-maximum/minimum kind of external driver on top of the SMT solver. Quantified approaches are also possible that can leverage the particular capabilities of the SMT solvers, but in practice such constraints end up being too hard for the underlying solver. See this discussion in particular: How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related)

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

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 states x=3, y=1 maximizes x with respect to the predicate x==3 && y>=1. The second result says there is no value that maximizes y with respect to the same predicate. Third call says x=3,y=1 minimizes the predicate with respect to x. Fourth call says x=3,y=1 minimizes the predicate with respect to y. (See http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34 for details.)

You can also use the option "Iterative" (instead of Quantified) to have the library do the optimization iteratively instead of using quantifiers. These two techniques are not equivalent as the latter can get stuck in a local minima/maxima, but iterative approaches might solve problems where the quantified version is way too much to handle for the SMT solver.

Fain