DPLL.lhs

   1 \begin{code}
   2 {-# OPTIONS_GHC -fglasgow-exts  #-}
   3
   4 module Main where
   5
   6 import Control.Monad
   7 import Control.Monad.State
   8 import Control.Monad.Trans
   9 import Control.Monad.Error
  10 import Control.Arrow
  11
  12 import Text.ParserCombinators.Parsec hiding (State)
  13
  14 import Data.Set (Set)
  15 import qualified Data.Set as Set
  16 import Data.Map (Map)
  17 import qualified Data.Map as Map
  18 import Data.List
  19 import Data.Maybe
  20
  21 import Debug.Trace
  22 \end{code}
  23
  24 \begin{code}
  25 type StateWithFail s e a =  ErrorT e (State s) a
  26
  27 evalSWF :: StateWithFail s e a -> s -> Either e a
  28 evalSWF swf s = evalState (runErrorT swf) s
  29
  30 runSWF :: StateWithFail s e a -> s -> (Either e a, s)
  31 runSWF swf s = runState (runErrorT swf) s
  32
  33 instance Error () where
  34   noMsg    = ()
  35   strMsg _ = ()
  36
  37 instance Error Clause where
  38   noMsg    = undefined
  39   strMsg   = undefined
  40
  41 type Variable = Int
  42 data CNF = And [Clause] deriving (Show, Eq)
  43 data Clause = Or [Literal] deriving (Show, Eq)
  44 type Literal = (Bool, Variable)
  45 type Decision = (Bool, Variable)
  46 type WatchList = Map Literal [Clause]
  47 data Env = Env (Map Variable Bool) [Variable]
  48   deriving (Show)
  49
  50 class WatchListC w where
  51   initWL :: CNF -> w
  52   appendWatches :: Literal -> [Clause] -> w -> w
  53   appendWatch :: Literal -> Clause -> w -> w
  54   clearWatch :: Literal -> w -> w
  55   lookupWatch :: Decision -> w -> [Clause]
  56   updateWatch :: Literal -> Clause -> Clause -> w -> w
  57
  58 class EnvC e where
  59   empty :: [Variable] -> e
  60   bindVar :: Variable -> Bool -> e -> e
  61   lookupVar :: Variable -> e -> Maybe Bool
  62   decide :: e -> Maybe Variable
  63 \end{code}
  64
  65 \begin{code}
  66 instance EnvC Env where
  67   empty = Env (Map.empty)
  68   bindVar v b (Env a ua) = Env (Map.insert v b a) (delete v ua)
  69   lookupVar v (Env a _) = Map.lookup v a
  70   decide (Env _ uas) = listToMaybe uas
  71
  72 litValue :: EnvC a => a -> Literal -> Maybe Bool
  73 litValue e (bar, v) = (/= bar) `fmap` lookupVar v e
  74 \end{code}
  75
  76 \begin{code}
  77 instance WatchListC WatchList where
  78   initWL (And cs) = foldl' addReps Map.empty cs
  79     where
  80     addReps :: WatchList -> Clause -> WatchList
  81     addReps wl c@(Or (l1:l2:lits)) = appendWatch l1 c (appendWatch l2 c wl)
  82   appendWatches lit cs wl = Map.insertWith (flip (++)) lit cs wl
  83   appendWatch lit c wl = Map.insertWith ((:) . head) lit (return c) wl
  84   clearWatch lit wl = Map.delete lit wl
  85   lookupWatch d wl = maybe [] id $ Map.lookup d wl
  86   updateWatch lit oldc c wl = wl'
  87     where
  88     oldcs = maybe [] id (Map.lookup lit wl)
  89     cs = c : (delete oldc oldcs)
  90     wl' = Map.insert lit cs (Map.delete lit wl)
  91 \end{code}
  92
  93 \begin{code}
  94 dpll :: CNF -> [Variable] -> Maybe Env
  95 dpll cnf vars = either (const Nothing) Just $ evalSWF (dpll' (empty vars)) (initWL cnf)
  96   where
  97   dpll' :: Env -> StateWithFail WatchList () Env
  98   dpll' e = do
  99     wl <- get
 100     maybe (return e) (\v -> msum [tryDecision e (True, v), tryDecision e (False, v)]) $ trace "decide" (decide e)
 101
 102   tryDecision :: Env -> Decision -> StateWithFail WatchList () Env
 103   tryDecision e (b, v) = do
 104     wl <- get
 105     --let (ee, wl') = bcp wl e (b, v) in put wl' >> either (const $ throwError ()) dpll' ee
 106     let (ee, wl') = runState (bcpM e v b) wl in put wl' >> either (const $ throwError ()) dpll' ee
 107 \end{code}
 108
 109 \begin{code}
 110 bcpM :: (EnvC e, WatchListC w) => e -> Variable -> Bool -> State w (Either Clause e)
 111 bcpM e v b =
 112   do
 113     wl <- get
 114     let cs = trace "prop" (lookupWatch (b, v) wl) in
 115       case runSWF (mapM (checkClauseM e' (b, v)) cs) (clearWatch (b, v) wl) of
 116         (Left c, wl')   -> do put $ addOldWatches (b, v) c cs wl'
 117                               return $ Left c
 118         (Right ws, wl') -> do put wl'
 119                               uncurry (flip (>>)) ((return *** put) (foldl' checkImpl (Right e', wl') ws))
 120   where
 121     e' = bindVar v b e
 122     checkImpl (Left c, wl'') _                    = (Left c, wl'')
 123     checkImpl ee Nothing                          = ee
 124     checkImpl (Right e'', wl'') (Just (b'', v'')) = runState (bcpM e'' v'' (not b'')) wl''
 125
 126     addOldWatches lit c cs wl' = appendWatches lit (drop 1 $ dropWhile (/= c) cs) wl'
 127
 128 -- Left clause        ==> Conflict
 129 -- Right Nothing      ==> Continue -- not unit
 130 -- Right (Just lit)   ==> Continue -- unit
 131 checkClauseM :: (EnvC e, WatchListC w)
 132              => e -> Decision -> Clause -> StateWithFail w Clause (Maybe Literal)
 133 checkClauseM e d c = do
 134   wl <- get
 135   let (w1, w2, lits) = case c of
 136                          Or (lit1:lit2:lits) | d == lit1 -> (d, lit2, lits)
 137                                              | otherwise -> (d, lit1, lits)
 138       isSat = fromMaybe False $ litValue e w2
 139       findLit = find (\lit -> litValue e lit /= Just False) lits
 140       computeUnit w = maybe (return (Just w))
 141                             (\b -> if b then return Nothing else (trace "conflict" (throwError c))) $ litValue e w
 142       swapWatches lit awl = awl''
 143         where
 144         c' = (Or (lit:w2:w1:delete lit lits))
 145         awl' = updateWatch w2 c c' awl
 146         awl'' = appendWatch lit c' awl'
 147     in
 148       if isSat
 149         then put (appendWatch d c wl) >> return Nothing
 150         else case findLit of
 151                Just wi -> put (swapWatches wi wl) >> return Nothing
 152                Nothing -> put (appendWatch d c wl) >> computeUnit w2
 153
 154 \end{code}
 155
 156 \begin{code}
 157 bcp :: (EnvC e, WatchListC w) => w -> e -> Decision -> (Either e e, w)
 158 bcp wl e d =
 159   case conflict of
 160     True  -> (Left e', wl')
 161     False -> foldl' checkImpls (Right e', wl') impls
 162   where
 163   (db, dv) = d
 164   e' = bindVar dv db e
 165   cs = lookupWatch d wl
 166   (wl', cs') = mapAccumL checkClause (clearWatch d wl) cs
 167
 168   conflict = Left False `elem` cs'
 169   impls = [(not bar, v) | Right (bar, v) <- cs']
 170   checkImpls ((Left e''), wl'')  _ = ((Left e''), wl'')
 171   checkImpls ((Right e''), wl'') ri = bcp wl'' e'' ri
 172
 173   checkClause :: WatchListC w => w -> Clause -> (w, Either Bool Literal)
 174   checkClause wl c =
 175     if isSat
 176       then (appendWatch d c wl, Left True)
 177       else case newLit of
 178              Just wi -> (adjWatches wi wl, Left True)
 179              Nothing -> (appendWatch d c wl, newUnit w2)
 180     where
 181     (Or (lit1:lit2:lits)) = c
 182     (w1, w2) = if lit1 == d then (lit1, lit2) else (lit2, lit1)
 183
 184     isSat =  (maybe False id $ litValue e' w2)
 185     newLit = find (\lit -> litValue e' lit /= Just False) lits
 186     newUnit w = maybe (Right w) Left $ litValue e' w
 187     newClause w oldw  = (Or ((w:w2:delete w lits) ++ [oldw]))
 188     adjWatches newLit awl = bothFixed
 189       where
 190       c' = newClause newLit w1
 191       w2Fixed = updateWatch w2 c c' awl
 192       bothFixed = appendWatch newLit c' w2Fixed
 193 \end{code}
 194
 195 \begin{code}
 196 main = interact checkSat
 197   where
 198   checkSat :: String -> String
 199   checkSat s =
 200     case parse parseDIMACS "" s of
 201       Left err       -> "parse error at " ++ show err
 202       Right (cnf, v) -> maybe "UNSAT\n" (const "SAT\n") $ dpll cnf [1..v]
 203 \end{code}
 204
 205 \begin{code}
 206 ---
 207 --- Parser
 208 ---
 209
 210 parseDIMACS :: Parser (CNF, Int)
 211 parseDIMACS = do parseComments
 212                  (v, c) <- parseHeader
 213                  cnf <- liftM And parseClauses
 214                  return (cnf, v)
 215
 216 parseComments :: Parser [String]
 217 parseComments = many $ char 'c' >> manyTill anyChar newline
 218
 219 parseHeader :: Parser (Int, Int)
 220 parseHeader = do string "p cnf"
 221                  many1 space
 222                  vars <- many1 digit
 223                  many1 space
 224                  clauses <- many1 digit
 225                  many (char ' ')
 226                  newline
 227                  return (read vars, read clauses)
 228
 229 parseClauses :: Parser [Clause]
 230 parseClauses = sepEndBy1 parseLiteral space >>= return . map Or . split
 231   where
 232   split [] = []
 233   split xs = let (c, (z:xs')) = break (== (False, 0)) xs in c : split xs'
 234
 235 parseLiteral :: Parser Literal
 236 parseLiteral = many space >> choice [char '-' >> parseInt True, parseInt False]
 237                where
 238                parseInt polar = many1 digit >>= return . (,) polar . read
 239 \end{code}
 240