-- File: dpll.hs
-- Author: Keith Schwarz (htiek@cs.stanford.edu)
--
-- An implementation of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm
-- for CNF-SAT.  In a naive algorithm for SAT, one would pick a variable,
-- set that variable to be true or false, then recursively check whether
-- the resulting clauses are satisfiable.  If so, the algorithm reports
-- success, and otherwise it tries the other assignment.  DPLL improves on
-- this system by adding in two optimizations that tend to cut down the
-- search space:
--
-- 1. Unit Propagation: If a clause has exactly one literal in it, the only
--    possible way to satisfy the entire formula is to make that literal true.
--    DPLL does this and propagates the result through the rest of the
--    formula.
--
-- 2. Pure Literal Propagation: If every instance of a particular variable
--    is the same (either x or ~x), then it's possible to set that variable
--    such that every clause containing it is immediately satisfied.  In some
--    cases, this can dramatically cut down on the amount of branching
--    needed.
--
-- Neither of these optimziations by themselves improve on the worst-case
-- exponential runtime of the naive SAT algorithm, but under the (generally
-- believed) assumption that P != NP it's unlikely that any set of
-- optimizations like this will be able to do so.  Nonetheless, DPLL is
-- fairly fast in practice and not too difficult to implement.
module DPLL where
import Data.List(nub, elem, notElem)

-- Type: Literal
--
-- A literal in a CNF formula, which is either a variable or its negation.
data Literal a = Yes a | Not a
                  deriving (Eq, Show)

-- Type: Clause
--
-- A list of literals.  By convention, the empty clause is unsatistifable.
type Clause a = [Literal a]

-- Type: Formula
--
-- A list of clauses.
type Formula a = [Clause a]

-- Utility function: negate
--
-- Returns the negation of a literal
negateLiteral :: Literal a -> Literal a
negateLiteral (Yes x) = Not x
negateLiteral (Not x) = Yes x

-- Utility function: findUnit
--
-- Returns an arbitrary unit literal of a formula, or Nothing if one does
-- not exist.
findUnit :: Formula a -> Maybe (Literal a)
findUnit (c:cs) = if length c == 1 then Just (head c) else findUnit cs
findUnit []     = Nothing

-- Utility function: resolve
--
-- Given a formula and a literal, returns the updated formula formed by setting the
-- indicated variable to the specified value.  This works by first removing all
-- clauses that contain the indicated literal (since they're all resolved), then
-- removing from each other clause all copies of the negation of that literal.
resolve :: (Eq a) => Formula a -> Literal a -> Formula a
resolve f literal = let f' = filter (literal `notElem`) f in -- Get rid of satisfied clauses
                    map (filter (/= (negateLiteral literal))) f'    -- Remove negations from clauses


-- Utility function: unitPropagate
--
-- Applies the unit propagation optimization to a list of clauses.
unitPropagate :: (Eq a) => Formula a -> Formula a
unitPropagate f = case findUnit f of
                     Nothing -> f                           -- No units; we're done
                     Just a -> unitPropagate $ resolve f a  -- Set the literal to true and repeat

-- Utility function: isPure
--
-- Given a literal and a formula, returns whether that literal is pure in the formula.
-- This is true if the literal's negation appears nowhere in the formula.
isPure :: (Eq a) => Formula a -> Literal a -> Bool
isPure f l = (negateLiteral l) `notElem` (concat f)

-- Utility function: findPureLiteral
--
-- Given a list of clauses, finds a pure literal and returns it if one exists.
-- This works 
findPureLiteral :: (Eq a) => Formula a -> Maybe (Literal a)
findPureLiteral f = locatePureLiteral f (nub $ concat f)
                    where locatePureLiteral f (l:ls) = if isPure f l then Just l else locatePureLiteral f ls
                          locatePureLiteral f []     = Nothing

-- Utility function: purePropagate
--
-- Applies the pure literal propagation optimization to a list of clauses
purePropagate :: (Eq a) => Formula a -> Formula a
purePropagate f = case findPureLiteral f of
                    Nothing -> f                           -- No pure literals, so do nothing
                    Just a  -> purePropagate $ resolve f a -- Found something, repeat

-- Function: dpll
--
-- Applies the DPLL algorithm and returns whether the given formula is satisfiable.
dpll :: (Eq a) => Formula a -> Bool
dpll f = if [] == f then True                                  -- No clauses left means we're done.
         else if [] `elem` f then False                        -- If there is an unsatisfiable clause, we're done 
              else
                  let f' = purePropagate $ unitPropagate f in  -- Apply pure literal propagation and unit propagation
                  let nextLiteral = head $ head f in           -- Next literal to guess on is the first remaining literal
                  dpll (resolve f nextLiteral) || dpll (resolve f (negateLiteral nextLiteral))