Binair beslissingsdiagram

Binair beslissingsdiagram

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

Kenmerken

Definitie

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 ${\displaystyle 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

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

Het voorbeeld hieronder geeft de beslissingsboom, de waarheidstabel en het binaire beslissingsdiagram voor de functie ${\displaystyle f(x_{1},x_{2},x_{3})=-x_{1}*-x_{2}*-x_{3}+x_{1}*x_{2}+x_{2}*x_{3}}$, waarbij ${\displaystyle x1,x2}$ en ${\displaystyle 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 ${\displaystyle (\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 ${\displaystyle x1}$ en ${\displaystyle x2}$ waar zijn of ${\displaystyle x2}$ en ${\displaystyle 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.

Beslissingsboom en waarheidstabel voor de functie ${\displaystyle f}$

Binair beslissingsdiagram voor de functie ${\displaystyle f}$

Websites

• (en) HR Andersen. An Introduction to Binary Decision Diagrams, oktober 1997.

Mediabestanden

Zie de categorie Binary decision diagrams van Wikimedia Commons voor mediabestanden over dit onderwerp.