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