"Binary Decision Diagram (BDD) merupakan representasi dari fungsi Boolean
secara simbolik yang dikembangkan dan dipopulerkan oleh Randal E. Bryant.
Selain mengembangkan BDD, Bryant juga memberikan algoritma untuk
melakukan manipulasi pada BDD. Dengan menerapkan suatu kondisi tertentu
terhadap BDD, yaitu dengan menentukan urutan variabel, akan didapat BDD yang
terurut atau disebut juga Ordered Binary Decision Diagram (OBDD). Lalu
dengan menyederhanakan OBDD maka akan didapatkan Reduced Binary
Decision Diagram (ROBDD). ROBDD akan memberikan representasi yang unik
untuk suatu fungsi Boolean. Jadi, jika terdapat dua ROBDD yang
merepresentasikan suatu fungsi Boolean f, maka kedua ROBDD tersebut adalah
sama. Operasi pada fungsi Boolean dapat dilakukan dengan menggunakan operasi
pada ROBDD. Operasi – operasi yang ada pada ROBDD antara lain operasi
Apply, operasi Restrict, operasi SatCount, operasi AnySat, dan operasi AllSat."
