StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>Ok, changing your code to use <code>Logic</code> turned out to be entirely trivial. I went through and rewrote everything to use plain <code>Set</code> functions rather than the <code>Set</code> monad, because you're not really using <code>Set</code> 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 <code>Maybe</code>.</p> <p>In any case, you can just generalize the type signature of <code>pureRule</code>, <code>oneRule</code>, and <code>dpll</code> to operate over not just <code>Maybe</code>, but any <code>m</code> with the constraint <code>MonadPlus m =></code>. </p> <p>Then, in <code>pureRule</code>, your types won't match because you construct <code>Maybe</code>s explicitly, so go and change it a bit:</p> <pre><code>in if (pure /= mzero) then Just sequent' else Nothing </code></pre> <p>becomes</p> <pre><code>in if (not $ S.null pure) then return sequent' else mzero </code></pre> <p>And in <code>oneRule</code>, similarly change the usage of <code>listToMaybe</code> to an explicit match so</p> <pre><code> x <- (listToMaybe . toList) singletons </code></pre> <p>becomes</p> <pre><code> case singletons of x:_ -> return $ unitP x sequent -- Return the new simplified problem [] -> mzero </code></pre> <p>And, outside of the type signature change, <code>dpll</code> needs no changes at all!</p> <p>Now, your code operates over <em>both</em> <code>Maybe</code> <em>and</em> <code>Logic</code>!</p> <p>to run the <code>Logic</code> code, you can use a function like the following:</p> <pre><code>dpllLogic s = observe $ dpll' s </code></pre> <p>You can use <code>observeAll</code> or the like to see more results.</p> <p>For reference, here's the complete working code:</p> <pre><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 </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