{-# LANGUAGE BangPatterns #-} module Exercise09 where import Types import Data.List (delete, foldl', minimumBy, sort) import Data.Maybe (fromMaybe, mapMaybe) import Data.Ord (comparing) import qualified Data.IntSet as IntSet import qualified Data.Map.Strict as Map import qualified Data.Set as Set -- import Debug.Trace (trace) -- things from the tutorial lName :: Literal -> Name lName = abs lPos :: Name -> Literal lPos = id lNeg :: Name -> Literal lNeg n = -n lIsPos :: Literal -> Bool lIsPos = isPos lIsNeg :: Literal -> Bool lIsNeg = isNeg lNegate :: Literal -> Literal lNegate l = -l complements :: Literal -> Literal -> Bool complements n n' = lNegate n == n' evalLiteral :: Valuation -> Literal -> Bool evalLiteral val l | lIsPos l = lName l `elem` val | otherwise = lName l `notElem` val evalClause :: Valuation -> Clause -> Bool evalClause v = IntSet.foldr (\x acc -> evalLiteral v x || acc) False eval :: Valuation -> ConjForm -> Bool eval = all . evalClause clauseIsTauto :: Clause -> Bool clauseIsTauto cs = IntSet.foldr (\l acc -> acc || IntSet.member (lNegate l) cs) False cs -- clauseIsTauto [] = False -- clauseIsTauto (l:ls) = lNegate l `elem` ls || clauseIsTauto ls -- homework starts here -- Functions handling DPLLData createDPLLData :: EConjForm -> DPLLData createDPLLData cf = let k = length cf form = filter (not . clauseIsTauto . snd) (zip [0..] (map toClause cf)) (ks, cl) = unzip form mkc = Map.fromList form uC = filter (unitClause . snd) form uK = Map.fromList (map (\(i, c) -> (IntSet.findMin c, i)) uC) u = IntSet.unions (map snd uC) w = getWatched form d = DPLLData { key = k, processed = [], unprocessed = ks, valuation = [], rSteps = [], clauses = Set.fromList cl, mapKeyClause = mkc, watched = w, unit = u, unitKey = uK } in d -- TODO: Apply Unit clause rule before handing over -- Get watched Literals from a set of clauses getWatched :: KeyConjForm -> WatchedLiterals getWatched cf = let lt = map (\(k, c) -> (k, (IntSet.findMin c, IntSet.findMax c))) cf in Map.fromList lt -- feel free to change behaviour and type resolve :: Name -> Clause -> Clause -> Clause resolve l cp cn = IntSet.union (IntSet.delete (lPos l) cp) (IntSet.delete (lNeg l) cn) removeLiteral :: Name -> Clause -> Clause removeLiteral l = IntSet.filter ((l /=) . lName) -- feel free to change behaviour and type resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)] resolvants (ka, ca) (kb, cb) = mapMaybe aux (IntSet.toList ca) where helper :: Literal -> (KeyClause, KeyClause) helper l = if lIsPos l then ((ka, ca), (kb, cb)) else ((kb, cb), (ka, ca)) aux :: Literal -> Maybe (Resolve, Clause) aux l = let ((kp, cp), (kn, cn)) = helper l resolvable = IntSet.member (lNegate l) cb nc = resolve (lName l) cp cn in if resolvable && not (clauseIsTauto nc) then Just (FResolve (lName l) kp kn, nc) else Nothing -- resolvants' ka kb [] ca cb -- Takes a list of processed literals, unprossesed literals, and the other clause -- Sees if the literal at the head is contained in the other clause in the opposite form -- Resolves the clause if it is --resolvants' ::Key -> Key -> Clause -> Clause -> Clause -> [(Resolve, Clause)] --resolvants' _ _ _ [] _ = [] --resolvants' a b pl (l:ul) ol -- | lNegate l `elem` ol = let c = removeLiteral (lName l) ol ++ pl ++ ul -- n = lName l -- r = if lIsPos l then FResolve n a b else FResolve n b a -- in if clauseIsTauto c then resolvants' a b (l:pl) ul ol else (r, c):resolvants' a b (l:pl) ul ol -- | otherwise = resolvants' a b (l:pl) ul ol -- proof checking -- don't change the type nor expected behaviour proofCheck :: EConjForm -> Proof -> Bool proofCheck cf (FModel vs) = vs `eval` toConjForm cf proofCheck cf (FRefutation steps) = fst (checkContradiction (length cf) (toConjForm cf) steps) checkContradiction :: Key -> ConjForm -> [Resolve] -> (Bool, ConjForm) -- checkContradiction _ cf (FResolve l cp cn:_) | trace ("l: " ++ show l ++ " cp: " ++ show (cf !! cp) ++ " cp: " ++ show (cf !! cn) ++ " nc: " ++ show (resolve l (cf !! cp) (cf !! cn))) False = undefined checkContradiction _ cf [] = (IntSet.empty `elem` cf, cf) checkContradiction k cf (FResolve l cp cn:rs) = let nc = resolve l (cf !! cp) (cf !! cn) in checkContradiction (succ k) (cf ++ [nc]) rs -- feel free to change behaviour and type selClause :: SelClauseStrategy selClause [] = Nothing selClause uc = Just $ minimumBy (comparing length) uc -- feel free to change behaviour and type resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm) resolutionParam s cf = resolutionSolver s (length cf) [] (preprocessForm cf) [] -- Is clause a Unit clause? unitClause :: Clause -> Bool unitClause c = not (IntSet.null c) && (IntSet.findMin c == IntSet.findMax c) -- Apply the Unit Clause Rule unitClauseRule :: SolverStep unitClauseRule (_, p, [], _, _, vs) = Left (FModel (extractModel (map snd p) ++ vs)) -- Get Satisfactory Model unitClauseRule a@(k, p, u, c, rs, vs) = let units = filter (unitClause . snd) (p ++ u) -- Gets all unit clauses ls = IntSet.unions (map snd units) -- Gets the literals in the unit clauses ks = keys units -- Creates a Map from a Literal (Unit clause) to it's key contra = clauseIsTauto ls -- Checks if there's a contradiction prf = FRefutation (reverse (findContradiction ls ks:rs)) -- Creates a proof based on the contradiction vs' = vs ++ filter lIsPos (IntSet.elems ls) -- Updates the valuation with the positive literals (p', k0, rs0) = simplify p ls ks k rs (u', k', rs') = simplify u ls ks k0 rs0 c' = simplifySet c ls -- Simplifies the processed and unprocessed clauses with the new valuation recurse = unitClauseRule (k', p', u', c', rs', vs') -- Recursive Call to units in if null units then Right a else if contra then Left prf else recurse -- If there are no more unit clauses go to next step -- Else if a contradiction was found then return it's proof -- Otherwise recurse -- Simplify FConjForm with a Valuation simplifySet :: FConjForm -> Clause -> FConjForm simplifySet c lt = let ng = IntSet.map lNegate lt in Set.map (`IntSet.difference` ng) (lt `simplifySetPure` c) -- Finds a contradiction in a set of Unit clauses (Represented as a clause) -- and returns the resolution step to prove it findContradiction :: Clause -> UnitClauseKeys -> Resolve findContradiction ls ks = let lp = IntSet.findMax (IntSet.filter (\l -> IntSet.member (lNegate l) ls) ls) kp = fromMaybe undefined (Map.lookup lp ks) kn = fromMaybe undefined (Map.lookup (lNegate lp) ks) in FResolve lp kp kn -- Creates a mapping from literal (unit clauses) to keys keys :: KeyConjForm -> UnitClauseKeys keys = Map.fromList . map (\(k, c) -> (IntSet.findMin c, k)) -- Pure Literal Rule WIP pureLiteralRule :: SolverStep -- pureLiteralRule a | trace (show a) False = undefined pureLiteralRule (_, _, [], c, _, vs) = Left (FModel (extractModel (Set.toList c) ++ vs)) -- Gets a Satisfactory Model pureLiteralRule a@(k, p, u, c, rs, vs) = let ls = IntSet.unions (Set.toList c) -- Literals -- Pure Literals pl = IntSet.filter ((`IntSet.notMember` ls) . lNegate) ls -- Add to valuation vs' = filter lIsPos (IntSet.toList pl) ++ vs -- Simmplify according to new valuation p' = pl `simplifyPure` p u' = pl `simplifyPure` u c' = pl `simplifySetPure` c -- Recursive call recurse = pureLiteralRule (k, p', u', c', rs, vs') in if IntSet.null pl then Right a else recurse -- Simmplifying a clause with pure literals -- No need to check if the negation appears simplifyPure :: Clause -> KeyConjForm -> KeyConjForm simplifyPure pl = filter (IntSet.null . IntSet.intersection pl . snd) simplifySetPure :: Clause -> FConjForm -> FConjForm simplifySetPure pl = Set.filter (IntSet.null . IntSet.intersection pl) -- DPLL Algorithm dpllSolver:: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm) dpllSolver s cf = let d = Right (length cf, [], preprocessForm cf, Set.fromList cf, [], []) st = fromSteps [unitClauseRule, pureLiteralRule, resolutionStep s] in (solver st d, []) -- A solver Step that does nothing noOpStep :: SolverStep noOpStep = Right -- Chains a list of SolverSteps together fromSteps :: [SolverStep] -> SolverStep fromSteps [] = undefined fromSteps (x:xs) = foldl' chainSteps x xs -- Gets resolvants of the clause selected by SelClauseStrategy resolutionStep :: SelClauseStrategy -> SolverStep resolutionStep _ (_, _, [], c, _, vs) = Left (FModel (extractModel (Set.toList c) ++ vs)) -- Gets a Satisfactory Model resolutionStep s (k, p, u, c, rs, vs) = let kc = fromMaybe undefined (s u) -- Gets a Clause to resolve against p' = kc:p -- Adds clause to processed u0 = delete kc u -- Removes it from unprocessed (k', c', u', rs') = fResolvants k c kc p u0 rs -- Gets all resolvants step = Right (k', p', u', c', rs', vs) -- Packs updated values into a Tuple in if IntSet.null (snd kc) then Left (FRefutation (reverse rs)) else step -- If the null clause was found then return Resolution steps -- Otherwise return updated values -- Gets the Resolvants of "kc" against "p" and "u" fResolvants :: Key -> FConjForm -> KeyClause -> KeyConjForm -> KeyConjForm -> [Resolve] -> (Key, FConjForm, KeyConjForm, [Resolve]) fResolvants k c kc p u rs = let (k', c', u', rs') = fResolvants' k c kc u u rs in fResolvants' k' c' kc p u' rs' fResolvants' :: Key -> FConjForm -> KeyClause -> KeyConjForm -> KeyConjForm -> [Resolve] -> (Key, FConjForm, KeyConjForm, [Resolve]) fResolvants' k c _ [] p rs = (k, c, p, rs) fResolvants' k c (ka, ca) ((kb, cb):u) p rs = let ng = IntSet.map lNegate cb lt = IntSet.toList (IntSet.intersection ca ng) (k', c', p', rs') = go k c rs p lt in fResolvants' k' c' (ka, ca) u p' rs' where go :: Key -> FConjForm -> [Resolve] -> KeyConjForm -> [Literal] -> (Key, FConjForm, KeyConjForm, [Resolve]) go nk nc nr nu [] = (nk, nc, nu, nr) go nk nc nr nu (l:ls) = let (kp, cp, kn, cn) = if lIsPos l then (ka, ca, kb, cb) else (kb, cb, ka, ca) rc = resolve (lName l) cp cn isNew = Set.notMember rc c r = FResolve (lName l) kp kn nc' = Set.insert rc nc new = go (succ nk) nc' (r:nr) ((nk, rc):nu) ls same = go nk nc nr nu ls in if isNew && not (clauseIsTauto rc) then new else same -- Chains two solver steps, shortcircuits if thefirst found a proof chainSteps :: SolverStep -> SolverStep -> SolverStep chainSteps s1 s2 d = case s1 d of Left p -> Left p Right d' -> s2 d' -- Simplifies Form by setting the value of single literal Clauses simplify :: KeyConjForm -> Clause -> UnitClauseKeys -> Key -> [Resolve] -> (KeyConjForm, Key, [Resolve]) simplify cf vs = simplify' vs (IntSet.map lNegate vs) cf [] simplify' :: Clause -> Clause -> KeyConjForm -> KeyConjForm -> UnitClauseKeys -> Key -> [Resolve] -> (KeyConjForm, Key, [Resolve]) simplify' _ _ [] pc _ k rs = (pc, k, rs) simplify' lp ln (cl@(kc, c):uc) pc ks k rs | hasCommon lp c = simplify' lp ln uc pc ks k rs | hasCommon ln c = let (r, cl', k') = removeFalse ln ks (kc, c) k in simplify' lp ln uc (cl':pc) ks k' (r ++ rs) | otherwise = simplify' lp ln uc (cl:pc) ks k rs hasCommon :: Clause -> Clause -> Bool hasCommon l c = not (IntSet.null (IntSet.intersection l c)) removeFalse :: Clause -> UnitClauseKeys -> KeyClause -> Key -> ([Resolve], KeyClause, Key) removeFalse ls ks (kc, cl) k = let lt = IntSet.intersection ls cl (rs, k') = chainResoutions ls ks kc k in (rs, (k' - 1, IntSet.difference cl lt), k') chainResoutions :: Clause -> UnitClauseKeys -> Key -> Key -> ([Resolve], Key) chainResoutions lt = chainResoutions' [] (map lNegate (IntSet.elems lt)) chainResoutions' :: [Resolve] -> [Literal] -> UnitClauseKeys -> Key -> Key -> ([Resolve], Key) -- chainResoutions' rs ls ks _ _ | trace (show rs ++ " " ++ show ls ++ " " ++ show ks) False = undefined chainResoutions' rs [] _ _ k = (rs, k) chainResoutions' rs (l:ls) ks kc k = let lk = fromMaybe undefined (Map.lookup l ks) (kp, kn) = if lIsPos l then (lk, kc) else (kc, lk) r = FResolve (lName l) kp kn in chainResoutions' (r:rs) ls ks k (succ k) -- Debug print Resolutionalgorithm Step showResolutionStep :: Key -> KeyConjForm -> KeyConjForm -> [Resolve] -> String showResolutionStep k pc uc r = "Key: " ++ show k ++ " P: " ++ show pc ++ " U: " ++ show uc ++ " R: " ++ show r -- Resolution Algorithm resolutionSolver :: SelClauseStrategy -> Key -> KeyConjForm -> KeyConjForm -> [Resolve] -> (Proof, KeyConjForm) -- resolutionSolver _ k pc uc r | trace (showResolutionStep k pc uc r) False = undefined resolutionSolver _ _ pc [] _ = (FModel $ extractModel (map snd pc), pc) resolutionSolver !s !k !pc !uc !r = let kc@(_, c) = fromMaybe undefined (s uc) pc' = kc:pc uc' = delete kc uc (nr, nc) = unzip (concatMap (resolvants kc) (uc' ++ pc)) uc'' = uc' ++ zip [k..] nc k' = k + length nc r' = nr ++ r -- Relies on laziness to not compute the above if kc is null in if IntSet.null c then (FRefutation (reverse r), pc ++ uc) else resolutionSolver s k' pc' uc'' r' -- Filters tautologies and removes duplicated literals preprocessForm :: ConjForm -> KeyConjForm preprocessForm = filter (not . clauseIsTauto . snd) . zip [0..] -- Generic solver solver :: SolverStep -> Either Proof SolverStepData -> Proof solver _ (Left pr) = pr solver s (Right d) = solver s (s d) {-WETT-} -- don't change the type; instantiate your best resolution prover here -- Please leave some comments for the MC Jr to understand your ideas and code :') resolution :: EConjForm -> (Proof, KeyConjForm) resolution = dpllSolver selClause . toConjForm {-TTEW-} -- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf extractModel :: ConjForm -> Valuation extractModel cf = run [] (sort cf) where run val [] = val run val (c:cs) | evalClause val c = run val cs | otherwise = let l = IntSet.findMax c in run (lName l:val) cs