Arbeitsgruppe Rechnergestützte Programmentwicklung

KielerLandtag.pdf

BDDModule.hs

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

TestGames_01.hs

module TestGames where import BDDModule ---------------------------------------------------------------------------------------------------- -- BDD aus der Vorlesung, Aufbau: Bottom-Up. Diese Aufbau-Reihenfolge ist wichtig, weil es sich -- anderenfalls immer nur um vollständige Entscheidungsdiagramme handelt. bdd :: OBDD bdd = OBDD left3 1 right3 where left3 = OBDD left2 2 left2 right3 = OBDD left2 2 right2 left2 = OBDD left1 3 right1 right2 = OBDD right1 3 right1 left1 = OBDD One 4 Zero right1 = OBDD Zero 4 Zero -- BDD für x1*x2 bezüglich der Variablenordnung (1, 2). bddAnd :: OBDD bddAnd = OBDD left 1 Zero where left = OBDD One 2 Zero -- BDD für x1+x2 bezüglich der Variablenordnung (1, 2). bddOr :: OBDD bddOr = OBDD One 1 (OBDD One 2 Zero) -- ROBDD für x1x2 + x3x4 +x5x6 bzgl. der Ordnung (1, 3, 5, 2, 4, 6). largeBDD :: OBDD largeBDD = OBDD three1 1 three2 where three1 = OBDD five1 3 five2 three2 = OBDD five3 3 five4 five1 = OBDD two1 5 two2 five2 = OBDD two3 5 two4 five3 = OBDD four1 5 four2 five4 = OBDD six 5 Zero two1 = OBDD One 2 four1 two2 = OBDD One 2 four2 two3 = OBDD One 2 six two4 = OBDD One 2 Zero four1 = OBDD One 4 six four2 = OBDD One 4 Zero six = OBDD One 6 Zero -- ROBDD für x1x2 + x3x4 +x5x6 bzgl. der Ordnung (1, 2, 3, 4, 5, 6). smallBDD :: OBDD smallBDD = OBDD two 1 three where two = OBDD One 2 three three = OBDD four 3 five four = OBDD One 4 five five = OBDD six 5 Zero six = OBDD One 6 Zero ---------------------------------------------------------------------------------------------------- danishParliamentWeirdRules :: OBDD danishParliamentWeirdRules = OBDD two1 1 two2 where two1 = OBDD three1 2 three2 two2 = OBDD three2 2 three2 three1 = OBDD four1 3 four2 three2 = OBDD four3 3 four3 four1 = OBDD five1 4 five2 four2 = OBDD five2 4 five3 four3 = OBDD five4 4 five4 five1 = OBDD six1 5 six2 five2 = OBDD six2 5 six3 five3 = OBDD six3 5 six4 five4 = OBDD six4 5 six4 six1 = OBDD seven1 6 seven2 six2 = OBDD seven2 6 seven3 six3 = OBDD seven3 6 seven4 six4 = OBDD seven4 6 seven4 seven1 = OBDD eight1 7 eight1 seven2 = OBDD eight1 7 eight2 seven3 = OBDD eight2 7 eight3 seven4 = OBDD eight3 7 eight3 eight1 = OBDD One 8 One eight2 = OBDD One 8 Zero eight3 = OBDD Zero 8 Zero -- ith(2) mit drei Variablen, d. h. Spieler 2 ist ein Diktator. dictator :: OBDD dictator = OBDD two 1 two where two = OBDD three1 2 three2 three1 = OBDD One 3 One three2 = OBDD Zero 3 Zero -- Hier sind 3, 4, 5, 6, 7 Vetospieler und 1, 2 belanglos. vetoers :: OBDD vetoers = OBDD two 1 two where two = OBDD three 2 three three = OBDD four1 3 four2 four1 = OBDD five1 4 five2 four2 = OBDD five2 4 five2 five1 = OBDD six1 5 six2 five2 = OBDD six2 5 six2 six1 = OBDD seven1 6 seven2 six2 = OBDD seven2 6 seven2 seven1 = OBDD One 7 Zero seven2 = OBDD Zero 7 Zero -- Keine Diktatoren, aber Spieler 5 (die Grünen) ist ein belangloser Spieler. germanParliament:: OBDD germanParliament = OBDD two1 1 two2 where two1 = OBDD three1 2 three2 two2 = OBDD three3 2 three4 three1 = OBDD four1 3 four1 three2 = OBDD four1 3 four2 three3 = OBDD four2 3 four3 three4 = OBDD four3 3 four3 four1 = OBDD five1 4 five1 four2 = OBDD five1 4 five2 four3 = OBDD five2 4 five2 five1 = OBDD One 5 One five2 = OBDD Zero 5 Zero shParliament :: OBDD shParliament = OBDD two1 1 two2 where two1 = OBDD three1 2 three2 two2 = OBDD three2 2 three3 three1 = OBDD four1 3 four1 three2 = OBDD four2 3 four3 three3 = OBDD four4 3 four4 four1 = OBDD five1 4 five1 four2 = OBDD five1 4 five2 four3 = OBDD five3 4 five4 four4 = OBDD five4 4 five4 five1 = OBDD six1 5 six1 five2 = OBDD six1 5 six2 five3 = OBDD six2 5 six3 five4 = OBDD six3 5 six3 six1 = OBDD One 6 One six2 = OBDD One 6 Zero six3 = OBDD Zero 6 Zero

