dpll.hs

{-
DPLL from the textbook:

function DPLL(clauses, symbols, model ) returns true or false
  if every clause in clauses is true in model then return true
  if some clause in clauses is false in model then return false
  P , value ← FIND-PURE-SYMBOL (symbols, clauses, model )
  if P is non-null then return DPLL(clauses, symbols – P , model ∪ {P =value})
  P, value ← FIND-UNIT-CLAUSE (clauses, model)
  if P is non-null then return DPLL(clauses, symbols – P , model ∪ {P =value})
  P ← F IRST (symbols); rest ← R EST (symbols)
  return DPLL(clauses, rest, model ∪ {P =true}) or DPLL(clauses, rest, model ∪ {P =false}))
-}

-- Translated directly into Haskell:

dpll0 :: Clauses -> Symbols -> Model -> Bool
dpll0 clauses symbols model =
  if all (`isTrueIn` model) clauses
  then True
  else 
    if any (`isFalseIn` model) clauses
    then False
    else
      case findPureSymbol symbols clauses model of
           (Just sym, val) -> 
             dpll0 clauses (symbols `minus` sym) 
                           (model `including` (sym := val))
           (Nothing, val) -> 
             case findUnitClause clauses model of
                  (Just sym, val) -> 
                    dpll0 clauses (symbols `minus` sym)
                                  (model `including` (sym := val))
                  (Nothing, val) ->
                    case symbols of
                         (x:xs) -> 
                           dpll0 clauses xs (model `including` (x := False))
                           || dpll0 clauses xs (model `including` (x := True))

-- taking advantage of lazy lists and asum as a means of "choose first successful alternative":
dpll :: Clauses -> Symbols -> Model -> Maybe Model
dpll clauses symbols model
  | all (`isTrueIn` model) clauses  = Just model
  | any (`isFalseIn` model) clauses = Nothing
  | otherwise =
      asum (map (>>= next) controlList)
  where
    next :: Assignment -> Maybe Model
    next (sym := val) =
      dpll clauses (symbols `minus` sym) (model `including` (sym := val))

    controlList :: [Maybe Assignment]
    controlList =
      [ findPureSymbol symbols clauses model
      , findUnitClause clauses model
      , (:= False) <$> listToMaybe symbols
      , (:= True) <$> listToMaybe symbols
      ]