Using the Logic Monad in Haskell

Question

Recently, I implemented a naïve DPLL Sat Solver in Haskell, adapted from John Harrison's Handbook of Practical Logic and Automated Reasoning.

DPLL is a variety of backtrack search, so I want to experiment with using the Logic monad from Oleg Kiselyov et al. I don't really understand what I need to change, however.

Here's the code I've got.

• What code do I need to change to use the Logic monad?
• Bonus: Is there any concrete performance benefit to using the Logic monad?

---

{-# LANGUAGE MonadComprehensions #-} module DPLL where import Prelude hiding (foldr) import Control.Monad (join,mplus,mzero,guard,msum) import Data.Set.Monad (Set, (\\), member, partition, toList, foldr) import Data.Maybe (listToMaybe)  -- "Literal" propositions are either true or false data Lit p = T p | F p deriving (Show,Ord,Eq)  neg :: Lit p -> Lit p neg (T p) = F p neg (F p) = T p  -- We model DPLL like a sequent calculus -- LHS: a set of assumptions / partial model (set of literals) -- RHS: a set of goals  data Sequent p = (Set (Lit p)) :|-: Set (Set (Lit p)) deriving Show  {- --------------------------- Goal Reduction Rules -------------------------- -} {- "Unit Propogation" takes literal x and A :|-: B to A,x :|-: B',  - where B' has no clauses with x,   - and all instances of -x are deleted -} unitP :: Ord p => Lit p -> Sequent p -> Sequent p unitP x (assms :|-:  clauses) = (assms' :|-:  clauses')   where     assms' = (return x) `mplus` assms     clauses_ = [ c | c <- clauses, not (x `member` c) ]     clauses' = [ [ u | u <- c, u /= neg x] | c <- clauses_ ]  {- Find literals that only occur positively or negatively  - and perform unit propogation on these -} pureRule :: Ord p => Sequent p -> Maybe (Sequent p) pureRule sequent@(_ :|-:  clauses) =    let      sign (T _) = True     sign (F _) = False     -- Partition the positive and negative formulae     (positive,negative) = partition sign (join clauses)     -- Compute the literals that are purely positive/negative     purePositive = positive \\ (fmap neg negative)     pureNegative = negative \\ (fmap neg positive)     pure = purePositive `mplus` pureNegative      -- Unit Propagate the pure literals     sequent' = foldr unitP sequent pure   in if (pure /= mzero) then Just sequent'      else Nothing  {- Add any singleton clauses to the assumptions   - and simplify the clauses -} oneRule :: Ord p => Sequent p -> Maybe (Sequent p) oneRule sequent@(_ :|-:  clauses) =     do    -- Extract literals that occur alone and choose one    let singletons = join [ c | c <- clauses, isSingle c ]    x <- (listToMaybe . toList) singletons    -- Return the new simplified problem    return $ unitP x sequent    where      isSingle c = case (toList c) of { [a] -> True ; _ -> False }  {- ------------------------------ DPLL Algorithm ----------------------------- -} dpll :: Ord p => Set (Set (Lit p)) -> Maybe (Set (Lit p)) dpll goalClauses = dpll' $ mzero :|-: goalClauses   where       dpll' sequent@(assms :|-: clauses) = do         -- Fail early if falsum is a subgoal        guard $ not (mzero `member` clauses)        case (toList . join) $ clauses of          -- Return the assumptions if there are no subgoals left          []  -> return assms          -- Otherwise try various tactics for resolving goals          x:_ -> dpll' =<< msum [ pureRule sequent                                , oneRule sequent                                , return $ unitP x sequent                                , return $ unitP (neg x) sequent ] 

Answer 1

Ok, changing your code to use Logic turned out to be entirely trivial. I went through and rewrote everything to use plain Set functions rather than the Set monad, because you're not really using Set monadically in a uniform way, and certainly not for the backtracking logic. The monad comprehensions were also more clearly written as maps and filters and the like. This didn't need to happen, but it did help me sort through what was happening, and it certainly made evident that the one real remaining monad, that used for backtracking, was just Maybe.

In any case, you can just generalize the type signature of pureRule, oneRule, and dpll to operate over not just Maybe, but any m with the constraint MonadPlus m =>.

Then, in pureRule, your types won't match because you construct Maybes explicitly, so go and change it a bit:

in if (pure /= mzero) then Just sequent'    else Nothing 

becomes

in if (not $ S.null pure) then return sequent' else mzero 

And in oneRule, similarly change the usage of listToMaybe to an explicit match so

   x <- (listToMaybe . toList) singletons 

becomes

 case singletons of    x:_ -> return $ unitP x sequent  -- Return the new simplified problem    [] -> mzero 

And, outside of the type signature change, dpll needs no changes at all!

Now, your code operates over both Maybe and Logic!

to run the Logic code, you can use a function like the following:

dpllLogic s = observe $ dpll' s 

You can use observeAll or the like to see more results.

For reference, here's the complete working code:

{-# LANGUAGE MonadComprehensions #-} module DPLL where import Prelude hiding (foldr) import Control.Monad (join,mplus,mzero,guard,msum) import Data.Set (Set, (\\), member, partition, toList, foldr) import qualified Data.Set as S import Data.Maybe (listToMaybe) import Control.Monad.Logic  -- "Literal" propositions are either true or false data Lit p = T p | F p deriving (Show,Ord,Eq)  neg :: Lit p -> Lit p neg (T p) = F p neg (F p) = T p  -- We model DPLL like a sequent calculus -- LHS: a set of assumptions / partial model (set of literals) -- RHS: a set of goals data Sequent p = (Set (Lit p)) :|-: Set (Set (Lit p)) --deriving Show  {- --------------------------- Goal Reduction Rules -------------------------- -} {- "Unit Propogation" takes literal x and A :|-: B to A,x :|-: B',  - where B' has no clauses with x,  - and all instances of -x are deleted -} unitP :: Ord p => Lit p -> Sequent p -> Sequent p unitP x (assms :|-:  clauses) = (assms' :|-:  clauses')   where     assms' = S.insert x assms     clauses_ = S.filter (not . (x `member`)) clauses     clauses' = S.map (S.filter (/= neg x)) clauses_  {- Find literals that only occur positively or negatively  - and perform unit propogation on these -} pureRule sequent@(_ :|-:  clauses) =   let     sign (T _) = True     sign (F _) = False     -- Partition the positive and negative formulae     (positive,negative) = partition sign (S.unions . S.toList $ clauses)     -- Compute the literals that are purely positive/negative     purePositive = positive \\ (S.map neg negative)     pureNegative = negative \\ (S.map neg positive)     pure = purePositive `S.union` pureNegative     -- Unit Propagate the pure literals     sequent' = foldr unitP sequent pure   in if (not $ S.null pure) then return sequent'      else mzero  {- Add any singleton clauses to the assumptions  - and simplify the clauses -} oneRule sequent@(_ :|-:  clauses) =    do    -- Extract literals that occur alone and choose one    let singletons = concatMap toList . filter isSingle $ S.toList clauses    case singletons of      x:_ -> return $ unitP x sequent  -- Return the new simplified problem      [] -> mzero    where      isSingle c = case (toList c) of { [a] -> True ; _ -> False }  {- ------------------------------ DPLL Algorithm ----------------------------- -} dpll goalClauses = dpll' $ S.empty :|-: goalClauses   where      dpll' sequent@(assms :|-: clauses) = do        -- Fail early if falsum is a subgoal        guard $ not (S.empty `member` clauses)        case concatMap S.toList $ S.toList clauses of          -- Return the assumptions if there are no subgoals left          []  -> return assms          -- Otherwise try various tactics for resolving goals          x:_ -> dpll' =<< msum [ pureRule sequent                                 , oneRule sequent                                 , return $ unitP x sequent                                 , return $ unitP (neg x) sequent ]  dpllLogic s = observe $ dpll s