SAT.hs

module SAT where

-- simple file for generating an SLD tree (TESTED ON ONE FORMULA ONLY!)
-- (c) Thomas Lang, 2017

import Data.List

-- A literal, can be either positive or negative
data Literal = L String
             | NEG String
             deriving (Ord, Eq)

-- A clause is simply a list of literals (or a set precisely)
newtype Clause = C [Literal] deriving Eq

-- A formula can be a literal, a conjunction or disjunction.
data Formula = LIT Literal
             | AND [Formula]
             | OR  [Formula]

instance Show Literal where
    show (L   str) = str
    show (NEG str) = "¬" ++ str
               
instance Show Clause where
    show (C []) = "{}"
    show (C xs) = "{" ++ intercalate "," (map show xs) ++ "}"

instance Show Formula where
    show (LIT  l) = show l
    show (AND fs) = intercalate " /\\ " (map (\f -> "(" ++ show f ++ ")") fs)
    show (OR  fs) = intercalate " \\/ " (map (\f -> "(" ++ show f ++ ")") fs)

data SLDTree = Leaf Clause
             | Branch [(Clause, SLDTree)]

showTree :: SLDTree -> String
showTree = showTree' 0

showTree' :: Int -> SLDTree -> String
showTree' _ (Leaf   l) = "<" ++ show l ++ ">"
showTree' i (Branch b) = let indentation = replicate i '\t'
                         in concat $ map (\(n,t) -> "\n" ++ indentation ++ show n ++ ":" ++ showTree' (i+1) t) b

instance Show SLDTree where
    show = showTree


-- Generates a SLD tree.
-- assumes one question clause only
genSLDTree :: Formula -> SLDTree
genSLDTree f = let clauses  = formClauses f
                   question = getQuestion clauses
               in Branch [(question, genSLDTree' question clauses)]

genSLDTree' :: Clause -> [Clause] -> SLDTree
genSLDTree' question clauses = let nextLevel = sldNextLevel question clauses
                               in case nextLevel of
                                    [] -> Leaf question
                                    cs -> Branch $ map (\c -> (c, genSLDTree' c clauses)) cs

sldNextLevel :: Clause -> [Clause] -> [Clause]
sldNextLevel question     [] = []
sldNextLevel question (c:cs) = case resolutionStep question c of
                                 Nothing -> sldNextLevel question cs
                                 Just r  -> r : sldNextLevel question cs


getQuestion :: [Clause] -> Clause
getQuestion         []                      = error "No question clause found!"
getQuestion ((C c):cs) | all isNegLiteral c = C c
                       | otherwise          = getQuestion cs

isNegLiteral :: Literal -> Bool
isNegLiteral (L   lit) = False
isNegLiteral (NEG lit) = True


resolutionStep :: Clause -> Clause -> Maybe Clause
resolutionStep (C ls) (C ms) = case (resolutionStep' (ressort ls) (ressort ms) 0) of
                                 Just c  -> Just $ C c
                                 Nothing -> Nothing
    where
      ressort :: [Literal] -> [Literal]
      ressort = sort

      opposed :: Literal -> Literal -> Bool
      opposed (L   l1) (NEG l2) = l1 == l2
      opposed (NEG l1) (L   l2) = l1 == l2
      opposed        _        _ = False
      
      resolutionStep' :: [Literal] -> [Literal] -> Int -> Maybe [Literal]
      resolutionStep' ls [] _ = Nothing
      resolutionStep' [] ms _ = Nothing
      resolutionStep' ls ms i = if length ls == i
                                then Nothing
                                else case find (opposed (ls!!i)) ms of
                                       Just m  -> (Just . rmdups) $ (ls \\ [ls!!i]) ++ (ms \\ [m])
                                       Nothing -> resolutionStep' ls ms (i + 1)

      rmdups :: (Ord a) => [a] -> [a]
      rmdups = map head . group . sort


-- assumes CNF
formClauses :: Formula -> [Clause]
formClauses (OR  xs) = [C $ map (\(LIT lit) -> lit) xs]
formClauses (AND xs) = concat $ map formClauses xs
formClauses (LIT  l) = [C [l]]


lit :: String -> Bool -> Formula
lit str True  = LIT (L str)
lit str False = LIT (NEG str)

example :: Formula
example = AND [
           OR [lit "B" True, lit "C" False],
           OR [lit "A" False, lit "B" False],
           OR [lit "A" True, lit "B" False, lit "C" False],
           lit "C" True
          ]