SBV: programmatically driving the optimizer?

Learn
1

I’ve a small problem using SBV - specifically, I think I’m missing a trick to programmatically extract model values that arise from an optimization problem. Here’s a quick example:

main = do
    res <- runSMT $ do
        vs <- forM [1 .. 5] $ \i -> do
            x <- sInteger ("x" <> show i)
            constrain $ 1 .<= x .&& x .< 10
            maximize ("goal" <> show i) x
            pure x
        ifPasses $ do
            forM vs $ \v -> do
                getValue v
    print res

ifPasses output = do
    query $ do
        cs <- checkSat
        case cs of
            Sat -> do
                Just <$> output
            Unsat -> do
                pure Nothing

This is finding me a model that satisfies the constraints, but ignores the optimisation requirements: specifically, I see

Just [1,1,1,1,1]
  • is there a way to drive this using runSMT? (optimize Lexicographic will produce the correct result, but it seems much harder to extract the variable assignments from the result)
2

You do indeed have to use optimize, for example like this:

import Data.SBV
import Data.Foldable
main = do
    let vs = ["x" <> show i | i <- [1..5 :: Integer]]
    res <- optLexicographic $
        forM_ vs $ \v -> do
            x <- sInteger v
            constrain $ 1 .<= x .&& x .< 10
            maximize ("goal" <> v) x
    print (traverse (\v -> getModelValue v res) vs :: Maybe [Integer])
3

Thanks!

(Looking at the implementation in SBV, the reason for this is that the optimisation layer is built in-library by adding constraints and repeatedly refining SMTlib-generated solutions; it doesn’t lean on the more capable optimisation support in the underlying solver, which seems to vary between solvers.)

4

The documentation of SBV does say this:

Currently, optimization requires the use of the z3 SMT solver as the backend, and a good review of these features is given in this paper: http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.

Which makes me think the optimization is specific to the z3 solver. Also, I think SMT also are basically only able to optimize by repeatedly solving with added constraints. If you want something faster you’d need to do integer linear programming instead.

5

@unsat @jaror

The problem here is what the return value of getValue should be if the optimization result is unbounded. For instance, if you try to maximize an integer variable with no constraints on it, then there’s no bounded maximum value. The way z3 deals with this is to return a value in the extension field; i.e., oo representing infinity. A similar thing happens with SReal, where optimization values can have epsilon values. (Consider minimizing a real value which is strictly positive.)

This is why SBV did not allow mixing optimization and query mode; as the notion of satisfiability is a little different for MaxSAT problems. There was no obvious way to support it without adding extra functions that dealt with extension-fields; a can of worms really. So, I left it unimplemented.

But your question here (which I saw a year after you posted) motivated me to take another look at this. As you mention, the fact that optimization goals weren’t supported in query mode was not apparent; i.e., SBV didn’t even tell you about it. That’s definitely a usability bug if nothing else. I’m happy to announce that the freshly released version of SBV (v13.4) now supports optimization with queries. In fact, the program you were trying works out-of-the box:

*Main> main
Just [9,9,9,9,9]

The question, of course, is what to do if the problem is satisfiable in an extension field. For instance, what happens if you change your:

constrain $ 1 .<= x .&& x .< 10

to:

constrain $ 1 .<= x

Well, here’s what happens:

*Main> main
*** Exception:
*** Data.SBV.getValue: The current solver state is satisfiable in an extension field.
*** That is, the optimized values assume epsilon/infinity values.
***
*** Calls to getValue is not supported in this context. Instead, use the 'optimize' method
*** directly and inspect the objective values explicitly.

So we punt and pass the baton back to the user in that case. Not ideal, but is arguably the right thing to do.

I’m happy to consider alternatives here or other ideas to explore. As @jaror mentioned, optimization features in SMT solvers is not standardized. Z3 has its own support, and OptiMathSAT (which SBV does not currently support) has its own interface. Until there’s a common standard on how MaxSAT should behave via SMTLib, we have a large design space to explore.

Happy hacking!

4 Likes