Optimization and unsat-cores

[iamrecursion]

I've got a problem I'm trying to solve with sbv where it would be useful to be able to use a record as an interpreted sort, rather than as a an uninterpreted sort containing interpreted sorts. The motivation behind doing this would be to get an output in the model for some type T, rather than the free variables (SInteger in this case) that make up T.

Is this possible? I can't find any section in the user guide that mentions it.

[LeventErkok]

When working with SBV, it is actually recommended that records are modeled so that the fields are symbolic: This leads to much cleaner code and underlying solver support is much better with symbolic base fields.

Having said that, SMTLib does support a notion of symbolic records (data-types in general), but SBV does not support them currently. There are many design/technical challenges for that.

In either case, I'd recommend going with symbolic fields for records. If you're running into issues/bugs, or need some help on modeling them, I'm happy to help. Sharing some actual code showing what you are trying to do always helps!

[iamrecursion]

I'm currently working with my data as a record of symbolic values, yes! The main reason I wanted to be able to define a symbolic record itself would be ease of working with the data.

I have a type similar to the following, with accompanying instances of EqSymbolic, OrdSymbolic, Mergeable, and Provable.

data Foo = Foo
    { __one   :: SWord64
    , __two   :: SWord64
    , __three :: SWord64
    , __four  :: SWord64
    , __five  :: SWord64
    } deriving (Eq, Generic, Show)

It's not really an issue that I'm running into as much as a user-experience bug. Currently I can't find a better way to create a version of this struct in the solver as free symbolic variables than to give each field a name based on the master name.

sFoo :: String -> Symbolic Foo
sFoo name = do
    a <- free $ name <> ":one"
    b <- free $ name <> ":two"
    c <- free $ name <> ":three"
    d <- free $ name <> ":four"
    e <- free $ name <> ":five"
    pure $ Foo a b c d e

This does the job I need of it, but it feels somewhat clunky to have to read out each of the components of the record individually by these awkward names, rather than being able to get at the record as a whole!

The only reason I even posted an issue about it is that, writing the code, I felt like there must be a better way. I don't know if I'm missing something or this really is how I should go about it, so your thoughts are definitely appreciated.

By the way, thank you for your work on this library! It's a beautiful interface and it makes my life a lot easier.

[LeventErkok]

I think you have the right idea and the structure. The creation/extraction can be simplified by some helper functions. Here's some code that might help you out, feel free to adopt for your needs:

