module Exercise09 where import Types import Data.List (sort, sortOn) import Data.Ord (Down(Down)) import Data.Maybe import Data.HashSet (union, delete, member, map, toList, intersection, empty) -- things from the tutorial 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 -> EClause -> Bool evalClause = any . evalLiteral eval :: Valuation -> EConjForm -> Bool eval = all . evalClause -- TODO better solution clauseIsTauto :: Clause -> Bool clauseIsTauto c = clauseIsTautoR (toList c) where clauseIsTautoR [] = False clauseIsTautoR (l:ls) = lNegate l `elem` ls || clauseIsTautoR ls -- homework starts here -- feel free to change behaviour and type resolve :: Name -> Clause -> Clause -> Clause resolve name cp cn = delete (Literal Pos name) cp `union` delete (Literal Neg name) cn -- feel free to change behaviour and type resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)] resolvants keyClause1 keyClause2 = resolvantsRec keyClause1 keyClause2 (getCommonVariables (snd keyClause1) (snd keyClause2)) where getCommonVariables a b = toList (Data.HashSet.map lName a `intersection` Data.HashSet.map lName b) resolvantsRec _ _ [] = [] resolvantsRec (k1,c1) (k2,c2) (v:vs) | member (Literal Pos v) c1 && member (Literal Neg v) c2 = (Resolve v k1 k2, resolve v c1 c2):(if null (resolve v c1 c2) then [] else resolvantsRec (k1,c1) (k2,c2) vs) | member (Literal Neg v) c1 && member (Literal Pos v) c2 = (Resolve v k2 k1, resolve v c2 c1):(if null (resolve v c2 c1) then [] else resolvantsRec (k1,c1) (k2,c2) vs) | otherwise = resolvantsRec (k1,c1) (k2,c2) vs -- proof checking -- don't change the type nor expected behaviour toKeyCNF :: EConjForm -> EKeyConjForm toKeyCNF cnf = toKeyCNFRec cnf 0 where toKeyCNFRec [] _ = [] toKeyCNFRec (x:xs) i = (i,x):toKeyCNFRec xs (i + 1) proofCheck :: EConjForm -> Proof -> Bool proofCheck cnf (Model val) = eval val cnf proofCheck _ (Refutation []) = False proofCheck cnf (Refutation ((Resolve var s1 s2):ss)) | s1 >= length cnf || s2 >= length cnf = False | otherwise = null newClause || proofCheck (cnf ++ [toEClause newClause]) (Refutation ss) where newClause = resolve var (toClause (cnf !! s1)) (toClause (cnf !! s2)) -- feel free to change behaviour and type selClause :: SelClauseStrategy selClause cnf | null cnf = Nothing | otherwise = selClauseRec cnf (-1, empty) where selClauseRec [] res = Just res selClauseRec ((key, clause):ss) (resKey, resClause) | null clause = Nothing | resKey == -1 || length clause < length resClause = selClauseRec ss (key, clause) | otherwise = selClauseRec ss (resKey, resClause) equivalentKeyClause :: KeyClause -> KeyClause -> Bool equivalentKeyClause (_, c1) (_,c2) = c1 == c2 isInForm :: KeyClause -> KeyConjForm -> Bool isInForm _ [] = False isInForm c1 (c2:cs) = snd c1 == snd c2 || isInForm c1 cs resolutionParam :: SelClauseStrategy -> EConjForm -> (Proof, KeyConjForm) resolutionParam strategy cnf | foundEmpty = (Refutation result, resU ++ resP) | otherwise = (Model (extractModel (toEConjForm (Prelude.map snd (resU ++ resP)))), resU ++ resP) where (resU, resP, result, foundEmpty) = resolutionRec (preprocessClauses cnf 0) [] [] preprocessClauses [] _ = [] preprocessClauses (c:cs) i = (i, toClause c) : preprocessClauses cs (i + 1) resolutionRec [] p res = ([], p, res, False) resolutionRec u p res = if isNothing uc then (u, p, res, True) else resolutionRec newU newP newRes where uc = strategy u (nr, nu) = formatResolvants (concat [resolvants (fromJust uc) x | x <- p]) (length cnf + length res) where formatResolvants [] _ = ([], []) formatResolvants (x:xs) i = (fst x : ra, (i, snd x) : rb) where (ra,rb) = formatResolvants xs (i + 1) newRes = res ++ nr newU = [x | x <- u, x /= fromJust uc] ++ [x | x <- nu, not (isInForm x p), not (isInForm x u), not (clauseIsTauto (snd x))] newP = p ++ [fromJust uc] {-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 selClause {-TTEW-} -- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf extractModel :: EConjForm -> Valuation extractModel = run [] . sort . Prelude.map (sortOn Down) where run val [] = val run val (c:cs) | evalClause val c = run val cs | otherwise = run (lName (head c):val) cs -- tests -- [2,2],[3],[~2,1,~3] tiny :: EConjForm tiny = [[Literal Pos "2", Literal Pos "2"], [Literal Pos "3"], [Literal Neg "2", Literal Pos "1", Literal Neg "3"]] -- [~a,b,c][~c,a][~a][~b,a][b] small :: EConjForm small = [[Literal Neg "a", Literal Pos "b", Literal Pos "c"],[Literal Neg "c", Literal Pos "a"],[Literal Neg "a"], [Literal Neg "b", Literal Pos "a"], [Literal Pos "b"]] -- [~a,b,c][~c,a][a][~b,a][b] smallSat :: EConjForm smallSat = [[Literal Neg "a", Literal Pos "b", Literal Pos "c"],[Literal Neg "c", Literal Pos "a"],[Literal Pos "a"], [Literal Neg "b", Literal Pos "a"], [Literal Pos "b"]] medium :: EConjForm medium = [[Literal Neg "2",Literal Neg "2",Literal Neg "6"],[Literal Neg "2",Literal Pos "1",Literal Pos "2",Literal Neg "1",Literal Neg "2"],[Literal Pos "9",Literal Pos "4",Literal Pos "5",Literal Neg "5",Literal Pos "4",Literal Pos "3"],[Literal Pos "5",Literal Pos "2",Literal Neg "7"],[Literal Pos "8"],[Literal Pos "1",Literal Pos "5",Literal Neg "10",Literal Neg "4",Literal Neg "3",Literal Neg "5",Literal Neg "7"],[Literal Neg "1",Literal Neg "6",Literal Pos "2",Literal Neg "1",Literal Neg "6",Literal Pos "6",Literal Pos "4"],[Literal Pos "2"],[Literal Pos "1",Literal Neg "3",Literal Pos "3",Literal Pos "4",Literal Pos "10",Literal Pos "9",Literal Neg "5"],[Literal Pos "2",Literal Pos "5",Literal Pos "8",Literal Pos "9",Literal Neg "2",Literal Neg "6",Literal Neg "7",Literal Pos "6"],[Literal Pos "7",Literal Pos "9",Literal Pos "10",Literal Neg "7"],[Literal Pos "2",Literal Neg "3",Literal Pos "6",Literal Neg "3",Literal Neg "1",Literal Pos "4"],[Literal Neg "9",Literal Pos "5",Literal Neg "7",Literal Neg "3"],[Literal Neg "6",Literal Pos "5"],[Literal Pos "3",Literal Neg "6",Literal Pos "7",Literal Neg "10"],[Literal Neg "5"],[Literal Pos "9",Literal Pos "8",Literal Neg "7",Literal Neg "7",Literal Neg "2",Literal Pos "5"],[Literal Neg "6",Literal Pos "9"],[Literal Neg "5",Literal Neg "1",Literal Neg "8",Literal Neg "4",Literal Neg "7"],[Literal Neg "1",Literal Neg "3",Literal Neg "6",Literal Pos "1",Literal Pos "8",Literal Neg "2",Literal Pos "5",Literal Pos "7"],[Literal Pos "1",Literal Neg "3"],[Literal Pos "7",Literal Neg "3",Literal Neg "8"],[Literal Neg "5",Literal Pos "6",Literal Pos "8",Literal Pos "7",Literal Neg "1",Literal Neg "8"],[Literal Pos "7",Literal Neg "3",Literal Pos "10",Literal Neg "5",Literal Neg "6",Literal Pos "5",Literal Pos "6"],[Literal Pos "3",Literal Neg "6",Literal Pos "7",Literal Neg "10"],[Literal Pos "2",Literal Neg "1",Literal Pos "8",Literal Neg "6"],[Literal Pos "5",Literal Pos "1",Literal Pos "7",Literal Neg "10",Literal Neg "4",Literal Neg "9"],[Literal Pos "6",Literal Neg "9",Literal Neg "9"],[Literal Neg "9",Literal Neg "10",Literal Neg "6",Literal Neg "1",Literal Neg "8",Literal Neg "3",Literal Neg "9"],[Literal Neg "5",Literal Neg "10"],[Literal Neg "9",Literal Pos "8",Literal Neg "7",Literal Pos "9",Literal Neg "5",Literal Neg "9"],[Literal Neg "1",Literal Neg "2",Literal Neg "8",Literal Neg "3",Literal Pos "8"],[Literal Pos "5",Literal Neg "2"],[Literal Neg "5",Literal Pos "10",Literal Neg "2",Literal Neg "2"],[Literal Pos "10",Literal Neg "4",Literal Neg "7",Literal Pos "7",Literal Neg "2",Literal Pos "7"],[Literal Neg "4",Literal Pos "4",Literal Neg "5",Literal Pos "7"],[Literal Neg "2",Literal Pos "6"],[Literal Pos "5",Literal Neg "10",Literal Pos "1",Literal Neg "3",Literal Neg "10",Literal Neg "8",Literal Neg "9"],[Literal Neg "3"]] medium2 :: EConjForm medium2 = [[Literal Pos "1", Literal Neg "3", Literal Neg "2"], [Literal Pos "1", Literal Neg "3", Literal Neg "2", Literal Neg "4"], [Literal Pos "5", Literal Pos "6"], [Literal Pos "6", Literal Neg "1"], [Literal Neg "8"], [Literal Pos "7", Literal Neg "6", Literal Pos "1"], [Literal Neg "7"]] {- 0 [~2,~2,~6] 1 [~2,1,2,~1,~2] 2 [9,4,5,~5,4,3] 3 [5,2,~7] 4 [8] 5 [1,5,~10,~4,~3,~5,~7] 6 [~1,~6,2,~1,~6,6,4] 7 [2] 8 [1,~3,3,4,10,9,~5] 9 [2,5,8,9,~2,~6,~7,6] 10 [7,9,10,~7] 11 [2,~3,6,~3,~1,4] 12 [~9,5,~7,~3] 13 [~6,5] 14 [3,~6,7,~10] 15 [~5] 16 [9,8,~7,~7,~2,5] 17 [~6,9] 18 [~5,~1,~8,~4,~7] 19 [~1,~3,~6,1,8,~2,5,7] 20 [1,~3] 21 [7,~3,~8] 22 [~5,6,8,7,~1,~8] 23 [7,~3,10,~5,~6,5,6] 24 [3,~6,7,~10] 25 [2,~1,8,~6] 26 [5,1,7,~10,~4,~9] 27 [6,~9,~9] 28 [~9,~10,~6,~1,~8,~3,~9] 29 [~5,~10] 30 [~9,8,~7,9,~5,~9] 31 [~1,~2,~8,~3,8] 32 [5,~2] 33 [~5,10,~2,~2] 34 [10,~4,~7,7,~2,7] 35 [~4,4,~5,7] 36 [~2,6] 37 [5,~10,1,~3,~10,~8,~9] 38 [~3] ------ 39 [~6] 40 [~6] 41 [~2,~9] 42 [~9] -}