StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POUsing the Logic Monad in Haskell
text
Body
copied!<p>Recently, I implemented a naïve <a href="http://en.wikipedia.org/wiki/DPLL_algorithm" rel="noreferrer">DPLL Sat Solver</a> in <em>Haskell</em>, adapted from John Harrison's <a href="http://www.cambridge.org/gb/knowledge/isbn/item2327697/?site_locale=en_GB" rel="noreferrer">Handbook of Practical Logic and Automated Reasoning</a>.</p> <p>DPLL is a variety of backtrack search, so I want to experiment with using the <a href="http://hackage.haskell.org/packages/archive/logict/0.2.3/doc/html/Control-Monad-Logic.html" rel="noreferrer">Logic monad</a> from <a href="http://www.cs.rutgers.edu/~ccshan/logicprog/LogicT-icfp2005.pdf" rel="noreferrer">Oleg Kiselyov et al</a>. I don't really understand what I need to change, however.</p> <p>Here's the code I've got.</p> <ul> <li>What code do I need to change to use the Logic monad?</li> <li><strong>Bonus</strong>: Is there any concrete performance benefit to using the Logic monad? </li> </ul> <hr> <pre><code>{-# 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 ] </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload