Binair beslissingsdiagram

In de informatica is een binair beslissingsdiagram (Engels: binary decision diagram, BDD) een datastructuur waarmee een booleaanse functie gerepresenteerd kan worden.

Kenmerken[bewerken | brontekst bewerken]

Definitie[bewerken | brontekst bewerken]

Een BDD is een gerichte acyclische graaf die de in- en uitvoer van een booleaanse functie bevat. Een BDD heeft een wortel met daaronder allerlei kinderen die de parameters, afhankelijk van de context ook variabelen genoemd, van de functie representeren en onderaan bevinden zich twee bladeren met 0 en 1. Deze twee bladeren bevatten de uitvoer van de functie. Elke knoop voor een parameter heeft twee kinderen, een voor als de parameter de waarde 0 heeft, het low child, en de andere voor als de parameter de waarde 1 heeft, het high child. Deze twee mogelijke verbindingen worden met een stippellijn voor een 0 en een normale lijn voor een 1 aangeduid.

Een BDD is geordend als de parameters in dezelfde volgorde langskomen in alle paden vanaf de wortel. Dit houdt in dat er een ordening op de parameters bestaat, bijvoorbeeld $x_{1}<\ldots <x_{n}$ . Een BDD is gereduceerd als alle isomorfe subgrafen zijn samengevoegd en elke knoop met twee isomorfe kinderen is verwijderd. Met BDD wordt vaak een gereduceerd geordend binair beslissingsdiagram bedoeld, een reduced ordered binary decision diagram (ROBDD). Een geordend binair beslissingsdiagram heet een ordered binary decision diagram (OBDD).

Voor een vaststaande parameterordening bestaat er voor elke booleaanse functie exact één ROBDD die de functie representeert.

Vervulbaarheid[bewerken | brontekst bewerken]

Een pad vanaf de wortel naar een 1-blad geeft een (mogelijk partiële) toekenning van 0 of 1 aan de parameters van de functie zodanig dat de functie 1 oplevert. Op dezelfde manier geeft een pad naar een 0-blad een manier waarvoor de functie 0 oplevert. De waarden voor de parameters worden verkregen door bij te houden naar welk kind men gaat: het kind dat hoort bij het toekennen van de waarde 0 (1) betekent een 0 (1). Een binair beslissingsdiagram kan dus ook worden gebruikt om de vervulbaarheid van een logische formule te bepalen: een logische formule is vervulbaar als het bijbehorende binaire beslissingsdiagram een pad vanaf de wortel naar het 1-blad heeft.

Aangezien er exact één ROBDD voor een booleaanse functie (logische propositie) bestaat, is het zo dat er zowel voor een tautologie als een contradictie exact één representatie bestaat, namelijk de constanten 1 en 0. Het is dus mogelijk om in constante tijd te controleren of de formule van een ROBDD een tautologie of een contradictie is. Dit is anders dan bij het algemene vervulbaarheidsprobleem voor logische formules, dat NP-volledig is. Een ROBDD kan in het uiterste geval exponentieel groter zijn dan een equivalente logische formule.

Voorbeeld[bewerken | brontekst bewerken]

Het voorbeeld hieronder geeft de beslissingsboom, de waarheidstabel en het binaire beslissingsdiagram voor de functie $f(x_{1},x_{2},x_{3})=-x_{1}*-x_{2}*-x_{3}+x_{1}*x_{2}+x_{2}*x_{3}$ , waarbij $x1,x2$ en $x3$ de waarden 0 of 1 kunnen aannemen. Er is daarin te zien wanneer de functie 0 en wanneer 1 oplevert. De functie is ook te lezen als de logische propositie $(\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})$ . Dit zijn de situaties waarvoor de functie de waarde 1 oplevert. Als $x1$ en $x2$ waar zijn of $x2$ en $x3$ dan is de derde variabele niet meer van invloed.

Deze functie kan als een beslissingsboom worden gerepresenteerd, waarbij men bij elke knoop moet aangeven wat de waarde is voor die parameter. Als de waarde 0 is gaat men over de stippellijn naar het ene kind en als de waarde 1 is gaat men over de normale lijn naar het andere kind. Op deze manier kan de beslissingsboom worden doorlopen om bij een blad te eindigen.

Het binaire beslissingsdiagram gebruikt ditzelfde principe: de knopen vertegenwoordigen de parameters en de bladeren geven de uitvoer van de functie.