module Exercise_9 where {-WETT-} import Data.List import Data.Maybe import Data.Function (on) import Data.Bifunctor import Data.IntMap.Strict (IntMap, fromList, insertWith, member, insert, (!), delete, adjust, unionWith, singleton, toList, delete, size, empty) import qualified Data.IntMap.Strict as IntMap import Data.Sequence (Seq, fromList, empty, (|>), (><), length, index, update, singleton, take, drop, elemIndexL) 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 cs = let cnf = filter (/=[top]) . map (\ls -> let fs = filter (/= bottom) ls in if top `elem` ls then [top] else fs) $ cs in if [] `elem` cnf then [[]] else cnf {-H9.2.2-} cnf :: Form -> ConjForm cnf (L m) = [[m]] cnf (fp :&: fq) = cnf fp ++ cnf fq cnf (L l :|: L m) = [[l, m]] cnf (j :|: k) = let (t, u) = (cnf j, cnf k) in [ a ++ b | a <- t, b <- u] {-H9.2.3-} -- variable is Present viP :: ConjForm -> [Name] viP = nub . map name . filter (\x -> x /= top && x /= bottom) . concat -- maximum occurence of variable in disjunctive clauses miO :: ConjForm -> [Name] -> (Name, Bool) miO cj = second (>0) . maximumBy (compare `on` snd) . map (\n -> (n, foldr (\ls i -> if ct ls n then i + 1 else i) 0 cj)) where ct ls n = Pos (Var n) `elem` ls || Neg (Var n) `elem` ls selectV :: ConjForm -> Maybe (Name, Bool) selectV cj = let scj = simpConj cj vars = viP cj firstVar = head vars in if null vars then Nothing else (if scj == [[]] || null scj then Just (firstVar, True) else Just $ miO scj vars) {-H9.2.5-} toInt :: String -> Int toInt = read name :: Literal -> Name name (Pos (Var n)) = n name (Neg (Var n)) = n name _ = "" deleteAt :: Int -> Seq a -> Seq a deleteAt i seq = Data.Sequence.take i seq >< Data.Sequence.drop (succ i) seq -- simplified clause will be reversed due to (:) simpConjSat :: ConjForm -> ConjForm -> ConjForm simpConjSat [] as = as simpConjSat (c:cs) as | null fcs = [[]] | top `elem` fcs = simpConjSat cs as | otherwise = simpConjSat cs (fcs:as) where fcs = nub $ filter (/=bottom) c -- remove duplicates -- representing (Neg and Pos), X represents special One literal clause which is [top] data Signum = N | P | X deriving (Eq, Show) type Variable = (Int, Signum) type SignMap = IntMap [Signum] -- VarMap fst = var, snd = Signmap, where fst = index of list where Var occurs and snd = -- list of types of signums in the list of the variable, eg. VarMap of 4 in [[Pos $ Var "4", Neg $ Var "4"], ..] = fromList [(4, fromList[(0, [P, N])])] type VarMap = IntMap (IntMap [Signum]) type SeqClause = Seq (Seq Variable) -- in order to deal with the indices in the sequence, during one literal rule execution the one literal -- clause won't be removed but replaced with the Sequence fromList [(0, 2)], which indicates the clause -- is True clsTrue :: Variable clsTrue = (0, X) sClsTrue :: Seq Variable sClsTrue = Data.Sequence.singleton clsTrue -- next assignment picker determined by occurences of Variable in clauses nextPick :: [(Int, IntMap [Signum])] -> [Int] nextPick = map fst . sortBy (flip compare `on` (IntMap.size . snd)) -- one literal rule assignment insertion asmLookUp :: Variable -> IntMap Bool -> SeqClause -> [(Int, [Signum])] -> Maybe (SeqClause, IntMap Bool) asmLookUp (v, s) imasm sqcls sgnmp -- if an assignment already exists, then current branch does not satisfy | IntMap.member v imasm = Nothing | otherwise = case usqcls sgnmp sqcls of Just ssq -> Just (ssq, IntMap.insert v a imasm) _ -> Nothing where a = s /= N -- assignment of variable -- cancel clauses containing v with assigment or shorten them cancel :: Signum -> Seq Variable -> Maybe (Seq Variable) cancel sig sq = case elemIndexL (v, sig) sq of -- if the resulting reduced clause is the empty clause, then dpll will stop for this branch Just i -> let n = deleteAt i sq in if n == Data.Sequence.empty then Nothing else Just n _ -> Just sq -- usqcls will update all clauses containing Variable v with its assignment and sign usqcls ::[(Int, [Signum])] -> SeqClause -> Maybe SeqClause usqcls [] sq = Just sq usqcls ((i, [P]):is) sq = let n = cancel P (index sq i) in if a then usqcls is (update i sClsTrue sq) else case n of Just ss -> usqcls is (update i ss sq) _ -> Nothing usqcls ((i, [N]):is) sq = let n = cancel N (index sq i) in if not a then usqcls is (update i sClsTrue sq) else case n of Just ss -> usqcls is (update i ss sq) _ -> Nothing usqcls ((i, _):is) sq = usqcls is (update i sClsTrue sq) -- update clause list cj under partial assignments in IntMap im, if a literal is assigned both false and true -- it returns Nothing unitSol :: Int -> SeqClause -> VarMap -> IntMap Bool -> Maybe (SeqClause, IntMap Bool, VarMap) unitSol i scnf imap imasm | i == Data.Sequence.length scnf = Just (scnf, imasm, imap) | otherwise = let -- one literal rule currClause = index scnf i -- current clause lcc = Data.Sequence.length currClause h = index currClause 0 -- first elem from currClause v = fst h tbl = toList $ imap ! v in if lcc == 1 && h /= clsTrue then case asmLookUp h imasm scnf tbl of -- olr for next clause, and delete v IntMap [Signum] from VarMap imap Just (nscnf, nimasm) -> unitSol (succ i) nscnf (IntMap.delete v imap) nimasm _ -> Nothing else unitSol (succ i) scnf imap imasm -- algorithm used : Modern Dpll : https://baldur.iti.kit.edu/sat/files/2016/l05.pdf satSol :: SeqClause -> IntMap Bool -> VarMap -> Maybe Valuation satSol sqcls imap varmap = case unitSol 0 sqcls varmap imap of -- remove all unit literal clauses Nothing -> Nothing Just (nsqcls, nimap, nvarmap) -> let nps = nextPick $ IntMap.toList nvarmap -- next variable assignment list sorted by occurences in clauses valt = Just $ map (first show) $ IntMap.toList nimap -- new assignments done = nvarmap == IntMap.empty -- all variables have been assigned in if done then valt else mdpll nps where sgnmp v = IntMap.toList (nvarmap ! v) -- SignIndexMap for v nnvarmap v = IntMap.delete v nvarmap -- updated VarMap with v's entry removed partAssig s v = asmLookUp (v, s) nimap nsqcls (sgnmp v) -- partial Assigment with s for v mdpll [] = Nothing -- no partial satisfying assignment found mdpll (v:vs) = case partAssig P v of -- check with True assignment Nothing -> case partAssig N v of -- check with False assigment Nothing -> mdpll vs Just (nnsqcls, nnimap) -> case satSol nnsqcls nnimap (nnvarmap v) of Just valuation -> Just valuation Nothing -> mdpll vs Just (nnsqcls, nnimap) -> case satSol nnsqcls nnimap (nnvarmap v) of Just valuation -> Just valuation Nothing -> case partAssig N v of Nothing -> mdpll vs Just (nnsqcls, nnimap) -> case satSol nnsqcls nnimap (nnvarmap v) of Just valuation -> Just valuation Nothing -> mdpll vs satConj :: ConjForm -> Maybe Valuation satConj cj = let scj = simpConjSat cj [] -- simplify conj (sqcls, varmap) = sqsq 0 scj (Data.Sequence.fromList []) (IntMap.fromList []) -- transform to SeqClause in if scj == [[]] then Nothing else satSol sqcls (IntMap.fromList []) varmap --------------------------------------------- set up -------------------------------------------------------------------- -- adds the signum occurences of variable d in the clause at i into the VarMap of all d's inside clause ds mapLit :: Int -> Int -> [Variable] -> VarMap -> VarMap mapLit _ _ [] im = im mapLit i j (q@(d, s):ds) im = let f = IntMap.unionWith (++) in mapLit i (succ j) ds (IntMap.insertWith f d (IntMap.singleton i [s]) im) -- transform cnf into SeqClause and keep track of each variables occurences in each clause sqsq :: Int -> ConjForm -> SeqClause -> VarMap -> (SeqClause, VarMap) sqsq _ [] s imap = (s, imap) sqsq i (cs:cnfs) s im = sqsq (succ i) cnfs (s |> Data.Sequence.fromList vblList) $ mapLit i 0 vblList im where toVbl l = case l of Pos (Var n) -> (toInt n, P) Neg (Var n) -> (toInt n, N) vblList = map toVbl cs {-H9.2.6-} sat :: Form -> Maybe Valuation sat = undefined {-TTEW-}