Binary Decision Diagram (BDD) merupakan representasi dari fungsi Booleansecara simbolik yang dikembangkan dan dipopulerkan oleh Randal E. Bryant.Selain mengembangkan BDD, Bryant juga memberikan algoritma untukmelakukan manipulasi pada BDD. Dengan menerapkan suatu kondisi tertentuterhadap BDD, yaitu dengan menentukan urutan variabel, akan didapat BDD yangterurut atau disebut juga Ordered Binary Decision Diagram (OBDD). Laludengan menyederhanakan OBDD maka akan didapatkan Reduced BinaryDecision Diagram (ROBDD). ROBDD akan memberikan representasi yang unikuntuk suatu fungsi Boolean. Jadi, jika terdapat dua ROBDD yangmerepresentasikan suatu fungsi Boolean f, maka kedua ROBDD tersebut adalahsama. Operasi pada fungsi Boolean dapat dilakukan dengan menggunakan operasipada ROBDD. Operasi – operasi yang ada pada ROBDD antara lain operasiApply, operasi Restrict, operasi SatCount, operasi AnySat, dan operasi AllSat.