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 . 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 , waarbij  en  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 . Dit zijn de situaties waarvoor de functie de waarde 1 oplevert. Als  en  waar zijn of  en  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.

Websites 
  HR Andersen. An Introduction to Binary Decision Diagrams, oktober 1997.

Datastructuur
Diagram
Logica