module Exercise09 where import Types import Data.List ( (\\), nub, sort, sortOn ) import Data.Ord ( Down(Down) ) import qualified Data.Set as Set import qualified Data.Map as Map import qualified Data.IntMap as IntMap -- 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 -- Takes a List of all vars that should be pos and return if the clause is pos in this case evalClause :: Valuation -> Clause -> Bool evalClause = any . evalLiteral eval :: Valuation -> ConjForm -> Bool eval = all . evalClause clauseIsTauto :: Clause -> Bool clauseIsTauto cs = not $ Set.null $ Set.filter (\lit -> Set.member (lNegate lit) cs) cs --------------------------------------------- HOMEWORK --------------------------------------------- -- homework starts here -- feel free to change behaviour and type -- Take two clauses (OR) where cp contains Pos n and cn contains Neg n and creates a single clause (OR) w/o n resolve :: Name -> Clause -> Clause -> Clause resolve i cp cn = Set.union (Set.delete (Literal Pos i) cp) (Set.delete (Literal Neg i) cn) -- feel free to change behaviour and type -- Takes two clauses (OR) with unique keys and return all possible resolves [((varName, key cp, key cn), resolve varName cp cn)] -- Asumes both clauses are ordered resolvants :: KeyClause -> KeyClause -> Set.Set (Resolve, Clause) resolvants (k1, c1) (k2, c2) = Set.foldr (Set.insert . calcRes) Set.empty $ Set.filter (\lit -> Set.member (lNegate lit) c2) c1 where calcRes (Literal Pos i) = (Resolve i k1 k2, resolve i c1 c2) calcRes (Literal Neg i) = (Resolve i k2 k1, resolve i c2 c1) -- don't change the type nor expected behaviour -- This is very slow. -- proofCheck :: EConjForm -> Proof -> (Bool, EConjForm) proofCheck :: EConjForm -> Proof -> Bool proofCheck cnf (Model val) = eval val $ toConjForm cnf --, cnf) -- If the Resolve ends before reaching the empty clause, the proof is wrong as the exersice sheet tells us -- a new step could have been generated proofCheck _ (Refutation []) = False --, cnf) proofCheck cnf (Refutation ((Resolve i k1 k2):rs)) -- If we get to the empty clause we are done as proof has proven that the ConjForm is unsatisfyable | null result = True --, cnf) -- Otherwise we can keep going | otherwise = proofCheck (cnf ++ [toEClause result]) (Refutation rs) where result = resolve i (toClause (cnf !! k1)) $ toClause (cnf !! k2) -- feel free to change behaviour and type -- :: KeyConjForm -> Maybe KeyClause -- Selects the clause with the least amoung of Symbols selClause :: SelClauseStrategy selClause kCs | Set.null kCs = Nothing | otherwise = Just $ findMinWith (Set.size . snd) kCs where findMinWith :: (Ord a, Ord b) => (a -> b) -> Set.Set a -> a findMinWith orderFunc xs = snd $ foldl (\(currMinValue, ele) currEle -> let newVal = orderFunc currEle in if newVal < currMinValue then (newVal, currEle) else (currMinValue, ele)) (let startMin = Set.findMin xs in (orderFunc startMin, startMin)) xs -- Returns true if cl1 implies cl2 i.e. cl1 c cl2 isImplicit :: Clause -> Clause -> Bool isImplicit = Set.isSubsetOf -- Resolves a whole set of KeyClauses with a single set while filtering implicit clauses resolveSet :: KeyClause -> Set.Set KeyClause -> Int -> Set.Set Clause -> Int -> (Int, [Resolve], Set.Set KeyClause, Set.Set Clause) resolveSet (k, cl) ps startingI allCl maxWeight = (lastIndex + 1, resRs, resKcls, newAllCl) where allResolves :: Set.Set (Resolve, Clause) allResolves = foldl (\overallSet currKcl@(_, currCl) -> -- We take one KeyClause from ps at a time Set.union overallSet -- And check for all possible resovles if we want to do them (takeClause newCl = True) or not and if so we -- insert it into the comSet which in the end will be put into the overallSet $ Set.foldl (\comSet lit -> let newStep@(_, newCl) = calcRes lit currKcl in if takeClause newCl then Set.insert newStep comSet else comSet ) Set.empty $ Set.filter (\lit -> Set.member (lNegate lit) currCl) cl) Set.empty ps -- For the whole set P -- Faster calculation of the Resolution since the Literal is always taken from cl calcRes :: Literal -> KeyClause -> (Resolve, Clause) calcRes (Literal Pos i) (pKey, pCl)= (Resolve i k pKey, resolve i cl pCl) calcRes (Literal Neg i) (pKey, pCl)= (Resolve i pKey k, resolve i pCl cl) -- checks if any existing clause implies this clause or the clause is always true. If so, we do not add it -- Also the maxWeightCheck is done here takeClause :: Clause -> Bool takeClause cl = Set.size cl < maxWeight && not (clauseIsTauto cl) && Set.null (Set.filter (`isImplicit` cl) allCl) lastIndex = startingI + Set.size allResolves - 1 -- We build the resolveList in such a way that the order matches the order of the KeyClauses (So that proofCheck works) (_, resRs, resKcls, newAllCl) = foldl (\(currI, rs, kcls, currAllCl) (newR, newCl) -> (currI - 1, newR:rs, Set.insert (currI, newCl) kcls, Set.insert newCl currAllCl)) (lastIndex, [], Set.empty, allCl) allResolves -- I use the algorithm which was described on the Sheet. -- The only changes are some optimizations regarding the Data Structures, Removing of Implicit clauses and Tautos -- Oh and later on I added the maxWeight which might be kind of a change. resSolver :: KeyConjForm -> KeyConjForm -> KeyConjForm -> Int -> Proof -> ConjForm -> Int -> (Proof, KeyConjForm) resSolver _ _ _ _ (Model _) _ _ = undefined resSolver originalCnf us ps currI (Refutation rs) allCls maxWeight -- If the set of clauses is "saturated" we have to check if we cannot create more clauses due to the maxWeight or if it is actually saturated | Set.null us = let resVal = extractModel $ map Set.toList $ Set.toList $ keyConjFormToConjForm ps valCorrect = eval resVal $ keyConjFormToConjForm originalCnf in -- If we found a valuation which does fullfill the cnf, we found a solution and return it. -- Here we do not have to consider maxWeight, as a correct Valuation is always a proof if valCorrect then (Model resVal, ps) -- If we did not find a correct Valuation we cannot say anything about the cnf. It might be fullfillable but it might also not -- Here we have to try again with a bigger maxWeight. -- Proof that this terminates below else resSolver originalCnf ps Set.empty currI (Refutation rs) allCls $ 2*maxWeight -- If we reached the empty clause (False) the whole cnf must be false -> We return the Resolve Steps | Set.null uc = (Refutation rs, Set.union ps us) -- If Nothing special happens we keep the same maxWeight and go again | otherwise = resSolver originalCnf newU newP newI (Refutation newRs) newAllCls maxWeight where Just kUc@(_, uc) = selClause us removedUs = Set.delete kUc us -- Here we calculate the resolve steps and all the other nice goodies (newI, addedRs, addedKCls, newAllCls) = resolveSet kUc ps currI allCls maxWeight newU = Set.union removedUs addedKCls newRs = rs ++ addedRs newP = Set.insert kUc ps {-"Proof" of termination The max amount of unique Variables inside a cnf does not change with any of the operations. We can only create different clauses but never create new variables. Hence, if at the start there are n different variables, in the end there will also be at most n different variables. Hence, a Clause can have a maxium size of 2*n (if we say Pos "1" and Neg "1" are the same var) since we are using sets -> every variable only max. twice (neg, pos) Therefore, since maxWeight >= 2 by definition and 2^n -> inf we will get to a point where every clause is accepted since it is smaller than 2^N for a big enough N the correctness for a Model was already mentioned above If we end up with an empty clause, this is also a valid Proof since we did never leave the given cnf but only reduced to possible outcomes. -} -- Removes multiple variables in the same clause, -- Removes implicit clauses ([a, ~b] => [a, c, ~b] hence [a, c, ~b] can be removed) preOpt :: EConjForm -> (Int, KeyConjForm) preOpt eCfs = (maxWeight, removedImplicitClauses) where removedMultiples = map nub eCfs keyedCfs :: EKeyConjForm keyedCfs = zip [0..] removedMultiples kcfs = ownToKeyConjForm keyedCfs removedTautos = Set.filter (not . clauseIsTauto . snd) kcfs -- Removed implied clauses (k >= clK so that we do not remove equal clauses completly) (maxWeight, removedImplicitClauses) = foldr (\(k, currCl) (currMaxW, currKcfs) -> (max currMaxW (Set.size currCl), Set.filter (\(clK, cl) -> k >= clK || not (isImplicit currCl cl)) currKcfs)) (0, removedTautos) removedTautos -- Those functions are here cuz profiling had some fucky behaviours when they were in Types.hs ownToKeyConjForm = Set.fromList . map ownToKeyClause ownToKeyClause (k, eCl) = (k, ownToClause eCl) ownToClause = Set.fromList {-WETT-} {- The basics of my Algorithm are the same, some specifications: preOpt: Removes duplicates inside clauses Removes Tautos Removes Clauses which are implied by other clauses Calculated the maximum amount of unique Variables (Pos a =/= Neg a) in a Clause selClause: Selects the clause with the least amount of unique Variables The Bigger changes I made include: When new Clauses are added by resolving, they are only added if - They are not already implied by already existing clauses - They are no tautos - They have less unique Variables than maxWeight The idea of maxWeight is, to prevent the creation of huge clauses as they will most likely just grow bigger Due to maxWeight we cannot guarantee anymore that a saturated set of clauses can be fullfilled hence we have to check that and if it is not fullfilled we increase the maxWeight and go again. For very large inputs maxWeight could be decreased to (floor $ maxWeight / 2) if the clause sizes have a high variance Nevermind, I changed it to maxLength / 2 now incase there is one long ass clause while all the others are smaller Maybe average * 1.5 might be even better but idc anymore, this is good enough -} resolution :: EConjForm -> (Proof, KeyConjForm) resolution eCfs = resSolver cfs cfs Set.empty (length eCfs) (Refutation []) (keyConjFormToConjForm cfs) maxWeight where (maxLength, cfs) = preOpt eCfs maxWeight = max 2 $ div maxLength 2 {-TTEW-} -- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf extractModel :: [[Literal]] -> Valuation extractModel = run [] . sort . map (sortOn Down) where run val [] = val run val (c:cs) | evalList val c = run val cs | otherwise = run (lName (head c):val) cs evalList :: Valuation -> [Literal] -> Bool evalList _ [] = False evalList val ((Literal Pos i):ls) = i `elem` val || evalList val ls evalList val ((Literal Neg i):ls) = notElem i val || evalList val ls -- Gets a Set and enumerates it's elements from startI -> startI + Set.size -- This should (I hope) keep the order of the Set -- Returns (NewSet, startI + Set.size newSet) enumerateSet :: Ord a => Int -> Set.Set a -> (Int, Set.Set (Int, a)) enumerateSet startI = foldl (\(currIndex, currEnumSet) ele -> (currIndex + 1, Set.insert (currIndex, ele) currEnumSet)) (startI, Set.empty) -- Taken from Georg Kreuzmayr's Zulip post makeInputAux :: [Char] -> EConjForm makeInputAux [] = [] makeInputAux ('[':xs) = makeInputAux xs makeInputAux (']':xs) = makeInputAux xs makeInputAux (',':xs) = makeInputAux xs makeInputAux xs = let clause_string = takeWhile (/= ']') xs a = clauseFromString clause_string in a:makeInputAux(xs\\clause_string) clauseFromString :: [Char] -> EClause clauseFromString [] = [] clauseFromString (',':xs) = clauseFromString xs clauseFromString ('~':xs) = let name = takeWhile (/= ',') xs in Literal Neg name:clauseFromString (xs\\name) clauseFromString xs = let name = takeWhile (/= ',') xs in Literal Pos name:clauseFromString (xs\\name) tiny = makeInputAux "[[1],[~2]]" small = makeInputAux "[[1,~4,7,3,3],[~7,~8],[~1,~4,~4,~7],[~6,~4,~7,4,2],[~5,~6,7,~3,~3],[8,4,8,7,~6],[4,~5,5],[~8,1],[~7,2,8,~5],[~1],[2,~4,1],[~8,~4],[~6,~6],[~2,7,~8,8],[4],[2],[1,1,3],[8,4],[~4,8,4,~7],[3,~5,2,6],[7,4,4,~4],[3,~5],[~6,~7,8],[~2,4,~4,2],[5,5,~2],[1,~7],[8,8,8,4,8],[8,3]]" small2 = makeInputAux "[[4,~3,8,~7],[~3],[2,~2,7,~8],[7],[5,6,~7,~3],[~4],[1,~3],[1,~8,3],[~6,7,3,4],[~7,~3,~3,~4,1],[2,~6,4],[~1,1,~1],[~6,~2,2,~6],[5,~5,~5,~2],[~1,~8],[~3,~8,1,6,7],[8],[3,~8,2,~1]]" smallMed = makeInputAux "[[~2,~2,~6],[~2,1,2,~1,~2],[9,4,5,~5,4,3],[5,2,~7],[8],[1,5,~10,~4,~3,~5,~7],[~1,~6,2,~1,~6,6,4],[2],[1,~3,3,4,10,9,~5],[2,5,8,9,~2,~6,~7,6],[7,9,10,~7],[2,~3,6,~3,~1,4],[~9,5,~7,~3],[~6,5],[3,~6,7,~10],[~5],[9,8,~7,~7,~2,5],[~6,9],[~5,~1,~8,~4,~7],[~1,~3,~6,1,8,~2,5,7],[1,~3],[7,~3,~8],[~5,6,8,7,~1,~8],[7,~3,10,~5,~6,5,6],[3,~6,7,~10],[2,~1,8,~6],[5,1,7,~10,~4,~9],[6,~9,~9],[~9,~10,~6,~1,~8,~3,~9],[~5,~10],[~9,8,~7,9,~5,~9],[~1,~2,~8,~3,8],[5,~2],[~5,10,~2,~2],[10,~4,~7,7,~2,7],[~4,4,~5,7],[~2,6],[5,~10,1,~3,~10,~8,~9],[~3]]" med = makeInputAux "[[~9,12,10,~14,~11,4,~10,12,14],[11,1,9,~10,~14,3,~9,9,1,~5],[~3,~2,~13,5,~3,~3],[~3,4],[13,4,~8,~13,~13,~5,~3,~6,12,~2],[~11],[7,8],[~6,~13,10,2,13,~8,~13,~3],[~1,3,7,~7,14],[7,~11,11,~10,~7,~5],[14,~3,3],[~8,10],[5,3,10,10,~8,10],[1,~11,~5,7,9,~3,14],[14,8,13,~1,~11,3],[~13,4,~7,5,5,4],[~8,~6,~12,4,9,~4,~5,~1],[1,~2,9,2,6,~5],[14,~14,14,~7,9,~10,9,6],[~8,~7,4],[~12,~1,14,~8],[~3,~2,~13,3,9,~14,~3],[12],[11,~14,~6,12,~8,7,9],[~1,~12,~6,7],[~12,~12],[3,10,12],[10,~7,~8,3,~13,14,~14],[~10,4],[~6,4,~14],[11],[~7],[~6,~1,9,11],[~4,10,~1,~11,5,9],[13,9,~3,~6,~3],[~3,6,5,8,8,~12,7,6,6,10],[~10,4],[~4,~14,~2],[6,~4,8,~11,5,~5,~3,13,11,~5],[5,~4,~8,~13,~7],[~6,~1,10,3,~8,~12,~2,5,8,1],[~1,3]]" medLarge = makeInputAux "[[~9,12,10,~14,~11,4,~10,12,14,~8,8,12,13,6],[11,1,9,~10,~14],[~3,~2,~13,5,~3,~3],[~3,4,~12,11,~7,6,4,~1,~7,9,~12,~6],[13,4,~8,~13,~13],[~11,~14,14,12,~2,~5,9,~8,~13,~13,1],[7,8,13,~7,~6,11,9,~13,14,~2,10,5],[~6,~13,10,2,13,~8,~13,~3],[~1,3,7,~7,14,1,~13,~7,12,9],[7,~11,11,~10,~7,~5],[14,~3,3,12,5,~4,~6,~11,2,~6,~6,12,~14],[~8,10,1,~10,10,~10,~7],[5,3,10,10,~8,10,~9,3,~13,10,2],[1,~11],[14],[~13,4,~7,5,5,4,9,~7,8,7,5],[~8,~6,~12],[1,~2,9,2,6,~5,14,~6,~10,~10,~13],[14,~14,14],[~8,~7,4,~3,~11,~10,11,~5,~6,1,~2,9,~7],[~12,~1,14,~8,~7,~10,~1,~8,5],[~3,~2,~13,3,9,~14,~3,~8,12,5,12,4],[12,3,~3,3,14,1,5,14,9,10,14],[11,~14,~6,12,~8,7,9,~12,~12,12,13,4],[~1,~12,~6,7,1,~8,~1,2,~7],[~12,~12,3,4,~6,2,14],[3,10,12,12,~6,7,~7,~8,~6,11,~6,~4,3],[10,~7,~8,3,~13,14,~14],[~10,4,8,2,~4,2,7,~4,~10,~13,13,~14],[~6,4,~14,~12,13,7,~10,1,12,5,~11,4,5],[11],[~7,9,~4,~8,~4,~10,12,~7,7,1,~4],[~6,~1,9,11,~13,~11,10,~5,6],[~4,10,~1,~11,5,9,~1,~2,~7,13,~3],[13,9,~3,~6,~3,~11,14,~6,~10,2,13,14,~2,~10,10],[~3,6,5,8,8,~12,7,6,6,10,6,~12,5,~6,5],[~10,4,4,14,~1,~6,6],[~4,~14,~2],[6,~4,8,~11,5,~5,~3,13,11,~5],[5,~4,~8,~13,~7],[~6,~1,10,3,~8],[~1,3,~3,7,~9,~14,2],[~1,~8,14,~11,~12],[~12],[~2,13,~3,~7,1,10,~4,6,~6,8,~8,~5,1,2],[5,~10,3,4,13,3,~11,~7,9],[~8,~3],[~5,12,11,~1,5,~2,~14,1,5,~1,2],[5],[~1],[~6,5,4,~3,~8,8],[1,~1,~1,~10],[9,~12,6,10,~2,11,5,~9,~7,~11,~4,~12],[~3,~9,1,~13,~14,14,~9,~6,~13,14,~13,~4,8,~13],[~5,12,~14,~14],[10,~13,~3,~11,4,~8,7,~9],[~3,~1,~1,14,10,12,8,1,~7,~5,11,~6,12],[~12,11,~4,13,~2,~3],[10,~13,5],[7,~12,~8,4,~14,~13,8,~13,~10,~9,~11,~9,~11,~1],[5,~8,6,~6,11,3,~13,~2,2,9,~14,~11,9,~6],[8,13,13,~11,12,2,3,12,7,~1,10,~13,~3],[~14,~10,~4,10,~6,~4,2,5,~6,14],[10,~9,12,11,~10,~6,4,~10],[13,2,10,~10,4,5,11,2,1,~10,2,1,~5],[1],[~13,1,~2,10,~12,~3,5,10,5,~4],[~14,~2,~6,~9,~5,~6,2,14,8,14,10,~5,~6,~1],[~12,~5,~12,14,13,~13],[~9,~9,~13,7,12,6,~3],[~7,~8,3,13,6,~9,10,8,12,~13,11,~14,~2],[~3,~10,14,~14,~11,6,4,~2,6,1,14,10,~5],[~11,13],[6,~1,2,~5],[~12,~1,~1,3,9,14,~8,~9,~9,6,5,~13,3,~5,4],[~4,14,13,8,13,13,~12,2,~14,~11,5,13,6],[7,~14,~11,~2,8,7,~14,~12,10,14,~6,4,4],[~6],[~12,4,13,4,9,~5,~14,~12,8,~11],[12,11],[1,~4,~12],[4,~4,14,11,14,~2,3,14,~7],[~3,11,~9,11,2,8,1,~13,~10,14,~11,~6,~9,5,14],[~10,1,7,~12,2,7,~11,2,~5,~10,9,~14,9],[~1,12,~12,2],[~14,3,~7,12,~4,14,7,~10,14,~4,~4],[~11,14,~9],[5,~8,7,8,~13,2,10,~14,11,~9,7,13,11],[5,8,~7,9,~11,6,6,10,1],[~2,~12,7,~10,~2],[~4,~4],[8,1,4,~6,~6,5,~12,~13,8,6,11,~2,~14,12],[9,~6,11,14],[4,13,10,10,4,~1,~2,10,10,~9,~4],[~12,~8,8,~2,10,~5,5,~7,~8,~10,2],[9],[~14,10,~13,~11,~3,2],[5,10,~8,9,10,10],[~4,~14,~11,10],[~6,~6,~1,~6],[10,~11,~9,~6,13,~4,9,~7,~8,14,~13,10,~5,4],[8,12],[9,14,~13,7,~7,~6,~2,11],[6,~12,~1],[~8,~11,~2,3,4,2],[~2,~5,~2],[~9,13,~11,1,~3,1,13,1,14,~14],[6,~12,~14,2,~4,14,~12,5,~14,2],[2,9,13,11,~9],[~2,~6,~9,5,7,12,~4,6,~5],[6,14,3,~12,~9,13,2,~9,~13,1],[~13,8,~10,~6,~13,~7,~14,5,~13,~13,12,~13,5,~7,2],[8,~3,~2,~4,13],[11,4],[12,~9,~8,~2,13,5],[~11,~8,4,13,6,14,11,~6],[14,~4],[~13,3,5,10,5,9,9,~1,~1,~13,10],[~2,12,7,4,~14,~5,14,~6,2,~9,9],[~12,2,~14,~1],[2,~1,3,~6,~9,~8,11,14,8,11],[~8,14,~8,~6,~6,6,~4,~7,~2,~12,~14,12,9,~4],[11,~4,10,~7,~5,9,~7,~7,~1,~11,2,~13,4,11],[4,9,1,~6,~10,13,5],[8,~9,6,~2,~5],[3,~3,~11,8,1,~6,5,~12],[~2,3,~3,~4,5,~1],[~11,~14,3,~2,~1,5,3,~7,~11,12,1,~10,4,~13],[~1,8,~9,~5,~6,~5,~10],[8,7,~10,11,~10,~1,~3,~10,~11,~6,~3,~4,~3,3,~1],[5,11,~6,2,4,12,8,8,~9,~3,2,11,~7,~9],[3,7],[~10,~5,14,~14],[6,~5,10,~1,5,~1,7,12,10,5,~11,~12,12,~12],[~5,7,~13,10,1,14,~12,1,8,13,7,~8,~2,~4],[6,8,4],[2,~3,~9,4,~12,1,5,1,7,~12],[6,9,8,3,~10,~5,~3,~6],[9,~8,~12,~9],[~8,4,~1,~11,14,7,13,~7,~3],[6,7,~6,1],[1,7,12,1,~4]]" myWrongEx = makeInputAux "[[1,2],[~2,~3,6],[1,3,6],[~1,2],[~1,~2,4,~5,6],[~4,5],[5,~6]" longEx = makeInputAux "[[26,~20,~12,~17,~25,~20,10,~12,18,~30,19,22,16,24,19,~30,7,~22,20,~12,~25],[23,~4,27,~27,~22,25,~3,~7],[11,~8,23,~6,4,~10,~9,2,23,22,26,~20],[~28,20,~27,15,~5,~16,~19,~1,29,~15,~23,~12,~9,27,17,16,~27,27,11,~5,~29,25],[30,27,~17,~26,~28,27,7,~29,1,14,25,~24,30,~7,~15,~24],[22,13,12,26,~5,~25,6,~18,24,27,5],[~10,~20,24,~18,~14,~5,6,~27,~19,17,14,2,~6,9,~5,~16,8,~29,24,30,25,~5,3,~11,~1,13,25,~8,12,17],[16,~19,~19,~9,~6,~16,~6,~30,~30,21],[30,~23,5,~7,26,11,14,~24,8,24,~27],[2,19,17,~16,~30,~11,~1,~2,14,~9,26,~2,24,~8,~27,7,~14],[~4,28,~9,~23,14,~6,~22,~20,~2,~13,14,~23,25,7,14,10,~24,12,~22,~24],[~26,~25,~9,23,~18,4,29,~18,~8,~23,15,~25,3,~7,~2,26,13],[~8,~30,~1,~30,~25,~3,~23,~13,22,11,~15,~14,~16],[15,~29,~21,~1,29,1,~7,30,17,~26,~27,~8,~20,~18,20,19,29,25,~11,~20,~9],[~25,20,3,~17,~12,27,22,~12,~30,8,~27,20,20,~17,~16,~16,~9,~27,22,~19,6,~22,18,15,~16,~29,6,~28,~30,~21],[12,11,27,~21,~25,26],[21,~24,30,~29,~27,~26,26],[~18,~21,9,20,~18,~19,~16,~15,~27,~10,1,15,25,~3,~14,28],[6,~29,~13,~3,~15,~16],[~28,2,~29,~7,5,~5,1,~17,11,17,19,6,28,~9,~1,25],[~1,~19,24,~10,5,4,~27,~2,~23],[~8,20,~12,7,~15],[~28,22,21,~30,~1,~4,13,3,12,5,16,~27,~26,16,~5,~4,16,~17,~6,10,14,~28,5,9,~8,28,26,~15,~25],[~25,~6,23,~5,~8,19,5,~30,3,23,7,21,17,3,~24,7,~18,~3,28,~8,~23,2,9,~9,30,~13,1,20,15],[5,~20,23,5,7,~16,~14,9],[9,16],[7,~24,4,3,9,7],[8,26,11,~29,17,~27,~3,~20,~24,~4,29,7,22,29,3,25,~6,5],[~21,5,~9,~3,~1,27,27,5,19,~1,~25,~30,~15,20,~7,18,~16,~20,~17,28,24,6,~6,12]]" ------------------------------- Old Stuff ------------------------------- {- resolvantsRec :: KeyClause -> Clause -> KeyClause -> Clause -> [(Resolve, Clause)] resolvantsRec (_, []) _ _ _ = [] resolvantsRec _ _ (_, []) _ = [] resolvantsRec keCl1@(k1, Lit p1 i1 : ls1) c1 keCl2@(k2, Lit p2 i2 : ls2) c2 -- Same variable but also same values -> goto next | i1 == i2 && p1 == p2 = resolvants (k1, ls1) keCl2 -- Same variable but p1 is Pos, p2 is Neg | i1 == i2 && p1 == Pos = (Resolfe i1 k1 k2, resolve i1 c1 c2) : resolvants (k1, ls1) keCl2 --TODO -- p2 Pos p1 Neg | i1 == i2 = (Resolfe i1 k2 k1, resolve i1 c2 c1) : resolvants (k1, ls1) keCl2 -- If different variables ignore lowest one and go to next in the lowest list | i1 < i2 = resolvants (k1, ls1) keCl2 | otherwise = resolvants keCl1 (k2, ls2) -- feel free to change behaviour and type -- :: (KeyConjForm -> Maybe KeyClause) -> [Clause] -> (Prrof, [(Key, Clause)]) -- :: selClause -> C -> (ExtractModel(P), P) resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm) resolutionParam selClause cs = resolutionParamRec selClause (conjFormToKeyConjForm cs) [] (length cs) (Refugee []) -- :: selClause -> U -> P -> currKey -> proof -> (proof, P u U) resolutionParamRec :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> Int -> Proof -> (Proof, KeyConjForm) resolutionParamRec _ [] ps _ _ = (SuperModel (extractModel $ keyConjFormToConjForm ps), ps) resolutionParamRec _ _ _ _ (SuperModel _) = undefined resolutionParamRec selClause us ps currKey (Refugee rs) | null (snd uc) = (Refugee rs, ps ++ us) | otherwise = resolutionParamRec selClause newNewU newP newKey (Refugee newRs) where Just uc = selClause us newU = delete uc us allResolves = [resolvants uc pc | pc <- ps] -- [[(Resolve, Clause)]] newClauses = concatMap (map snd) allResolves -- concat [[Clause]] = [Clause] newResolves = concatMap (map fst) allResolves newRs = rs ++ newResolves newKeyClauses = zip [currKey..] newClauses newNewU = newU ++ newKeyClauses newP = ps ++ [uc] newKey = currKey + length newClauses -- This was --orderingSet = Set.unions $ -- Set.map (Set.filter (\(_, cl) -> not $ Set.member cl allCls)) $ -- removes already existing clauses -- Set.map (resolvants kUc) ps -- Set (Set (Resolve, Clause)) --(newI, enumeratedOrderingSet) = enumerateSet currI orderingSet -- The Ordering in this is important: -- FoldR makes it so that the largest key is used first -> we build rs from behing -- Hence in the end rs !! k will produce they keyClause with key k (I hope) --(newTempRs, newkCls) = Set.foldr (\(k, (r, cl)) (rs, kClSet) -> (r:rs, Set.insert (k, cl) kClSet)) ([], Set.empty) enumeratedOrderingSet --newAllCls = Set.union allCls $ Set.map snd newkCls -- (newI, newKcfs) = enumerateSet currI newCls -}