Using the Logic Monad in Haskell
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
Is there any concrete performance benefit to using the Logic monad?
TL;DR: Not that I can find; it appears that Maybe outperforms Logic since it has less overhead.
I decided to implement a simple benchmark to check the performance of Logic versus Maybe.
In my test, I randomly construct 5000 CNFs with n clauses, each clause containing three literals. Performance is evaluated as the number of clauses n is varied.
In my code, I modified dpllLogic as follows:
dpllLogic s = listToMaybe $ observeMany 1 $ dpll s
I also tested modifying dpll with fair disjunction, like so:
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:_ -> msum [ pureRule sequent
, oneRule sequent
, return $ unitP x sequent
, return $ unitP (neg x) sequent ]
>>- dpll'
I then tested the using Maybe, Logic, and Logic with fair disjunction.
Here are the benchmark results for this test:
As we can see, Logic with or without fair disjunction in this case makes no difference. The dpll solve using the Maybe monad appears to run in linear time in n, while using the Logic monad incurs additional overhead. It appears that the overhead incurred plateaus off.
Here is the Main.hs file used to generate these test. Someone wishing to reproduce these benchmarks might wish to review Haskell's notes on profiling:
module Main where
import DPLL
import System.Environment (getArgs)
import System.Random
import Control.Monad (replicateM)
import Data.Set (fromList)
randLit = do let clauses = [ T p | p <- ['a'..'f'] ]
++ [ F p | p <- ['a'..'f'] ]
r <- randomRIO (0, (length clauses) - 1)
return $ clauses !! r
randClause n = fmap fromList $ replicateM n $ fmap fromList $ replicateM 3 randLit
main = do args <- getArgs
let n = read (args !! 0) :: Int
clauses <- replicateM 5000 $ randClause n
-- To use the Maybe monad
--let satisfiable = filter (/= Nothing) $ map dpll clauses
let satisfiable = filter (/= Nothing) $ map dpllLogic clauses
putStrLn $ (show $ length satisfiable) ++ " satisfiable out of "
++ (show $ length clauses)