langthom · October 31, 2017 15:40 · Oct 31, 2017
diff --git a/SAT.hs b/SAT.hs
@@ -0,0 +1,122 @@
+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
+          ]