DPLL.hs

{- |
Module      :  <File name or $Header$ to be replaced automatically>
Description :  An implementation of DPLL in Haskell.
Copyright   :  (c) Joshua T. Guerin, Ph.D.
License     :  <license>

Maintainer  :  jguerin@utm.edu
Stability   :  experimental
Portability :  portable

<module description starting at first column>
-}

module DPLL where

import Data.List (sort, sortBy)
import Heuristics
import Common

cnf:: [[Int]]
cnf = [[16, 17, 30], [-17, 22, 30], [-17, -22, 30], [16, -30, 47], [16, -30, -47], [-16, -21, 31], [-16, -21, -31], [-16, 21, -28], [-13, 21, 28], [13, -16, 18], [13, -18, -38], [13, -18, -31], [31, 38, 44], [-8, 31, -44], [8, -12, -44], [8, 12, -27], [12, 27, 40], [-4, 27, -40], [12, 23, -40], [-3, 4, -23], [3, -23, -49], [3, -13, -49], [-23, -26, 49], [12, -34, 49], [-12, 26, -34], [19, 34, 36], [-19, 26, 36], [-30, 34, -36], [24, 34, -36], [-24, -36, 43], [6, 42, -43], [-24, 42, -43], [-5, -24, -42], [5, 20, -42], [5, -7, -20], [4, 7, 10], [-4, 10, -20], [7, -10, -41], [-10, 41, 46], [-33, 41, -46], [33, -37, -46], [32, 33, 37], [6, -32, 37], [-6, 25, -32], [-6, -25, -48], [-9, 28, 48], [-9, -25, -28], [19, -25, 48], [2, 9, -19], [-2, -19, 35], [-2, 22, -35], [-22, -35, 50], [-17, -35, -50], [-29, -35, -50], [-1, 29, -50], [1, 11, 29], [-11, 17, -45], [-11, 39, 45], [-26, 39, 45], [-3, -26, 45], [-11, 15, -39], [14, -15, -39], [14, -15, -45], [14, -15, -27], [-14, -15, 47], [17, 17, 40], [1, -29, -31], [-7, 32, 38], [-14, -33, -47], [-1, 2, -8], [35, 43, 44], [21, 21, 24], [20, 29, -48], [23, 35, -37], [2, 18, -33], [15, 25, -45], [9, 14, -38], [-5, 11, 50], [-3, -13, 46], [-13, -41, 43]]


-- | Generates a list of literals from cnf.
literals = filterDuplicates $ sort $
           map (\x->if x>0 then x else (-x)) $ flatten cnf


propagatePurify :: [[Int]] -> ([[Int]], [Int])
{- ^
  Wrapper for unitPropagate'.
  Applies unit propagation until convergence.
-}
propagatePurify cnf = propagatePurify' cnf []


propagatePurify' :: [[Int]] -> [Int] -> ([[Int]], [Int])
-- ^ Repeatedly apply unit Propagation until convergence.
propagatePurify' cnf units = 
  if newUnits==[] && pures==[] then (cnf, units)
  else propagatePurify' purified assignment
  where (propagated, newUnits) = unitPropagate cnf
        (purified, pures) = pureLiteralAssign propagated
        assignment = filterDuplicates $ sortAssign (newUnits ++ pures ++ units)


unitPropagate :: [[Int]] -> ([[Int]], [Int])
-- ^ Apply unit propagation once to cnf.
unitPropagate cnf =
  (reduceCNF units $ filter (not . clauseSat units) cnf, units)
  where units = findUnits cnf


findUnits :: (Ord a, Num a) => [[a]] -> [a]
-- ^ Generates a lit of unit clauses.
findUnits cnf = sortAssign $ findUnits' cnf
findUnits' [] = []
findUnits' (x:xs)
  | (length x) == 1 = (head x):findUnits' xs
  | otherwise = findUnits' xs


pureLiteralAssign cnf = (applyAssignment pureList cnf, pureList)
  where pureList = pureLiterals cnf


pureLiterals :: (Ord a, Num a) => [[a]] -> [a]
-- ^ Computes a list of pure literals from the cnf
pureLiterals cnf = 
  pureLiterals' positive negative
  where candidates = sort $ flatten cnf
        positive = filterDuplicates $ filter (\x->x>0) candidates
        negative = filterDuplicates $ reverse $ filter (\x->x<0) candidates


pureLiterals' :: (Ord a, Num a) => [a] -> [a] -> [a]
{- ^
  Helper function for pureLiterals
  Parameters:
    (x:xs) - A list of positive literals, ascending
    (y:ys) - A list of negative literals, descending
  Returns:
    A list of pure literals (occurs positive or negative, not both).
-}
pureLiterals' [] [] = []
pureLiterals' (x:xs) [] = (x:xs)
pureLiterals' [] (y:ys) = (y:ys)
pureLiterals' (x:xs) (y:ys)
  | x == (-y) = pureLiterals' xs ys
  | x < (-y) = x:(pureLiterals' xs (y:ys))
  | (-y) < x = y:(pureLiterals' (x:xs) ys)


contradiction :: Foldable t => [t a] -> Bool
-- ^ Checks for empty clauses (contradictions) in current theory.
contradiction cnf = foldr (||) False $ map (== 0) $ map length cnf


filterDuplicates :: Eq a => [a] -> [a]
-- ^ Filters out duplicate entries from a sorted list.
filterDuplicates [] = []
filterDuplicates [x] = [x]
filterDuplicates (x:xs) =
  if x == (head xs) then filterDuplicates xs
  else x:(filterDuplicates xs)


sortAssign list = sortBy (\x y -> if abs(x) < abs(y) then LT else GT) list

reduceCNF :: (Foldable t, Num a, Eq a) => t a -> [[a]] -> [[a]]
-- ^ Reduces opposite literals from assignment out of the CNF.
reduceCNF assignment cnf = map (reduce assignment) cnf


reduce :: (Foldable t, Num a, Eq a) => t a -> [a] -> [a]
-- ^ Reduce opposite literals from assignment out of clause.
reduce assignment clause = filter (\l ->(- l) `notElem` assignment) clause


applyAssignment :: [Int] -> [[Int]] -> [[Int]]
-- ^ Applies reduces CNF by assigned values.
applyAssignment assignment cnf = filter (not . clauseSat assignment) cnf


clauseSat :: [Int] -> [Int] -> Bool
-- ^ Returns True if assignment satisfies clause, False otherwise
clauseSat assignment clause =
 foldr (||) False $ map (check assignment) clause


check :: [Int] -> Int -> Bool
-- ^ Checks whether the literal value is the same as the value in assignment
check assignment literal = literal `elem` assignment