SAT solving with haskell SBV library: how to gener

Question

I want to parse a String that depicts a propositional formula and then find all models of the propositional formula with a SAT solver.

Now I can parse a propositional formula with the hatt package; see the testParse function below.

I can also run a SAT solver call with the SBV library; see the testParse function below.

Question: How do I, at runtime, generate a value of type Predicate like myPredicate within the SBV library that represents the propositional formula I just parsed from a String? I only know how to manually type the forSome_ $ \x y z -> ... expression, but not how to write a converter function from an Expr value to a value of type Predicate.

-- cabal install sbv hatt
import Data.Logic.Propositional
import Data.SBV


-- Random test formula:
-- (x or ~z) and (y or ~z)

-- graphical depiction, see: https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29

testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"

myPredicate :: Predicate
myPredicate = forSome_ $ \x y z -> ((x :: SBool) ||| (bnot z)) &&& (y ||| (bnot z))

testSat = do 
         x <- allSat $ myPredicate
         putStrLn $ show x     


main = do
       putStrLn $ show $ testParse
       testSat


    {-
       Need a function that dynamically creates a Predicate 
(as I did with the function (like "\x y z -> ..") for an arbitrary expression of type "Expr" that is parsed from String. 
    -}

Information that might be helpful:

Here is the link to the BitVectors.Data: http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Here is example code form Examples.Puzzles.PowerSet:

import Data.SBV

genPowerSet :: [SBool] -> SBool
genPowerSet = bAll isBool
  where isBool x = x .== true ||| x .== false

powerSet :: [Word8] -> IO ()
powerSet xs = do putStrLn $ "Finding all subsets of " ++ show xs
                 res <- allSat $ genPowerSet `fmap` mkExistVars n

Here is the Expr data type (from hatt library):

data Expr = Variable      Var
          | Negation      Expr
          | Conjunction   Expr Expr
          | Disjunction   Expr Expr
          | Conditional   Expr Expr
          | Biconditional Expr Expr
          deriving Eq

Answer 1

Working With SBV

Working with SBV requires that you follow the types and realize the Predicate is just a Symbolic SBool. After that step it is important that you investigate and discover Symbolic is a monad - yay, a monad!

Now that you you know you have a monad then anything in the haddock that is Symbolic should be trivial to combine to build any SAT you desire. For your problem you just need a simple interpreter over your AST that builds a Predicate.

Code Walk-Through

The code is all included in one continuous form below but I will step through the fun parts. The entry point is solveExpr which takes expressions and produces a SAT result:

solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat prd

The application of SBV's allSat to the predicate is sort of obvious. To build that predicate we need to declare an existential SBool for every variable in our expression. For now lets assume we have vs :: [String] where each string corresponds to one of the Var from the expression.

  prd :: Predicate
  prd = do
      syms <- mapM exists vs
      let env = M.fromList (zip vs syms)
      interpret env e0

Notice how programming language fundamentals is sneaking in here. We now need an environment that maps the expressions variable names to the symbolic booleans used by SBV.

Next we interpret the expression to produce our Predicate. The interpret function uses the environment and just applies the SBV function that matches the intent of each constructor from hatt's Expr type.

  interpret :: Env -> Expr -> Predicate
  interpret env expr = do
   let interp = interpret env
   case expr of
    Variable v -> return (envLookup v env)
    Negation e -> bnot `fmap` interp e
    Conjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 &&& r2)
    Disjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 ||| r2)
    Conditional e1 e2   -> error "And so on"
    Biconditional e1 e2 -> error "And so on"

And that is it! The rest is just boiler-plate.

Complete Code

import Data.Logic.Propositional hiding (interpret)
import Data.SBV
import Text.Parsec.Error (ParseError)
import qualified Data.Map as M
import qualified Data.Set as Set
import Data.Foldable (foldMap)
import Control.Monad ((<=<))

testParse :: Either ParseError Expr
testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"

type Env = M.Map String SBool

envLookup :: Var -> Env -> SBool
envLookup (Var v) e = maybe (error $ "Var not found: " ++ show v) id
                            (M.lookup [v] e)

solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat go
 where
  vs :: [String]
  vs = map (\(Var c) -> [c]) (variables e0)

  go :: Predicate
  go = do
      syms <- mapM exists vs
      let env = M.fromList (zip vs syms)
      interpret env e0
  interpret :: Env -> Expr -> Predicate
  interpret env expr = do
   let interp = interpret env
   case expr of
    Variable v -> return (envLookup v env)
    Negation e -> bnot `fmap` interp e
    Conjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 &&& r2)
    Disjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 ||| r2)
    Conditional e1 e2   -> error "And so on"
    Biconditional e1 e2 -> error "And so on"

main :: IO ()
main = do
       let expr = testParse
       putStrLn $ "Solving expr: " ++ show expr
       either (error . show) (print <=< solveExpr) expr

Answer 2

forSome_ is a member of the Provable class, so it seems it would suffice to define the instance Provable Expr. Almost all functions in SVB use Provable so this would allow you to use all of those natively Expr. First, we convert an Expr to a function which looks up variable values in a Vector. You could also use Data.Map.Map or something like that, but the environment is not changed once created and Vector gives constant time lookup:

import Data.Logic.Propositional
import Data.SBV.Bridge.CVC4
import qualified Data.Vector as V
import Control.Monad

toFunc :: Boolean a => Expr -> V.Vector a -> a
toFunc (Variable (Var x)) = \env -> env V.! (fromEnum x)
toFunc (Negation x) = \env -> bnot (toFunc x env)
toFunc (Conjunction a b) = \env -> toFunc a env &&& toFunc b env
toFunc (Disjunction a b) = \env -> toFunc a env ||| toFunc b env
toFunc (Conditional a b) = \env -> toFunc a env ==> toFunc b env
toFunc (Biconditional a b) = \env -> toFunc a env <=> toFunc b env

Provable essentially defines two functions: forAll_, forAll, forSome_, forSome. We have to generate all possible maps of variables to values and apply the function to the maps. Choosing how exactly to handle the results will be done by the Symbolic monad:

forAllExp_ :: Expr -> Symbolic SBool
forAllExp_ e = (m0 >>= f . V.accum (const id) (V.replicate (fromEnum maxV + 1) false)
  where f = return . toFunc e 
        maxV = maximum $ map (\(Var x) -> x) (variables e)
        m0 = mapM fresh (variables e)

Where fresh is a function which "quantifies" the given variable by associating it with all possible values.

fresh :: Var -> Symbolic (Int, SBool)
fresh (Var var) = forall >>= \a -> return (fromEnum var, a)

If you define one of these functions for each of the four functions you will have quite a lot of very repetitive code. So you can generalize the above as follows:

quantExp :: (String -> Symbolic SBool) -> Symbolic SBool -> [String] -> Expr -> Symbolic SBool
quantExp q q_ s e = m0 >>= f . V.accum (const id) (V.replicate (fromEnum maxV + 1) false)
  where f = return . toFunc e 
        maxV = maximum $ map (\(Var x) -> x) (variables e)
        (v0, v1) = splitAt (length s) (variables e)
        m0 = zipWithM fresh (map q s) v0 >>= \r0 -> mapM (fresh q_) v1 >>= \r1 -> return (r0++r1)

fresh :: Symbolic SBool -> Var -> Symbolic (Int, SBool)
fresh q (Var var) = q >>= \a -> return (fromEnum var, a)

If it is confusing exactly what is happening, the Provable instance may suffice to explain:

instance Provable Expr where 
  forAll_  = quantExp forall forall_ [] 
  forAll   = quantExp forall forall_ 
  forSome_ = quantExp exists exists_ []
  forSome  = quantExp exists exists_ 

Then your test case:

myPredicate :: Predicate
myPredicate = forSome_ $ \x y z -> ((x :: SBool) ||| (bnot z)) &&& (y ||| (bnot z))

myPredicate' :: Predicate
myPredicate' = forSome_ $ let Right a = parseExpr "test source" "((X | ~Z) & (Y | ~Z))" in a

testSat = allSat myPredicate >>= print
testSat' = allSat myPredicate >>= print