module Exercise09 where import Types import Data.List import Data.Ord (Down(Down)) --import Debug.Trace -- things from the tutorial instance Show Polarity where show Pos = "" show Neg = "~" instance Show ELiteral where show (Literal p a) = show p ++ a lName :: Literal -> Name lName (Literal _ n) = n lPos :: Name -> Literal lPos = Literal Pos lNeg :: Name -> Literal lNeg = Literal Neg lIsPos :: Literal -> Bool lIsPos (Literal p _) = p == Pos lIsNeg :: Literal -> Bool lIsNeg = not . lIsPos lNegate :: Literal -> Literal lNegate (Literal Pos n) = Literal Neg n lNegate (Literal Neg n) = Literal Pos n complements :: Literal -> Literal -> Bool complements (Literal p n) (Literal p' n') = p /= p' && n == n' evalLiteral :: Valuation -> Literal -> Bool evalLiteral val l@(Literal _ n) | lIsPos l = n `elem` val | otherwise = n `notElem` val evalClause :: Valuation -> Clause -> Bool evalClause = any . evalLiteral eval :: Valuation -> ConjForm -> Bool eval = all . evalClause clauseIsTauto :: Clause -> Bool clauseIsTauto [] = False clauseIsTauto (l:ls) = lNegate l `elem` ls || clauseIsTauto ls -- homework starts here isNotSubsumed:: Clause -> [Clause] -> Bool isNotSubsumed clause cs = not (or [ and [ l `elem` clause| l <- c] | c <- cs]) -- feel free to change behaviour and type resolve :: Name -> Clause -> Clause -> Clause resolve n cp cn = nub (delete (Literal Pos n) cp ++ delete (Literal Neg n) cn) -- feel free to change behaviour and type resolvants :: (Key, [ELiteral]) -> (Key, [ELiteral]) -> [(Resolve, Clause)] resolvants (k1, ls1) (k2, ls2) = nubbedRes where possibleRes = [(Resolve name k1 k2, resolve name ls1 ls2)| (Literal Pos name) <- ls1, (Literal Neg name2) <- ls2, name == name2, (not.clauseIsTauto) (resolve name ls1 ls2) ] ++ [(Resolve name k2 k1, resolve name ls2 ls1) | (Literal Neg name) <- ls1, (Literal Pos name2) <- ls2, name == name2, (not.clauseIsTauto) (resolve name ls2 ls1) ] nubbedRes = removeSubsumedSec [ (k,pr) | (k,pr) <-possibleRes, not (clauseIsTauto pr)] removeSubsumedSec :: Eq a => [(a,Clause)] -> [(a,Clause)] removeSubsumedSec [] = [] removeSubsumedSec kcs = [ (x,y) | (x,y) <- savekcs, let (_,kks) = unzip (delete (x,y) savekcs) in isNotSubsumed y kks] where savekcs = removeSecDupl kcs (xs, ys) = unzip savekcs removeSecDupl :: Eq a => [(a,Clause)] -> [(a,Clause)] removeSecDupl [] = [] removeSecDupl ((x,y):kcs) | y `clauseElem` ys = removeSecDupl kcs | otherwise = (x,y) : removeSecDupl kcs where (xs, ys) = unzip kcs clauseEq :: Clause -> Clause -> Bool clauseEq c1 c2 = length c1 == length c2 && and [c `elem` c2 | c <- c1] clauseElem :: Clause -> [Clause] -> Bool clauseElem c [] = False clauseElem c (x : xs) = clauseEq c x || clauseElem c xs -- proof checking -- don't change the type nor expected behaviour proofCheck :: ConjForm -> Proof -> Bool proofCheck conj (Model v) = eval v conj proofCheck conj (Refutation []) = [] `elem` conj proofCheck conj (Refutation (Resolve name k1 k2 : rest)) = Literal Pos name `elem` cl1 && Literal Neg name `elem` cl2 && proofCheck (conj ++ [resolve name cl1 cl2]) (Refutation rest) where cl1 = nub (conj !! k1) cl2 = nub (conj !! k2) -- feel free to change behaviour and type selClause :: SelClauseStrategy --select clause with least length, which should be the head of the list selClause (x:_) = Just x -- feel free to change behaviour and type resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm) resolutionParam select conj = resolution0 (length conj - 1) filteredKeyedConj [] [] select where keyedConj = zip [0 ..] conj filteredKeyedConj = sortBy (\(_, c1) (_, c2) -> compare (length c1) (length c2)) [(k, nub c) | (k,c) <- keyedConj, not (clauseIsTauto c)] --trace (concat ["rec: chosen: ", show chosen,"\n\tunprocessed: ", show unprocessed, "\n\tprocessed: ", show processed, "\n"]) $ resolution0::Int -> [EKeyClause] -> [EKeyClause] -> [EResolve] -> SelClauseStrategy -> (Proof, KeyConjForm) resolution0 highestKey unprocessed processed resSteps select | null unprocessed = let (_, n) = unzip processed in (Model (extractModel n), processed) -- | clauseIsTauto selVal = resolution0 (highestKey + length newClauses) newnewUnprocessed newProcessed newRes select | null chosenClause = (Refutation newRes, sortKey (processed ++ unprocessed)) | otherwise = resolution0 (highestKey + length newClauses) unprocessed3 processed2 newRes select where Just chosen = select unprocessed --which is selClause (_, chosenClause) = chosen --get [Literal] from chosen, for (_, unproce) = unzip unprocessed (_, proce) = unzip processed --(nr, nu) = (unzip.concat) [ filter (\( _ , g ) -> not (clauseIsTauto g) && g /= chosenClause && isNotSubsumed g unproce && isNotSubsumed g proce) (resolvants chosen p) | p <- processed, chosen /= p] resol = concat [resolvants chosen p | p <- processed] (nr, nu) = unzip [ (res, clau) | (res, clau) <- resol, isNotSubsumed clau proce, isNotSubsumed clau unproce] newRes = resSteps ++ nr --add new resolution steps newClauses = zip [(highestKey + 1) .. ] nu --give new clauses a key unprocessed1 = delete chosen unprocessed -- move chosen clause to processed processed1 = chosen : processed -- --unprocessed2 = [ (k, un) | (k,un) <- unprocessed1, isNotSubsumed un nu ] --remove sub from new clauses --processed2 = [(k,pr) | (k,pr) <- processed1, isNotSubsumed pr nu ] unprocessed2 = removeSubsumedSec unprocessed1 processed2 = removeSubsumedSec processed1 unprocessed3 = newClauses `union` unprocessed2 -- append newly created clauses to unprocessed sortKey = sortBy (\(a,_) (b,_) -> compare a b) --tests conjFromList:: [[Integer]] -> ConjForm conjFromList xss = [clauseFromList xs| xs <- xss] clauseFromList::[Integer] -> Clause clauseFromList xs = [ if x < 0 then Literal Neg (show (-x)) else Literal Pos (show x)| x <- xs] clause1 = conjFromList [[1,2,3],[-3],[-2], [-1]] clause2 = conjFromList [[3,-3],[-1,-1,-2],[-3,-2,1]] clause3 = conjFromList [[1,2], [-1,-2]] clause4 = conjFromList [[-2,9,-14,-2,12,10,-5,8,12,-8,6],[13,5,-14,2,2,7,11,-5,-1,9,-10,-11,-3,2,-6],[-1,-4,-4,8,-4,-6,9,13,2,-11,12,-14,-8,-11],[-5],[14,-14,-14,-5,-6,-2,5,2,-12,12,-1,-13,-2],[-1,12,11,-5,-12,-6,2,-2],[-13,-1,5,-8,-9,10,7],[-12,-11,-1,4],[-6,9,6,-7,14,1,-13,-10,6,4,-13,-1,-6,3],[-1,-1,10,3,-2,-4,-3,-4,1,12,12,-6,6,-12,10],[2,-4,5,2,-10,13,-8,9,-10,-13,8,-11,4],[-12,-5,-9,-8],[11,5],[-14,-11,8],[4,-11,-11,1,-6,-4,14,-8,1,-5,8],[13,5,11,5],[-5,14,4,-3,13,7,6,13,-9],[-13,4,10,1,1,-12,4,-14,12,6,13,-9,-7,-14,9],[2,10,10,-1,-14,-2,14,6,12,-3,5,10,-13],[2,-6,14,14,-2,14,6,-11,-5],[7,-2,-2,-9,-7],[-10,-10,-3,-4],[12,8,3,-9,-6,-11,14,3,6,10,13,-12,-5,10],[-13,-10,-8,11,-9,-12,9,-11,14,5,-5,-10,-4,-3],[5,2,12,14,-13,13,13,1,5,-2,-3,5,-1,-2,-5],[-8,-8,3,6],[7,5,14,4],[-2,11,-9,6,3,9,-10,-9,-7,3,-8,-2,12],[14,-6,1,13,-2,-12]] clause5 = conjFromList [[6,-8,7,-6],[-4,-1,-4,-1],[6],[6],[5,2,-3,-5,2],[5,5,2],[8,4],[8,-5,-3],[8,2,-7],[-4],[-2],[4,6],[2,-1,-2],[7,-2],[-7,6,-7,6],[-8],[7,6,2],[-5,-4,6],[4,5,3,-6,-1],[-1],[-6,3,3,-1],[8,4,8],[-8,-8,-6],[3,-6,3],[-3,-5],[7,-8],[-8],[7,-5],[-7,-5,8,8,-3],[-8,6,5,4],[-4,1]] clause6 = conjFromList [[-5,6],[-5,-2,-7,3,5],[-6,5,6,-7,2],[-6,-7,-4,-3,5],[8,-3,-2],[7,7],[8,7,2],[3,7,-3,-6],[-6,-2,-5],[3,-7],[-7,3,-7]] cla1 = clauseFromList [1,2,3] cla2 = clauseFromList [1,2,3,4] cla3 = zip [0..] (conjFromList [[-13,-1,-8,-9,7,-12,6],[-13,-1,-8,-9,7,-12,6,-4]]) fastres = resolutionParam selClause {-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 :: ConjForm -> (Proof, KeyConjForm) resolution = resolutionParam selClause {-TTEW-} -- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf instance Ord Polarity where Neg <= Pos = False _ <= _ = True instance Ord ELiteral where (Literal p a) <= (Literal p' a') = a < a' || a == a' && p <= p' extractModel :: ConjForm -> Valuation extractModel = run [] . sort . map (sortOn Down) where run val [] = val run val (c:cs) | evalClause val c = run val cs | otherwise = run (lName (head c):val) cs