module Exercise_9 where {-WETT-} import Data.Maybe import qualified Data.IntMap.Strict as IntMap import qualified Data.Array as Array --Das ist wohl etwas aus dem ruder gelaufen --import Debug.Trace main = print(satConjDPLLArray clBig) --for debugging type Name = String type Valuation = [(Name,Bool)] data Atom = T | Var Name deriving (Eq, Show) data Literal = Pos Atom | Neg Atom deriving (Eq, Show) data Form = L Literal | Form :&: Form | Form :|: Form deriving (Eq, Show) type Clause = [Literal] type ConjForm = [Clause] -- positions in arr bucket staticRelevance preferedValue type LitLiteral = ([(Int, Int)], (Int, Int, Literal)) type Bucket = IntMap.IntMap LitLiteral type ClauseArr = Array.Array Int Literal --maybe better (Literal, Int(LowestOccurence)) -- say if the clause = [top] type ConjFormArr = Array.Array Int ClauseArr a = Pos (Var "10") b = Pos (Var "11") c = Pos (Var "12") d = Pos (Var "13") aNeg = Neg (Var "10") bNeg = Neg (Var "11") cNeg = Neg (Var "12") dNeg = Neg (Var "13") cl = [[a,b,c], [aNeg, bNeg], [d]] clST = [[a,aNeg]] clF = [[a],[aNeg]] clBig = [[Neg (Var "8"),Neg (Var "7")], [Neg T,Pos (Var "6")], [Pos (Var "1")], [Neg (Var "1"),Neg (Var "9")], [Neg (Var "5")], [Pos T], [Neg (Var "9"),Neg (Var "11"),Pos T], [Pos (Var "2"),Pos (Var "10"),Pos (Var "2")], [Neg (Var "3"),Neg (Var "4"), Pos (Var "11")], [Neg (Var "3"),Pos (Var "10"),Neg (Var "7")], [Neg (Var "9")],[Pos (Var "5"),Pos (Var "6")], [Neg (Var "10"),Pos (Var "10"),Pos (Var "14")], [Neg (Var "5")], [Pos (Var "6"),Pos T], [Neg (Var "1"),Pos (Var "4"),Neg (Var "14")], [Neg (Var "6"),Neg (Var "4")]] clBig2 = [[Pos (Var "9"),Neg (Var "10")], [Pos (Var "3")], [Neg (Var "4"),Pos T], [Pos (Var "5")], [Pos (Var "14"),Neg (Var "4")], [Neg (Var "11"),Neg (Var "12"),Neg (Var "15")], [Neg (Var "15")], [Neg (Var "7"),Pos (Var "10")], [Neg T,Pos (Var "9")], [Neg (Var "1"),Neg (Var "14")], [Pos (Var "12")]] {-T9.3.2-} top :: Literal top = Pos T bottom :: Literal bottom = Neg T {-T9.3.3-} clauseToForm :: Clause -> Form clauseToForm [] = L bottom clauseToForm ls = Prelude.foldr ((:|:) . L) (L $ last ls) (init ls) conjToForm :: ConjForm -> Form conjToForm [] = L top conjToForm ds = Prelude.foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds) {-T9.3.4-} substLiteral :: Valuation -> Literal -> Literal substLiteral v l@(Pos (Var n)) = case Prelude.lookup n v of Just b -> if b then top else bottom Nothing -> l substLiteral v l@(Neg (Var n)) = case Prelude.lookup n v of Just b -> if b then bottom else top Nothing -> l substLiteral _ l = l substClause :: Valuation -> Clause -> Clause substClause = Prelude.map . substLiteral substConj :: Valuation -> ConjForm -> ConjForm substConj = Prelude.map . substClause {-H9.2.1-} simpConj :: ConjForm -> ConjForm simpConj [] = [] simpConj cs = case aux cs of Nothing -> [[]] (Just cs) -> cs where aux [] = (Just []) aux (cl:cs) = case aux cs of Nothing -> Nothing (Just cs) -> case s_cl of [] -> Nothing [Pos T] -> (Just cs)--j s_cl -> (Just (s_cl : cs)) where s_cl = shortened cl shortened cl = topAdjst [l | l <- cl, l /= bottom] topAdjst cl = if elem (Pos T) cl then [Pos T] else cl --data Form = L Literal | Form :&: Form | Form :|: Form {-H9.2.2-} cnf :: Form -> ConjForm cnf (L l) = [[l]] cnf (fl :&: fr) = (cnf fl) ++ (cnf fr) cnf (fl :|: fr) = conc (cnf fl) (cnf fr) where conc fl fr = [cl ++ cr | cl<-fl, cr<-fr] {-H9.2.3-} --VAR SELECTION ALGORYTHMS --version for the tests, --this version doesn't expect the simplified version and thus doesn't neceserily return --nothing if the formula is unsolvable selectV :: ConjForm -> Maybe (Name, Bool) selectV [] = Nothing selectV (cl:cf) | simpleStrat /= Nothing = simpleStrat | otherwise = case firstVar cl of Nothing -> selectV cf (Just (Pos (Var name))) -> Just (name, True) (Just (Neg (Var name))) -> Just (name, False) _ -> Just ("Bools wherent filtered out corectly", False) where simpleStrat = selectV_smallestClausel $ simpConj (cl:cf) firstVar [] = Nothing firstVar (l:cl) = case l of (Pos (Var name)) -> Just (Pos (Var name)) (Neg (Var name)) -> Just (Neg (Var name)) _ -> firstVar cl --I RETURN VAR FROM SMALLEST CLAUSEL --strategie 1: return a variable which is in one of the clauseln with the lowest amount of variables --this function only expects the simplified version selectV_smallestClausel :: ConjForm -> Maybe (Name, Bool) selectV_smallestClausel cf = case literal of Nothing -> Nothing (Just (Pos (Var name))) -> Just (name, True) (Just (Neg (Var name))) -> Just (name, False) _ -> Just ("Bools wherent filtered out corectly", False) where (literal, _) = aux cf aux [] = (Nothing, -1) aux ([var] : _) = (Just var, 1) aux (cl:cf) = if restVar == Nothing || (lenCl < lenSmallest && firstVar /= Nothing) then (firstVar, lenCl) else (restVar, lenSmallest) where lenCl = length cl firstVar = firstVarFun cl firstVarFun [] = Nothing firstVarFun cl = Just $ head cl (restVar, lenSmallest) = aux cf {- PREPROCESS FORMULA, PUT VARS INTO PRIORITY BUCKETS, PUT CONJFORM INTO ARRAY, ATTACH TO EVERY VAR INDEXES TO ARRAY Bucket Rules: smallestClauseSize == 1 -> Bucket 1, at CDCF smallestClauseSize == 2 -> Bucket 2, smallestClauseSize == 3 -> Bucket 3, smallestClauseSize >= 4 -> Bucket 4, later: sign_value >= 0.8 (|pos_occurence-neg_occurence|/total_occurence) -> var goes_to_lower_bucket occurence high enough -> var goes to higher bucket -var van max go one bucket higher, through non smallest clause size stuff -to bucket one a var can only go through smallest clause size stuff -> TODO TODO: save for each klausel its amount of variables -> faster top recognition -} type DataCollector = ([(Int, Int)], (Int, Literal)) -- input formula formula as array, list of buckets a leteralin a bucket looks like that: Map (varId, ([pos_of_cl, pos_in_cl] , [lowest_occurence, ... , bucket_id]) preprocess :: ConjForm -> (ConjFormArr, (Bucket, Bucket, Bucket, Bucket))--each bucket will berealized by its own map --create hash --iterate through formula, add new vars to hash, save smallest clausel, and positions in formula --to make debugging easier currently everything is being put into the first bucket preprocess cf = (cfAsArray, toBuckets $ IntMap.map calcBucket (varMap cf 0) ) --it would be more efficient if clalcBucket was part of toBuckets where cfAsArray = Array.listArray (0, length cf -1) [clAsArray | cl <- cf, let clAsArray = Array.listArray (0, length cl -1) cl] varMap :: ConjForm -> Int -> IntMap.IntMap DataCollector varMap [] _ = IntMap.fromList [] varMap (cl:cf) xPos = addClausel cl (varMap cf (xPos+1)) xPos 0 (length cl) where addClausel :: Clause -> IntMap.IntMap DataCollector -> Int -> Int -> Int -> IntMap.IntMap DataCollector addClausel [] map _ _ _= map addClausel (lit:cl) map xPos yPos length | varId == -1 = addClausel cl map xPos (yPos+1) length | otherwise = addClausel cl mapUpdated xPos (yPos+1) length where (varId, nBool) = case lit of (Pos (Var nm)) -> (read nm :: Int, (Pos T)) (Neg (Var nm)) -> (read nm :: Int, (Neg T)) _ -> error "bool didnt got filtered out correctly" varM = map IntMap.!? varId mapUpdated = case varM of Nothing -> IntMap.insert varId ((xPos, yPos) : [] , (length, nBool)) (addClausel cl map xPos (yPos+1) length) (Just (positions, (minLength, bool))) -> if length < minLength then IntMap.insert varId (((xPos, yPos) : positions), (length, nBool)) (addClausel cl map xPos (yPos+1) length) else IntMap.insert varId (((xPos, yPos) : positions), (minLength, bool)) (addClausel cl map xPos (yPos+1) length ) toBuckets :: Bucket -> (Bucket, Bucket, Bucket, Bucket) toBuckets varMap = aux $ IntMap.toList varMap where aux [] = (IntMap.fromList [], IntMap.fromList [], IntMap.fromList [], IntMap.fromList []) aux ( (key,(positions, (bucket, dec, bool))) : vars) = case bucket of 1 -> (IntMap.insert key (positions, (bucket, dec, bool)) map1, map2, map3, map4) 2 -> (map1, IntMap.insert key (positions, (bucket, dec, bool)) map2, map3, map4) 3 -> (map1, map2, IntMap.insert key (positions, (bucket, dec, bool)) map3, map4) 4 -> (map1, map2, map3, IntMap.insert key (positions, (bucket, dec, bool)) map4) _ -> error "invalid bucket" where (map1, map2, map3, map4) = aux vars calcBucket :: DataCollector -> LitLiteral calcBucket (positions , (smallestOccurence, bool)) = (positions, (bucket, dec, bool)) where dec = 0 --this will be changed and set according to attributes bucket = if smallestOccurence < 4 then smallestOccurence else 4 --UPDATE BUCKETS -> only smallest Clause Size is changing --SUBSTITUATION ALGORYTHMS --SIMPLE SUBSTITUATION ON LIST --replaces every var with that name with that bool subst_native :: (Name, Bool) -> ConjForm -> ConjForm subst_native _ [] = [] subst_native (name, bool) (cl: cf) = clSubst : subst_native (name, bool) cf where clSubst = [varN | literal <- cl, let varN = if (Pos (Var name)) == literal then posReplacor else if literal == (Neg (Var name)) then negReplacor else literal, varN /= (Neg T)]--little optimation (posReplacor, negReplacor) = if bool then ((Pos T), (Neg T)) else ((Neg T), (Pos T)) --SUBSTITUATION ON OPTIMIZED DATA STRUCTURE -- updated buckes num of clauses which became [top] -> -1->subtet conjform == [[]] substArray :: LitLiteral -> ConjFormArr -> (Bucket, Bucket, Bucket, Bucket) -> (ConjFormArr, (Bucket, Bucket, Bucket, Bucket), Int) substArray ([], _) arr buckets = (arr, buckets, 0) substArray (((posX, posY): positions), (bucket,bucketDec,val)) arr buckets -- | trace ("substituting: " ++ show ((arr Array.! posX)Array.! posY)) False = undefined | isTop = substArray (positions, (bucket,bucketDec,val)) arr buckets | isSubstedTop == -1 = (substedClauselArr, (IntMap.empty, IntMap.empty, IntMap.empty, IntMap.empty), -1) | otherwise = (substedArr, recUpdatedBuckets, (numTops)) where numTops | isSubstedTop == -1 || numTopsSubsted == -1 = -1 | otherwise = isSubstedTop + numTopsSubsted (substedArr, recUpdatedBuckets, numTopsSubsted) = substArray (positions, (bucket,bucketDec,val)) substedClauselArr updatedBuckets unSubstedClausel = arr Array.! posX isTop = (containsPosVal (snd(Array.bounds unSubstedClausel)) unSubstedClausel) substedClauselArr = arr Array.// [(posX, (arr Array.! posX) Array.// [(posY, substVal)])] substVal = if trueVal == val then (Pos T) else (Neg T) trueVal = case (arr Array.! posX) Array.! posY of (Pos _) -> (Pos T) (Neg _) -> (Neg T) substedClausel = substedClauselArr Array.! posX updatedBuckets = if numVars >= 6 then buckets else updateBuckets buckets (snd(Array.bounds substedClausel)) numVars = numVarsAux (snd(Array.bounds substedClausel)) substedClausel 0 numVarsAux :: Int -> ClauseArr -> Int -> Int numVarsAux i arr acc | i == -1 = acc | acc >= 6 = 6 --we dont care about the num if there are more than 6 | otherwise = numVarsAux (i-1) arr (acc + isVar) where isVar = case arr Array.! i of (Pos (Var _)) -> 1 (Neg (Var _)) -> 1 _ -> 0 updateBuckets :: (Bucket, Bucket, Bucket, Bucket) -> Int -> (Bucket, Bucket, Bucket, Bucket) updateBuckets (b1, b2, b3, b4) i | i == -1 = (b1, b2, b3, b4) | varKey == -1 = updateBuckets (b1, b2, b3, b4) (i-1) | fromB == 2 && originalBucket - relevance -1 == 1 = updateBuckets (IntMap.insert varKey litLit b1, IntMap.delete varKey b2, b3, b4) (i-1) | fromB == 3 && originalBucket - relevance -1 == 2 = updateBuckets (b1, IntMap.insert varKey litLit b2, IntMap.delete varKey b3, b4) (i-1) | fromB == 4 && originalBucket - relevance -1 == 3 = updateBuckets (b1, b2, IntMap.insert varKey litLit b3, IntMap.delete varKey b4) (i-1) | otherwise = updateBuckets (b1, b2, b3, b4) (i-1) where varKey = case substedClausel Array.! i of (Pos (Var nm)) -> read nm :: Int (Neg (Var nm)) -> read nm :: Int _ -> -1 (fromB, (positions, (originalBucket, relevance, literal))) = findBucket varKey findBucket key | IntMap.member key b2 = (2, b2 IntMap.! key) | IntMap.member key b3 = (3, b3 IntMap.! key) | IntMap.member key b4 = (4, b4 IntMap.! key) | IntMap.member key b1 = (-1, ([], (0,0,(Pos T)))) --this is redundant, otherwise = (-1, ..) would do, i just use it to be able to throw the error message below | otherwise = error ("key not found in bucket, either it was put of from the buket to early or not correctly removed form array\nkey: " ++ show varKey ++ "\nb1: " ++ show b1 ++ "\nb2: " ++ show b2++ "\nb3: " ++ show b3++ "\nb4: " ++ show b4 ++ "\n SubstedClausel :" ++ show substedClausel) litLit = (positions, ((originalBucket-1), relevance, literal)) --updated literal isSubstedTop -- | trace ("numVars in subst: " ++ show numVars ++ " containsPos Val: " ++ show (containsPosVal (snd(Array.bounds substedClausel)) substedClausel)) False = undefined | containsPosVal (snd(Array.bounds substedClausel)) substedClausel = 1 | numVars > 0 = 0 | otherwise = -1 containsPosVal i clausel | i == -1 = False | otherwise = case clausel Array.! i of --is a little bit unefficient!!! (Pos T) -> True _ -> containsPosVal (i-1) clausel --_-> error "inalid pattern from substed 1clausel, !maybe! numVars doesnt work correctly" {-H9.2.5-} --FINAL ALGORYTHMS satConj :: ConjForm -> Maybe Valuation satConj f = satConjDPLL f --SIMPLE DPLL --for this to be dpll selectV must return the variable which dpll would choose haha satConjDPLL :: ConjForm -> Maybe Valuation satConjDPLL f | f' == [] = Just [] | f' == [[]] = Nothing | f'_varD /= Nothing = Just((var, value) : (fromJust f'_varD)) | f'_varND /= Nothing = Just((var, not value) : (fromJust f'_varND)) | otherwise = Nothing where f' = simpConj f f'_varD = satConjDPLL $ subst_native (var, value) f' f'_varND = satConjDPLL $ subst_native (var, not value) f' Just (var, value) = selectV_smallestClausel f' --DPLL WITH OPTIMIZED DATA STRUCTURE satConjDPLLArray :: ConjForm -> Maybe Valuation --on first call --simplify formula, check if formula already true or false: unlikly satConjDPLLArray cf = case simpConj cf of [[]] -> Nothing [] -> Just [] cf -> case preprocess cf of (arr, buckets) -> aux arr buckets 0 --preprocess: formula to array - generate varBuckets where --on every recursiv call -- num non[top] clauses, -1 formual == [[]] aux :: ConjFormArr -> (Bucket, Bucket, Bucket, Bucket) -> Int -> Maybe Valuation aux arr (b1,b2,b3,b4) numTops -- | trace ("numTops in aux: " ++ show numTops) False = undefined ---- | trace ("testVarL: " ++ show (substArray varL arr bucketsAfterTakeOut)) False = undefined | numTops == -1 = Nothing --check if formula verifiable (numTops != -1) | numTops == snd(Array.bounds arr)+1 = Just [] | solution /= Nothing = solution --aux (subst varL formuala) || aux (subst varR formula) -- | trace ("found dead end.") False = undefined | otherwise = Nothing where --try out varL and varR solution = if testVarL /= Nothing then case testVarL of Just evaluation -> Just (valuL : evaluation) _ -> error "testVarL has invalid pattern" else case test varR of Just evaluation -> Just (valuR : evaluation) Nothing -> Nothing testVarL = test varL --2. substArray, recive updated buckets, new amount of tops test var = case substArray var arr bucketsAfterTakeOut of (substedArr, newBuckets, newTops) -> aux substedArr newBuckets (numTopsSupsted newTops) numTopsSupsted newTops = if newTops == -1 then -1 else newTops + numTops --1. take var out of bucket --minViewWithKey :: IntMap a -> Maybe ((Key, a), IntMap a) (varL, bucketsAfterTakeOut) = case IntMap.minView b1 of --next time i will put the buckets into a list Just (var, newB1) -> (var, (newB1, b2, b3, b4)) Nothing -> case IntMap.minView b2 of Just (var, newB2) -> (var, (b1, newB2, b3, b4)) Nothing -> case IntMap.minView b3 of Just (var, newB3) -> (var, (b1, b2, newB3, b4)) Nothing -> case IntMap.minView b4 of Just (var, newB4) -> (var, (b1, b2, b3, newB4)) Nothing -> error "all buckets seem to be empty, but no [[]] or [] was identified. :(" varR = case varL of (positions, (bucket, releveance, Pos T)) -> (positions, (bucket, releveance, Neg T)) (positions, (bucket, releveance, Neg T)) -> (positions, (bucket, releveance, Pos T)) _ -> error "invalid pattern from varL, probably there is some funcktion putting variables into the litLiterals" (valuL, valuR) = case varL of (((x,y):_), (_,_,Pos T)) -> ((getName x y, True), (getName x y, False)) (((x,y):_), (_,_,Neg T)) -> ((getName x y, False), (getName x y, True)) _ -> error "invalid pattern from varL, !maybe! some function doesnt remove it from a bucket where it should" getName x y = case (arr Array.! x) Array.! y of (Pos (Var nm))->nm (Neg (Var nm))->nm _->error "val in array where a var should be" --CDCL WITH OPTIMIZED DATA STRUCTURE {-H9.2.6-} sat :: Form -> Maybe Valuation sat f = satConj $ cnf f {-TTEW-}