feat(dpll): add recursive dpll solver with model verification

src/Sift/Solver.hs

@@ -0,0 +1,75 @@
+module Sift.Solver
+  ( Result(..)
+  , solve
+  , dpll
+  ) where
+
+import Sift.Types
+import Sift.Verify (completeModel)
+import Data.List (maximumBy, nub)
+import Data.Ord (comparing)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+
+data Result
+  = Sat Assignment
+  | Unsat
+  deriving (Eq, Show)
+
+solve :: CNF -> Result
+solve cnf@(CNF cs) =
+  case dpll cs Map.empty of
+    Nothing  -> Unsat
+    Just asn -> Sat (completeModel cnf asn)
+
+dpll :: [Clause] -> Assignment -> Maybe Assignment
+dpll original asn =
+  case reduce asn original of
+    Nothing -> Nothing
+    Just cs
+      | null cs   -> Just asn
+      | otherwise ->
+          case findUnit cs of
+            Just l  -> dpll original (assign l asn)
+            Nothing ->
+              case findPure cs of
+                Just l  -> dpll original (assign l asn)
+                Nothing ->
+                  let l = chooseLit cs
+                  in case dpll original (assign l asn) of
+                       Just m  -> Just m
+                       Nothing -> dpll original (assign (neg l) asn)
+
+assign :: Lit -> Assignment -> Assignment
+assign l = Map.insert (litVar l) (litSign l)
+
+reduce :: Assignment -> [Clause] -> Maybe [Clause]
+reduce asn = fmap reverse . foldl step (Just [])
+  where
+    step Nothing _ = Nothing
+    step (Just acc) c
+      | any ((== Just True) . litValue asn) c = Just acc
+      | otherwise =
+          let remaining = filter ((== Nothing) . litValue asn) c
+          in if null remaining then Nothing else Just (remaining : acc)
+
+findUnit :: [Clause] -> Maybe Lit
+findUnit cs = case [ l | [l] <- cs ] of
+  (l:_) -> Just l
+  []    -> Nothing
+
+findPure :: [Clause] -> Maybe Lit
+findPure cs =
+  case [ Lit v s | (v, [s]) <- Map.toList signsByVar ] of
+    (l:_) -> Just l
+    []    -> Nothing
+  where
+    signsByVar :: Map Var [Bool]
+    signsByVar =
+      Map.map nub (Map.fromListWith (++) [ (litVar l, [litSign l]) | l <- concat cs ])
+
+chooseLit :: [Clause] -> Lit
+chooseLit cs = fst (maximumBy (comparing snd) (Map.toList counts))
+  where
+    counts :: Map Lit Int
+    counts = Map.fromListWith (+) [ (l, 1) | l <- concat cs ]

src/Sift/Verify.hs

@@ -0,0 +1,20 @@
+module Sift.Verify
+  ( satisfies
+  , clauseSatisfied
+  , completeModel
+  ) where
+
+import Sift.Types
+import qualified Data.Map.Strict as Map
+
+clauseSatisfied :: Assignment -> Clause -> Bool
+clauseSatisfied asn = any ((== Just True) . litValue asn)
+
+satisfies :: Assignment -> CNF -> Bool
+satisfies asn (CNF cs) = all (clauseSatisfied asn) cs
+
+completeModel :: CNF -> Assignment -> Assignment
+completeModel cnf asn =
+  foldr insertDefault asn (allVars cnf)
+  where
+    insertDefault v m = if Map.member v m then m else Map.insert v True m