A naive SAT solver in Haskell

CNF.hs

import qualified Data.Set as Set

data Clause = Value Bool | Not Int | Literal Int | Or Clause Clause deriving (Eq,Ord)
type CNF    = Set.Set Clause

instance Show Clause where
  show (Value True)  = "T"
  show (Value False) = "F"
  show (Not x)       = "~" ++ show x
  show (Literal x)   = show x
  show (Or l r)      = foldr1 (++) ["(", show l, ") || (", show r, ")"]

lits (Or l r)    = Set.unions $ map lits [l, r]
lits (Literal x) = Set.fromList [x]
lits (Not x)     = Set.fromList [x]
lits _           = Set.empty

eval (Value v) lit val = Value v
eval (Literal x) y val = if x == y then Value val else Literal x
eval (Not x) y val     = if x == y then Value (not val) else Not x
eval (Or l r) x val    = if truth then
                           Value True
                         else if leval == (Value False) then
                           reval
                         else if reval == (Value False) then
                           leval
                         else
                           Or leval reval
  where leval = eval l x val
        reval = eval r x val
        truth = (> 0) $ length $ filter (== Value True) [leval, reval]

solve cnf = map (map ((\x -> if x == True then 1 else 0) . snd)) $ solns cnf
solns cnf = filter (\x -> valid x clauses) bchoices
  where litxs    = (Set.elems . (Set.unions . map lits) . Set.elems) cnf
        clauses  = Set.elems cnf
        litln    = length litxs
        choices  = explode litxs
        bchoices = map (binchoice litln) choices

valid choice clauses = all (== Value True) $ map (applyc choice) clauses

applyc [] c = c
applyc ((n, v):xs) c = applyc xs $ eval c n v

binchoice len x = map (\e -> (e, elem e x)) [1..len]

explode :: [a] -> [[a]]
explode []     = []
explode [x]    = [[], [x]]
explode (x:xs) = (++) exs $ map (\xs -> [x] ++ xs) exs
  where exs = explode xs

main = do
  let t = Set.fromList [Or (Literal 1) (Literal 2), Or (Not 2) (Or (Literal 3) (Not 4)), Or (Literal 4) (Not 5)] :: CNF
  print $ solve t