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.