module Exercise_9 where {-WETT-} import Data.List import Data.Maybe type Name = String type Valuation = [(Name,Bool)] data Atom = T | Var Name deriving (Eq, Show) data Literal = Pos Atom | Neg Atom deriving (Eq, Show) data Form = L Literal | Form :&: Form | Form :|: Form deriving (Eq, Show) type Clause = [Literal] type ConjForm = [Clause] {-T9.3.2-} top :: Literal top = Pos T bottom :: Literal bottom = Neg T {-T9.3.3-} clauseToForm :: Clause -> Form clauseToForm [] = L bottom clauseToForm ls = foldr ((:|:) . L) (L $ last ls) (init ls) conjToForm :: ConjForm -> Form conjToForm [] = L top conjToForm ds = foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds) {-T9.3.4-} substLiteral :: Valuation -> Literal -> Literal substLiteral v l@(Pos (Var n)) = case lookup n v of Just b -> if b then top else bottom Nothing -> l substLiteral v l@(Neg (Var n)) = case lookup n v of Just b -> if b then bottom else top Nothing -> l substLiteral v l = l substClause :: Valuation -> Clause -> Clause substClause = map . substLiteral substConj :: Valuation -> ConjForm -> ConjForm substConj = map . substClause {-H9.2.1-} simpConj :: ConjForm -> ConjForm simpConj clauses = if elem [] simple then [[]] else simple where simple = map (filter (/=bottom)) $ filter (notElem top) clauses {-H9.2.2-} cnf :: Form -> ConjForm cnf (L l) = [[l]] cnf (l :&: r) = (cnf l) ++ (cnf r) cnf (l :|: r) = [lc ++ rc | lc <- cnf l, rc <- cnf r] getVarName (Pos (Var name)) = name getVarName (Neg (Var name)) = name {-H9.2.3-} selectV :: ConjForm -> Maybe (Name, Bool) selectV clauses = if null clauses then Nothing else if not $ null isect then Just (getVarName $ head isect, True) else if null notEmpty then Nothing else Just (getVarName $ head $ head notEmpty, True) where onlyVars = map (filter (\l -> l/=Pos T && l/= Neg T)) clauses isect = foldl1 intersect onlyVars notEmpty = filter (not . null) onlyVars {-H9.2.5-} {- Optimised for time spent with familiy -} satConj :: ConjForm -> Maybe Valuation satConj clauses = if null simple then Just [] else if simple == [[]] then Nothing else let allVars = foldl1 union simple nextVar = getVarName $ head allVars trueVal = (nextVar, True) falseVal = (nextVar, False) substTrue = substConj [trueVal] clauses satTrue = satConj substTrue in if isJust satTrue then Just (trueVal:fromJust satTrue) else let substFalse = substConj [falseVal] clauses satFalse = satConj substFalse in if isJust satFalse then Just (falseVal:fromJust satFalse) else Nothing where simple = simpConj clauses {-H9.2.6-} sat :: Form -> Maybe Valuation sat = satConj . cnf {-TTEW-}