Basic SAT solver

Sat.hs

module Sat where

-- A variable, e.g. p, q, r...
type Var = Int
-- A parity, either False (¬) or True (not ¬)
type Parity = Bool
-- A literal, e.g. ¬p, q, ¬r
type Literal = (Int, Bool)
-- A sequence of literals, which are combined by ||
type Clause = [Literal]
-- A sequence of clauses, which are combined by &&
type Formula = [Clause]

findOneLiteralClauses :: Formula -> [Literal]
findOneLiteralClauses formula = [literal | [literal] <- formula]

eliminateLiteral :: Literal -> Formula -> [Formula]
eliminateLiteral (var, parity) [] = [[]]
eliminateLiteral (var, parity) (clause:formula) = case clause of
  [(var', parity')]
    | var == var' && parity /= parity' -> [] -- contraditiction
  _ | (var, parity) `elem` clause -> eliminateLiteral (var, parity) formula
    | otherwise -> fmap (filter (\(var', _) -> var /= var') clause :)
      (eliminateLiteral (var, parity) formula)

splitOnVariable :: Var -> Formula -> [Formula]
splitOnVariable variable formula = do
  positiveElimination <- eliminateLiteral (variable, True) formula
  negativeElimination <- eliminateLiteral (variable, False) formula
  [positiveElimination, negativeElimination]

solve :: Formula -> [Formula]
solve formula =
  case findOneLiteralClauses formula of
    (literal:_) -> eliminateLiteral literal formula >>= solve
    [] -> case formula of
      [] -> pure [] -- we're done!
      ([]:_) -> [] -- no solution
      -- split on the first variable we see
      (((var,_):_):_) -> splitOnVariable var formula >>= solve

sat :: Formula -> Bool
sat = not . null . solve