TestGames.hs

module TestGames where import BDDModule ---------------------------------------------------------------------------------------------------- -- BDD aus der Vorlesung, Aufbau: Bottom-Up. Diese Aufbau-Reihenfolge ist wichtig, weil es sich -- anderenfalls immer nur um vollständige Entscheidungsdiagramme handelt. bdd :: OBDD bdd = OBDD left3 1 right3 where left3 = OBDD left2 2 left2 right3 = OBDD left2 2 right2 left2 = OBDD left1 3 right1 right2 = OBDD right1 3 right1 left1 = OBDD One 4 Zero right1 = OBDD Zero 4 Zero -- BDD für x1*x2 bezüglich der Variablenordnung (1, 2). bddAnd :: OBDD bddAnd = OBDD left 1 Zero where left = OBDD One 2 Zero -- BDD für x1+x2 bezüglich der Variablenordnung (1, 2). bddOr :: OBDD bddOr = OBDD One 1 (OBDD One 2 Zero) -- ROBDD für x1x2 + x3x4 +x5x6 bzgl. der Ordnung (1, 3, 5, 2, 4, 6). largeBDD :: OBDD largeBDD = OBDD three1 1 three2 where three1 = OBDD five1 3 five2 three2 = OBDD five3 3 five4 five1 = OBDD two1 5 two2 five2 = OBDD two3 5 two4 five3 = OBDD four1 5 four2 five4 = OBDD six 5 Zero two1 = OBDD One 2 four1 two2 = OBDD One 2 four2 two3 = OBDD One 2 six two4 = OBDD One 2 Zero four1 = OBDD One 4 six four2 = OBDD One 4 Zero six = OBDD One 6 Zero -- ROBDD für x1x2 + x3x4 +x5x6 bzgl. der Ordnung (1, 2, 3, 4, 5, 6). smallBDD :: OBDD smallBDD = OBDD two 1 three where two = OBDD One 2 three three = OBDD four 3 five four = OBDD One 4 five five = OBDD six 5 Zero six = OBDD One 6 Zero ---------------------------------------------------------------------------------------------------- danishParliamentWeirdRules :: OBDD danishParliamentWeirdRules = OBDD two1 1 two2 where two1 = OBDD three1 2 three2 two2 = OBDD three2 2 three2 three1 = OBDD four1 3 four2 three2 = OBDD four3 3 four3 four1 = OBDD five1 4 five2 four2 = OBDD five2 4 five3 four3 = OBDD five4 4 five4 five1 = OBDD six1 5 six2 five2 = OBDD six2 5 six3 five3 = OBDD six3 5 six4 five4 = OBDD six4 5 six4 six1 = OBDD seven1 6 seven2 six2 = OBDD seven2 6 seven3 six3 = OBDD seven3 6 seven4 six4 = OBDD seven4 6 seven4 seven1 = OBDD eight1 7 eight1 seven2 = OBDD eight1 7 eight2 seven3 = OBDD eight2 7 eight3 seven4 = OBDD eight3 7 eight3 eight1 = OBDD One 8 One eight2 = OBDD One 8 Zero eight3 = OBDD Zero 8 Zero -- ith(2) mit drei Variablen, d. h. Spieler 2 ist ein Diktator. dictator :: OBDD dictator = OBDD two 1 two where two = OBDD three1 2 three2 three1 = OBDD One 3 One three2 = OBDD Zero 3 Zero -- Hier sind 3, 4, 5, 6, 7 Vetospieler und 1, 2 belanglos. vetoers :: OBDD vetoers = OBDD two 1 two where two = OBDD three 2 three three = OBDD four1 3 four2 four1 = OBDD five1 4 five2 four2 = OBDD five2 4 five2 five1 = OBDD six1 5 six2 five2 = OBDD six2 5 six2 six1 = OBDD seven1 6 seven2 six2 = OBDD seven2 6 seven2 seven1 = OBDD One 7 Zero seven2 = OBDD Zero 7 Zero -- Keine Diktatoren, aber Spieler 5 (die Grünen) ist ein belangloser Spieler. germanParliament:: OBDD germanParliament = OBDD two1 1 two2 where two1 = OBDD three1 2 three2 two2 = OBDD three3 2 three4 three1 = OBDD four1 3 four1 three2 = OBDD four1 3 four2 three3 = OBDD four2 3 four3 three4 = OBDD four3 3 four3 four1 = OBDD five1 4 five1 four2 = OBDD five1 4 five2 four3 = OBDD five2 4 five2 five1 = OBDD One 5 One five2 = OBDD Zero 5 Zero