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.
{-# 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 ]
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