{-# LANGUAGE ViewPatterns #-} module Exercise09 (resolution, proofCheck) where import Types import Data.List (foldl1', foldl', maximumBy, partition, sort, sortOn ) import Data.Ord (comparing, Down(Down)) import qualified Data.Set as S import qualified Data.IntMap.Strict as IM import qualified Data.IntSet as IS import Data.Bifunctor import Data.Maybe import qualified Data.List.NonEmpty as NE -- things from the tutorial lName :: ELiteral -> Name lName (Literal _ n) = n lPos :: Name -> ELiteral lPos = Literal Pos lNeg :: Name -> ELiteral lNeg = Literal Neg lIsPos :: ELiteral -> Bool lIsPos (Literal p _) = p == Pos lIsNeg :: ELiteral -> Bool lIsNeg = not . lIsPos lNegate :: ELiteral -> ELiteral lNegate (Literal Pos n) = Literal Neg n lNegate (Literal Neg n) = Literal Pos n sNegate :: Literal -> Literal sNegate = SLiteral . negate . unLiteral complementsE :: ELiteral -> ELiteral -> Bool complementsE (Literal p n) (Literal p' n') = p /= p' && n == n' complements :: Literal -> Literal -> Bool complements lit1 lit2 = lit1 == sNegate lit2 evalLiteral :: Valuation -> ELiteral -> Bool evalLiteral val l@(Literal _ n) | lIsPos l = n `elem` val | otherwise = n `notElem` val evalClause :: Valuation -> EClause -> Bool evalClause = any . evalLiteral eval :: Valuation -> EConjForm -> Bool eval = all . evalClause clauseIsTauto :: Clause -> Bool clauseIsTauto c = any (\l -> sNegate l `S.member` c) $ S.toList c type CMap = IM.IntMap Clause type CClauseSet = IS.IntSet -- feel free to change behaviour and type resolvantsN :: CMap -> Key -> Key -> [(Resolve, Clause)] resolvantsN cmap uk pk = go $ S.toList uc where uc = fromJust $ IM.lookup uk cmap pc = fromJust $ IM.lookup pk cmap go [] = [] go ( lit:lits) = let res = if unLiteral lit >= 0 then resolve lit uc pc else resolve lit pc uc rrecord = if unLiteral lit >= 0 then Resolve (show . abs . unLiteral $ lit) uk pk else Resolve (show . abs . unLiteral $ lit) pk uk in if sNegate lit `S.member` pc && not (clauseIsTauto res) then (rrecord, res) : go lits else go lits -- homework starts here -- -- feel free to change behaviour and type resolve :: Literal -> Clause -> Clause -> Clause resolve (SLiteral (abs -> n)) cp cn = S.union (S.delete (SLiteral n) cp) (S.delete (SLiteral (negate n)) cn) -- proof checking applyRes :: (Int, IM.IntMap Clause) -> EResolve -> (Int, IM.IntMap Clause) applyRes (idx, kcnf) (Resolve n k1 k2) = (succ idx, IM.insert idx rres kcnf) where rres = resolve (SLiteral $ read n) c1 c2 c1 = fromJust $ IM.lookup k1 kcnf c2 = fromJust $ IM.lookup k2 kcnf -- don't change the type nor expected behaviour proofCheck :: EConjForm -> Proof -> Bool proofCheck cnf (Refutation resolutions) = S.null lastClause where (_, lastClause) = maximumBy (comparing fst) $ IM.assocs kcnf' kcnf = IM.fromList . zip [(0::Key)..] . fmap toClause $ cnf kcnf' = snd $ foldl' applyRes (length kcnf, kcnf) resolutions proofCheck cnf (Model e) = eval e cnf isSubsumed :: Clause -> S.Set Clause -> Bool isSubsumed c0 = any (`S.isSubsetOf` c0) . S.toList isNotSubsumed :: Clause -> [Clause] -> Bool isNotSubsumed c0 = all (\c -> not $ c `S.isSubsetOf` c0) findContradiction :: CMap -> Maybe (NE.NonEmpty EResolve) findContradiction cmap = NE.nonEmpty $ contradictions where check ((k1, lit1):x2@(k2, lit2):xs) | lit1 `complements` lit2 = Resolve (show . unLiteral $ lit1) k1 k2 : check xs | otherwise = check (x2:xs) check _ = [] contradictions = check clauses clauses = sortOn snd . fmap (second S.findMin) . filter (\(_, c) -> S.size c == 1) . IM.assocs $ cmap unitPropN :: CMap -> CClauseSet -> (CMap, CClauseSet) unitPropN cmap clauses = (cmap, res) where res = IS.union clauses' (IS.fromList . fmap fst $ units) (units, composite) = partition (\(_, c) -> S.size c == 1) . fmap (\k -> (k, fromJust $ IM.lookup k cmap)) . IS.toList $ clauses units' = fmap (second S.findMin) units unitsKeys = S.fromList $ fmap snd units' negatedUnitsKeys = S.fromList $ fmap (sNegate . snd) units' clauses' = IS.fromList . fmap fst $ filter (\(_, c) -> S.null $ S.intersection c unitsKeys) composite cmap' = IM.map (\c -> S.difference c negatedUnitsKeys) cmap selClause :: CMap -> CClauseSet -> Maybe Key selClause cmap clauses | IS.null clauses = Nothing | IM.null cmap = Nothing | S.empty `elem` IM.elems cmap = Nothing | otherwise = Just . head . sortOn (\c -> S.size . fromJust $ IM.lookup c cmap) $ IS.toList clauses toOMKey :: Literal -> Int toOMKey = unLiteral type OccursMap = IM.IntMap CClauseSet updateLiteralOccursMap :: CMap -> CClauseSet -> OccursMap -> OccursMap updateLiteralOccursMap cmap clauses = go (IS.toList clauses) where go [] om = om go (c:cs) om = go cs om' where ourClauses = S.toList . fromJust $ IM.lookup c cmap om' :: OccursMap om' = goLit ourClauses om goLit :: [Literal] -> OccursMap -> OccursMap goLit [] omu = omu goLit (lit:lits) omu = goLit lits omu' where omu' = IM.alter ago (toOMKey lit) omu ago Nothing = Just $ IS.singleton c ago (Just cls) = Just $ IS.insert c cls backwardSubsumptionCheck :: OccursMap -> CClauseSet -> Clause -> CClauseSet backwardSubsumptionCheck om uc cl = subsuming where ccs = fmap (\k -> fromJust $ IM.lookup (toOMKey k) om) . S.toList $ cl ccs' = if null ccs then IS.empty else foldl1' IS.intersection ccs subsuming = IS.intersection uc ccs' -- feel free to change behaviour and type resolutionParam :: EConjForm -> (Proof, KeyConjForm) resolutionParam cnf = case contraResult of Nothing -> (res, KeyConjForm S.empty cmap1) Just contras -> (Refutation (reverse $ NE.toList contras), KeyConjForm S.empty cmap1) where contraResult = findContradiction cmap0 (res, cmap1) = go startidx [] cmap0' notautos' IS.empty initialOM cnf' = fmap toClause cnf startidx = length cnf initialOM = updateLiteralOccursMap cmap0' notautos' IM.empty cmap0 = IM.fromList $ zip [(0::Key)..] cnf' ckeys0 = IM.keysSet cmap0 (notautos, tautos) = IS.partition (not . clauseIsTauto . fromJust . flip IM.lookup cmap0) ckeys0 (cmap0', notautos') = unitPropN cmap0 notautos go :: Int -> [EResolve] -> CMap -> CClauseSet -> CClauseSet -> OccursMap -> (Proof, CMap) go _ steps cmap@(findContradiction -> Just contradictions) _ _ _ = (Refutation (reverse $ NE.toList contradictions ++ steps) , cmap) go _ _ cmap uc _ _ | IS.null uc = let model = S.toList . S.fromList . extractModel . S.fromList . IM.elems $ cmap in (Model model, cmap) go idx steps cmap uc pc om = case selClause cmap uc of Just suk -> let rsv = resolvantsN cmap suk =<< IS.toList pc known = IM.elems cmap knownS = IS.union uc pc nu' = IM.fromList . zip [idx..] $ nu (nr, nu) = unzip . filter (flip isNotSubsumed known . snd) $ rsv nuSet = IM.keysSet nu' uc' = IS.union (IS.delete suk uc) nuSet backwardSubsumptions = IS.unions $ fmap (backwardSubsumptionCheck om knownS) $ nu uc'' = IS.difference uc' backwardSubsumptions cmap' = IM.union cmap nu' (cmap'', uc''') = unitPropN cmap' uc'' steps' = reverse nr ++ steps pc' = IS.insert suk pc idx' = idx + length nu om' = updateLiteralOccursMap cmap'' nuSet om in if not (any S.null nu) then go idx' steps' cmap'' uc''' pc' om' else (Refutation (reverse steps'), cmap) Nothing -> (Refutation (reverse steps), cmap) -- feel free to change behaviour and type {-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 = resolutionParam {-TTEW-} -- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf extractModel :: ConjForm -> Valuation extractModel = run [] . sort . map (sortOn Down) . toEConjForm where run val [] = val run val (c:cs) | evalClause val c = run val cs | otherwise = run (lName (head c):val) cs