module BDDModule where import Data.List ( sort, (\\), subsequences, nub ) -- Einfacher Datentyp für OBDDs - ein OBDD ist die Einssenke, die Nullsenke oder ein Baum bestehend -- aus einem namenlosen Knoten mit einer Markierung, sowie einem linken (then) und einem rechten -- (else) Teilbaum. data OBDD = OBDD OBDD Int OBDD | Zero | One thenBranch :: OBDD -> OBDD thenBranch (OBDD left _ _) = left thenBranch _ = error "thenBranch: sink." elseBranch :: OBDD -> OBDD elseBranch (OBDD _ _ right) = right elseBranch _ = error "elseBranch: sink." root :: OBDD -> Int root (OBDD _ x _) = x root _ = error "root: sink." ---------------------------------------------------------------------------------------------------- -- Serie 6, Aufgabe 3: (fast) wie in der Übung gesehen -- ---------------------------------------------------------------------------------------------------- -- Induktiver Aufbau aussagenlogischer Formeln über einer nummerierten Variablenmenge. -- Der Einfachheit halber werden die Konstanten EFalse und ETrue für "falsch" und "wahr" benutzt. Es data Exp = Exp :+: Exp | Exp :*: Exp | Not Exp | Exp Int | EFalse | ETrue -- x_1, nx_1 infix 7 :*: infix 6 :+: -- Hiermit können Boolesche Ausdrücke leserlich angezeigt werden. instance Show Exp where show ETrue = "1" show EFalse = "0" show (e :+: e') = "(" ++ show e ++ " + " ++ show e' ++ ")" show (e :*: e') = "(" ++ show e ++ " * " ++ show e' ++ ")" show (Not e) = "-" ++ show e show (Exp n) = "x_" ++ show n -- Interpretiert man die aussagenlogischen Formeln als Funktionen in den vorkommenden -- Variablenindizes, so kann man den obigen Datentyp verwenden, um die durch einen BDD dargestellte -- Funktion zu erhalten. Die Definition entspricht genau der Definition der Vorlesung. function :: OBDD -> Exp function Zero = EFalse function One = ETrue function (OBDD left index right) = Exp index :*: function left :+: Not (Exp index) :*: function right -- x_i * ... + nx_i * ... -- Implementierung der Funktion anz aus der Vorlesung. Das Ergebnis ist nur dann korrekt, wenn es -- sich bei dem Argument um ein QOBDD handelt. anz :: OBDD -> Int anz Zero = 0 anz One = 1 anz (OBDD left _ right) = anz left + anz right -- Implementierung des Erfüllbarkeitsalgorithmus. Hierbei ist zu beachten, dass die Einträge der -- Liste gemäß der Variablenordnung zu lesen sind und nicht notwendigerweise von links nach rechts. satisfy :: OBDD -> (Bool, [Int]) satisfy Zero = (False, []) satisfy One = (True, []) satisfy (OBDD left _ right) | aThenBool = (aThenBool, 1 : aThenVar) | aElseBool = (aElseBool, 0 : aElseVar) | otherwise = (False, []) where (aThenBool, aThenVar) = satisfy left (aElseBool, aElseVar) = satisfy right -- Alternative Implementierung. Hier werden anstelle von den Variablenindizes die Variablen, welche -- als wahr zu belegen sind ausgegeben. Hierdurch braucht man die Variablenordnung nicht zu kennen. satisfy2 :: OBDD -> (Bool, [Exp]) satisfy2 Zero = (False, []) satisfy2 One = (True, []) satisfy2 (OBDD left x right) | aThenBool = (aThenBool, Exp x : aThenVar) | aElseBool = (aElseBool, aElseVar) | otherwise = (False, []) where (aThenBool, aThenVar) = satisfy2 left (aElseBool, aElseVar) = satisfy2 right -- Wertet einen BDD bezüglich einer Belegung aus. Für QOBDDs und Listen mit Belegungen in der -- Variablenordnung ist das Ergebnis richtig. Anderenfalls nicht notwendigerweise. evaluate :: OBDD -> [Bool] -> Bool evaluate Zero _ = False evaluate One _ = True evaluate (OBDD left _ right) (b:bs) | b = evaluate left bs | otherwise = evaluate right bs o1, o2, o3 :: OBDD o1 = OBDD (OBDD Zero 2 Zero) 1 (OBDD Zero 2 Zero) -- 0 o2 = OBDD (OBDD Zero 2 Zero) 1 (OBDD Zero 2 One) -- nx_1 * nx_2 o3 = OBDD (OBDD (OBDD Zero 1 One) 2 (OBDD One 1 One)) 3 (OBDD (OBDD Zero 1 Zero) 2 (OBDD One 1 Zero)) -- x_1 * x_2 * nx_3 + x_1 * nx_2 * x_3 + x_1 * nx_2 * nx_3 + nx_1 * nx_2 + nx_3 ---------------------------------------------------------------------------------------------------- -- Nachtrag zu Serie 5, Nachtrag zur Serie 6 -- ---------------------------------------------------------------------------------------------------- -- Da der satisfy-Algorithmus einer Tiefensuche entspricht, wird hier zuerst der linke Teilbaum -- ausgewertet und falls dieser keine Belegung liefert wird der rechte ausgewertet. Das Ergebnis ist -- genau dann Nothing, wenn es keine erfüllende Belegung gibt. Das Ergebnis Just trues ist so zu -- interpretieren - Just besagt, dass es eine erfüllende Belegung gibt und die Liste trues enthält -- die Variablenindizes, welche auf 1 gesetzt werden müssen, um eine erfüllende Belegung zu -- erhalten. Alle anderen Variablen können in diesem Fall beliebig gesetzt werden. satisfy3 :: OBDD -> Maybe [Int] satisfy3 Zero = Nothing satisfy3 One = Just [] satisfy3 (OBDD left x right) = case satisfy3 left of Just trues -> Just (x : trues) _ -> satisfy3 right -- eval hat als Eingabe eine Funktion von Int nach Bool, sowie eine aussagenlogische Formel und -- liefert den Wahrheitswert ab, der sich ergibt, wenn man alle Variablen gemäß der Funktion in -- tatsächliche Wahrheitswerte umwandelt und die abstrakten Operatoren :+:, :*: durch die konkreten -- || und && ersetzt. eval :: (Int -> Bool) -> Exp -> Bool eval f = eval' where eval' EFalse = True eval' ETrue = False eval' (Exp n) = f n eval' (Not e) = not (eval' e) eval' (e :+: e') = eval' e || eval' e' eval' (e :*: e') = eval' e && eval' e' -- Hier wird zunächst die vom BDD dargestellte Funktion berechnet und anschließend ausgewertet. evaluateFull :: (Int -> Bool) -> OBDD -> Bool evaluateFull f = eval f . function -- Wandelt eine Liste als wahr zu belegender Variablen in eine Funktion um. So ist das natürlich -- sehr ineffizient, weil elem ineffizient ist. Verwendet man statt einer Liste einen Datentyp mit -- schnellem Zugriff, so wird auch die Implementierung effizienter. listToFun :: [Int] -> Int -> Bool listToFun xs x = x `elem` xs -- Eine Implementierung der in Serie 6, Aufgabe 2 angegebenen Funktion. -- Im letzten Fall reicht natürlich auch die Mitnahme von nur den Booleschen Werten, wobei man dann -- aber die Variablenordnung des BDD kennen muss. Kennt man diese nicht, so ist das kein -- verwertbares Ergebnis. sats :: OBDD -> [[(Int, Bool)]] sats Zero = [] sats One = [[]] sats (OBDD left x right) = map ((x, True) :) (sats left) ++ map ((x, False) :) (sats right) -- Hier wird das anders notiert - mitgenommen werden nur jene Variablen, die wahr sein müssen und -- alle anderen (egal wieviele) werden als falsch interpretiert. Stimmt nur für QOBDDs, für ROBDDs -- müssen die Ergebnisse anders interpretiert werden, weil keine vollständigen Belegungen entstehen. sats2 :: OBDD -> [[Int]] sats2 Zero = [] sats2 One = [[]] sats2 (OBDD left x right) = map (x :) (sats2 left) ++ sats2 right -- Korrektur der sats2-Funktion für ROBDDs -- Die Funktion correct erhält als Parameter die Anzahl der Variablen in einem BDD und eine Liste -- von Variablenindizes. Diese stellen jene dar, welche wahr zu sein haben. Anschließend wird diese -- Liste an jedes Element der "Potenzliste" der fehlenden Variablen angehängt. Die Grundidee ist, -- dass die fehlenden Variablen jede Belegung zulassen und man auf diese Art und Weise genau alle -- vollständigen Belegungen erhält. correct :: Int -> [Int] -> [[Int]] correct n xs = map (++ xs) (subsequences ([1..n] \\ xs)) -- Aus der tatsächlichen Variablenzahl und einem BDD konstruieren wir zunächst alle Belegungen. -- Da diese möglicherweise unvollständig sind, werden sie anschließend vervollständigt. Auf diese -- und Weise erhält man aber etliche Belegungen mehrfach. sats2corrected :: Int -> OBDD -> [[Int]] sats2corrected varNumber = concatMap (correct varNumber) . sats2 -- Berechnet das Ergebnis von sats2corrected, sortiert die einzelnen Belegungslisten und entfernt -- dann die Duplikate. Dieser Umstand ist nur prototypisch sinnvoll. Durch das innere Sortieren -- können gleiche Listen erkannt werden ([1,2,3] und [2,1,3] stellen in unserem Sinne die gleiche -- Belegung dar, es sind aber verschiedene Listen). sats2fullyCorrected :: Int -> OBDD -> [[Int]] sats2fullyCorrected varNumber = nub . map sort . sats2corrected varNumber -- Prüft zwei BDDs auf gleiche erfüllende Belegungen. Das ist SEHR viel schlechter als der Test aus -- der Vorlesung (die Spezifikation hier ist außerordentlich aufwändig, weil erst alle erfüllenden -- Belegungen berechnet werden müssen und diese anschließend auch noch korrigiert werden). Der -- einzige Vorteil ist, dass es sich auch als Test für BDDs mit verschiedenen Variablenordnungen -- handelt und zusätzlich unabhängig davon ist, was für ein BDD genau dargestellt wird. Die einzige -- konkrete Anwendung, die wir benutzt haben war der Test, dass die BDDs von x1x2 + x3x4 + x5x6 -- bezüglich der verschiedenen (!) Variablenordnungen in der Tat korrekt berechnet waren. sameFunction :: Int -> OBDD -> OBDD -> Bool sameFunction n bdd1 bdd2 = f bdd1 == f bdd2 where f = sort . sats2fullyCorrected n