Binair beslissingsdiagram

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken
Een 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]

Definitie[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, de ene 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). Respectievelijk worden deze aangeduid met een stippellijn en een normale lijn.

Een BDD is geordend als de parameters in dezelfde volgorde langskomen in alle paden vanaf de wortel. Formeel houdt dit 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 isomorfe kinderen is verwijderd. Concreet betekent dit dat redundante knopen worden weggehaald (een knoop waarbij beide alternatieven naar hetzelfde kind gaan) en knopen dienen uniek te zijn (er zijn niet twee knopen voor dezelfde parameter).

Met de term 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]

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 analoge wijze geeft een pad naar een 0-blad een manier waarvoor de functie 0 oplevert. De waarden voor de parameters wordt 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 1 ROBDD bestaat voor een Booleaanse functie (of logische propositie), is het zo dat er zowel voor een tautologie als een contradictie exact 1 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 in tegenstelling tot het algemene vervulbaarheidsprobleem voor logische formules dat NP-volledig is. De grootte van een ROBDD kan in het slechtste geval echter exponentieel groter zijn dan een equivalente logische formule.

Voorbeeld[bewerken]

Het voorbeeld hieronder geeft de beslissingsboom, de waarheidstabel en het binaire beslissingsdiagram voor de functie f(x1, x2, x3) = -x1 * -x2 * -x3 + x1 * x2 + x2 * x3, waarbij x1, x2 en x3 de waarden 0 of 1 kunnen aannemen. Wanneer de functie 1 oplevert is te zien in de onderstaande waarheidstabel. 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). In de waarheidstabel zijn dit exact 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 gerepresenteerd worden als een beslissingsboom waarbij men bij elke knoop moet aangeven wat de waarde is voor die parameter. Als de waarde 0 is dan gaat men naar het ene kind (de stippellijn) en als de waarde 1 is dan gaat men naar het andere kind (de normale lijn). Op deze manier kan de beslissingsboom worden doorlopen om bij een blad te eindigen. De waarde in het blad is de uitvoer van de booleaanse functie.

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

Beslissingsboom en waarheidstabel voor de functie f.
Binair beslissingsdiagram voor de functie f.

Externe links[bewerken]