{-# LANGUAGE NamedFieldPuns #-}

import Data.SBV
import Data.SBV.Control

data Foo a = Foo { __one   :: a
                 , __two   :: a
                 , __three :: a
                 , __four  :: a
                 , __five  :: a
                 }
                 deriving Show

sFoo :: String -> Symbolic (Foo SWord64)
sFoo nm = do a <- free $ nm ++ ":one"
             b <- free $ nm ++ ":two"
             c <- free $ nm ++ ":three"
             d <- free $ nm ++ ":four"
             e <- free $ nm ++ ":five"
             return $ Foo a b c d e

extractFoo :: Foo SWord64 -> Query (Foo Word64)
extractFoo f = Foo <$> getValue (__one   f)
                   <*> getValue (__two   f)
                   <*> getValue (__three f)
                   <*> getValue (__four  f)
                   <*> getValue (__five  f)

t :: IO (Foo Word64)
t = runSMT $ do s@Foo{__one, __two, __three, __four, __five} <- sFoo "myVersion"
                constrain $ __one .> 5
                constrain $ __two .> 10
                constrain $ __three .== __four + __five
                constrain $ __three .> 15
                query $ do cs <- checkSat
                           case cs of
                             Unsat -> error "Unsat!"
                             Unk   -> error "Unknown!"
                             Sat   -> extractFoo s

main :: IO ()
main = t >>= print

When I run it, I get:

*Main> main
Foo {__one = 6, __two = 9223372036854775808, __three = 18446744073709551600, __four = 18446744073709551600, __five = 0}

Is this of any help? Let me know if you run into any other difficulties!!

[iamrecursion]

That was such a great help! It's much, much nicer to work with now!

I was wondering how I'd combine this with an optimisation constraint: foo such that foo satisfies the constraints and is as large as possible. I've read the docs section on optimisation, but to express the goal I need Metric a (which I can't find described anywhere), and I have a Query a as the input to the query. Sorry if I've missed it and it's something obvious!

[LeventErkok]

A Metric is simply a function that returns an SInteger or SReal. Nothing magic about it.

Coding optimization in this style gets a little hairy, since there are so many cases to consider. (Different styles of optimizations, optimal value may be in an extension field, etc.) But below is how I would go about it:

{-# LANGUAGE NamedFieldPuns #-}

import Data.SBV
import Data.SBV.Control

import qualified Data.Map as M

data FooGen a = Foo { v1 :: a
                    , v2 :: a
                    , v3 :: a
                    , v4 :: a
                    , v5 :: a
                    }
                    deriving Show

type SFoo = FooGen SWord64
type Foo  = FooGen Word64

sFoo :: String -> Symbolic SFoo
sFoo nm = Foo <$> free_
              <*> free_
              <*> free_
              <*> free_
              <*> free_

extractFoo :: SFoo -> Query Foo
extractFoo Foo{v1, v2, v3, v4, v5} = Foo <$> getValue v1
                                         <*> getValue v2
                                         <*> getValue v3
                                         <*> getValue v4
                                         <*> getValue v5

t :: IO Foo
t = extractMin =<< optimize Lexicographic (do

                        s@Foo{v1, v2, v3, v4, v5} <- sFoo "myVersion"

                        -- some arbitrary constraints:
                        constrain $ v1 .> 5
                        constrain $ v2 .> 10
                        constrain $ v3 .== v4 + v5
                        constrain $ v3 .> 15
                        constrain $ v1 .>= 0 &&& v1 .< 20
                        constrain $ v2 .>= 0 &&& v2 .< 30
                        constrain $ v3 .>= 4
                        constrain $ v4 .>= 12
                        constrain $ v5 .>= 0
                        constrain $ v3 .<= 40

                        -- Minimize each component:
                        minimize "min-v1" v1
                        minimize "min-v2" v2
                        minimize "min-v3" v3
                        minimize "min-v4" v4
                        minimize "min-v5" v5)

  where -- This is a bit ugly and problem specific, but there's a lot of cases to consider!
        -- If you can abstract this into a nice pattern and suggest a helper function that
        -- can be useful in general, let me know!
        extractMin r = do let m = case r of
                                    LexicographicResult lr -> getModelObjectives lr
                                    _                      -> error "Non-lexicographic optimization, need more code here!"
                              grab s = case s `M.lookup` m of
                                         Nothing             -> error $ "Cannot find " ++ s ++ " in the optimal model!"
                                         Just (RegularCW  w) -> return $ fromCW w
                                         Just (ExtendedCW v) -> error $ "Optimal value is in an extension field for " ++ s ++ ": " ++ show v

                          Foo <$> grab "min-v1"
                              <*> grab "min-v2"
                              <*> grab "min-v3"
                              <*> grab "min-v4"
                              <*> grab "min-v5"

main :: IO ()
main = print =<< t

When I run it, I get:

*Main> main
Foo {v1 = 6, v2 = 11, v3 = 16, v4 = 12, v5 = 4}

I didn't check the results, but I trust SBV and Z3 that it is indeed the minimal model satisfying all the constraints! (Note that we lexicographically optimize in this case: First v1, then v2, etc.) You can change the optimization function easily, and/or play with other combos. For instance, you can minimize v1, but maximize v2 or mimimize (v1+v3) etc..

I hope this works for you, and you can extend it to your use case. The code is necessarily a bit involved here; but I trust one can "extract" the essence of it and come up with some helper optimization routines SBV currently lacks. If you do come up with an idea that can be useful in general, feel free to submit a pull request!

[iamrecursion]

Yet again you've been a fantastic help! There only remains one last thing for me to ask. Swapping to calling optimize vs. operating on the result of checkSat means that I can't see any way to get at the core in the unsat case. I was using the core to determine which goals conflicted, but I was wondering if there was a better way to do that.

Essentially, extract the conflicts that prevented satisfiability in the Unsatisfiable case.

[LeventErkok]

Ah, good catch. Unfortunately, this scenario is not currently supported. We should really add a means of accessing optimization routines in query mode. Historically, optimization was implemented before queries were supported, and I've been adding support for things in the query mode for various features. Unfortunately, optimization hasn't received that attention yet. (And it's rather tricky due to extension-fields, various optimization methods, etc. so I don't expect a quick design here.)

My recommendation would be to go with the optimize call; and if you detect unsat, then solve the problem again, but without the objectives and get the unsat-core. Yes, this wastes effort since you end up calling the solver twice for the same problem; but hopefully the unsat case happens rarely and it is not in the speed-path.

Let me know what you find out. I'd be interested to know if this works OK for you; if it's prohibitively expensive or doesn't work for some other reason, we can start experimenting with a design that allows optimization in the query mode.

[iamrecursion]

Oh that is ugly! It should work for now as the problem isn't ridiculously large, but I'd love to help experimenting with a design for optimisation in query mode regardless!

Edit: Is it not possible to provide the unsat core as an optional part of the SMTResult?

[LeventErkok]

Indeed, one can extract unsat-cores and put it as part of the Unsatisfiable constructor. But unsat-cores are only computed on demand by SMT-solvers, as it requires them to construct a proof first. So, there'd be an associated performance penalty. Perhaps the right thing to do is to put a Maybe [String] parameter; and only request them if the user asks for it. This could be a cheap solution.

But I'd like to see what a query-based optimization API might look like. That might open it up for an easier to use API.

[iamrecursion]

Well I'm definitely open to any solution that helps make this nicer! Is a GH issue the best place to discuss it or would you prefer some other method of contact?

[LeventErkok]

@iamrecursion

Well, I have good news and bad news. :-)

The good news is that returning unsat-core with the Unsatisfiable construction is just fine I think. Thanks for the suggestion. Indeed, I just implemented that. If you build from master, you can now say:

import Data.SBV
import Data.SBV.Control

q = sat $ do setOption $ ProduceUnsatCores True
             i <- sInteger "i"

             namedConstraint "c1" $ i .> 5
             namedConstraint "c2" $ i .< 2
             namedConstraint "c3" $ i .> 10

And you get:

*Main> q
Unsatisfiable. Unsat core:
    c1
    c2
*Main> SatResult (Unsatisfiable _ (Just ucore)) <- q
*Main> ucore
["c1","c2"]

Unfortunately, this doesn't solve your problem. This is what I get if I try to use it with minimization:

import Data.SBV
import Data.SBV.Control

q n = optimize Lexicographic $ do
          setOption $ ProduceUnsatCores True
          i <- sInteger "i"

          minimize "min-i" i

          namedConstraint "c1" $ i .> 5
          namedConstraint "c2" $ i .< literal n

If I try a satisfiable case, all is well:

*Main> q 10
Optimal model:
  i     = 6 :: Integer
  min-i = 6 :: Integer

Unfortunately, if the constraints are unsat, I get:

*Main> q 1
*** Exception:
*** Data.SBV: Unexpected response from the solver, context: getUnsatCore:
***
***    Sent      : (get-unsat-core)
***    Expected  : an unsat-core response
***    Received  : (error "line 21 column 15: Unsat cores are not supported with optimization")
***
***    Executable: z3
***    Options   : -nw -in -smt2
***
***    Reason    : Solver returned an error: "line 21 column 15: Unsat cores are not supported with optimization"
***    Hint      : Make sure you use:
***                       setOption $ ProduceUnsatCores True
***                so the solver will be ready to compute unsat cores,
***                and that there is a model by first issuing a 'checkSat' call.

So, looks like z3 doesn't support unsat-core extraction with optimization.

I am not sure why z3 doesn't support this. Perhaps it's something they just haven't implemented yet; or maybe there are good reasons behind it. It would be nice to ask them directly I suppose, to get a definitive answer.

I hope this helps you in any case, though obviously looks like you're stuck with running the problem twice in case of unsat. I can't think of any other way as things stand with z3.

Regarding query mode optimization in SBV: Yes, I think that requires its own github issue to discuss how the design might proceed. Please open one to get the discussion going!

[iamrecursion]

How annoying! I guess I'm stuck with the double run in the failure case for now! I've asked them here, and I'm interested to find out what the reason is!

I've created a new issue #361 to continue the discussion.

[iamrecursion]

The response here might be of interest!

[LeventErkok]

361 covers this now

[LeventErkok]

@iamrecursion SBV 7.7 is out on hackage now, and the Unsatisfiable constructor now contains the unsat-core if requested. Not quite what this ticket originally requested, but saves you from going to query mode in simple cases. #361 is still open to track how to do query mode optimization with your name on it!

[iamrecursion]

Oh well that is a sight for sore eyes! I’ll give it a go soon! And I know, #361 is definitely on my radar, but I’m very snowed under at the moment!

[LeventErkok]

@iamrecursion Z3 now supports unsat cores in the optimization engine. In case this helps with your project. (You'd need to build z3 from github.)

[iamrecursion]

I just saw the update to that issue! Thanks @LeventErkok! I'll definitely give it a go when I get back to the task this was for!