Binarni dijagrami odluke

U polju računarskih nauka, binarni diagram odluke(BDD) ili program grananja , predstavlja Strukturu podataka koje predstavljaju Bulova funkcija kao sto su negacija normalne forme ili kao iskani usmereni aciklicni graf, PDAG . Takođe na višem apstraktnom nivo, BDD može da se razmatrati kao komprimovano predstaljanja skupova и relacija. Za razliku od ostalih kompresovanih predstaljanja, operacije se direktno primenjuju na kompresovnu reprezentaciu bez potrebe za dekompresovanje.

Definicija

Bulova funkcija se može prestaviti kao korenski,usmereni,acikličan graf, koji sadrđž nekoliko odlučujućih(roditeljski) i krajnjih(sinovi) cvorova. Postoje dve vrste krajnjih čvorova koji imaju vrednost ili 0 ili 1.Svakom cvoru $N$ se dodeljuje jedna Bulovska promenljiva $V_{N}$ koja ima dva sina i koji se nazivaju niži(low) i viši(high). Od krajnjeg čvora $V_{N}$ do nižeg(višeg) sina predstalja vrednost od $V_{N}$ do 0(1). BDD se takođe može nazvati i uređen ukoliko se različite promenljive pojavljuju u svakoj putanji od korena u istom poretku. BDD može da bude uprošćen ukoliko se primene dva tekuca pravila na graf:

• Spojiti izomorfne podgrafove;
• Izbrisati čvorove čija su deca izomorfna.

U svkodnevnoj upotrebi, termin BDD skoro uvek se odnosi na Reduced Ordered Binary Decision Diagram (ROBDD u literaturi, koriste se kada se aspekti uređivanja i uprosćavanja trebaju da budu naglašeni). Prednosti ROBDD kanonski(jedinstven) redosled za posebne funkcije i promenljive. Ovo svojstvo čini korisnim u funkcionalnom proveravanju ekvivalencije i drugih operacija kao što su funkcionalne tehnologije mapiranja.

Putanja od korena do krajnjeg cvora sa vrednosti 1 predstavlja (moguće delimičnu) vrednosti promenljive za koju je Bulova funkcija tacna. Kako se spustamo do nižeg( ili višeg) sina iz čvora tada vrednost promenljive tog čvora je 0(ili 1).

Primer

Leva slika predstavlja binarno stablo odluke( bez primena pravilaza uprosćavanje), i tablica istinitosti, oba predstavljaju funkciju f(x1, x2, x3). U stablu, sa leve trane, vrednosti funkcije može biti određen za date vrednoti promenljivih prateci putanju od korena ka krajnjim čvorovima. U figuri ispod, isprekidane linije predstavljaju putanju ka nižim sinovima, dok neisprekidane predstaljaju putalje ka višim sinovima. Dakle, da bi našli vrednot funkcije za vrednosti x1=0, x2=1, x3=1, krećemo iz prvog čvora(korena) x1, prelazimo isprekidanom linijom do čvora x2 (pošto x1 ima vrednost 0), nakon toga prelazimo neisprekidanom linijemo dva puta (pošsto vrednosti preomenljivih x2 i x3 su jednaki 1) što vodi do krajnjeg čvora sa vrednosti jedan to je vrednost funkcije f(x1, x2, x3).

Binarno "stablo" odluke sa leve strane može biti transformisan u binarni diagram odluke maksimalnim uprošćavanjem prema dva pravila za uprošćavanje. Rezultat je BDD prikazan na desnoj slici.

Binarno stablo odluke i tabela istinitosti za funkciju $f(x_{1},x_{2},x_{3})={\bar {x_{1}}}{\bar {x_{2}}}{\bar {x_{3}}}+x_{1}x_{2}+x_{2}x_{3}$

BDD za funkciju f

Istorija

Osnovna ideja ove strukture podataka potiče od "Shannon expansion". Prebacivanje funkcija je podeljena u dve podfunkcije(kofaktora) dodeljujući jednu primenljivu(if-then-else normalna forma). Ukoliko se takva podfunkcija može posmatrati kao podstablo onda se može predstaviti kao binarno stablo odluke. Binarni diagram odluke (BDD) je uveo C. Y. Lee, i daljim istraživanjem Sheldon B. Akers i Raymond T. Boute. Dok potpuni potencijal za efikasne alogaritme bazirane na ovoj strukturi podataka je istraživao "Randal Bryant" na "Carnegie Mellon University": on je koristio fiksiran redosled promenljivih( za kanoničku prezentaciju) i deljeni podgrafovi (za kompresiju). Primenjujuci ova dva koncepta dovodi do efikasne strukture podataka i alogaritama za predstavljanje skupova i relacija. Proširujući na nekoliko dijagrama, tj. jedan podgraf korišćen za nekoliko dijagrama, definisana je struktura podataka Shared Reduced Ordered Binary Decision Diagram. Pojam BDD se sada uglavnom koristi da označi tu strukturu podataka. U ovoj video lekciji Fun With Binary Decision Diagrams (BDDs),"Donald Knuth" naziva ovu strukturu kao jednu od boljih fundamentalninih struktura koja je definisana u poslednjih dvadesetpet godina i pomenuo da je Bryant-ov clanak iz 1986. godine je jedno vreme bio najznačajnijh citiranih radova u računarstvu.

Aplikacije

BDD se intezivno koristi u CAD softveru za sitezu kola (logička sinteza) i na formalnu verifikaciju. Postoje nekoliko manje poznatih primena BDD, uključujuci Fault tree analize, Bayesian obrazlženju, konfiguracije proizvoda, i privatno pretraživanje informacija . Svak proizvoljan BDD (čak i ako nije uprošćen ili uređen) mogu se direktno implementirati zamenom svakog čvora sa 2-1 multiplekser. Svaki multiplekser može da se direktno implementira pomocu 4-LUT u FPGA. To nije tako jednostavno da se konvertuje iz proizvoljne logičke mreže u BDD(za razliku od and-inverter graph).

Uređivanje promenljivih

Velicina BDD je odredjena i funkcijom kojom je reprezentovana i izabranog uređivanja promenljivih. Postoje Bulove funkcije $f(x_{1},\ldots ,x_{n})$ za koje u odnosu na izbor uređivanja promenljivih zavisi broj čvorova da li će biti linearna (in n) u najboljem slučaju ili eksponencijalna u najgorem slučaju. Primetimo Bulovu funkciju $f(x_{1},\ldots ,x_{2n})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{2n-1}x_{2n}.$ Koristeći uređenje $x_{1}<x_{3}<\cdots <x_{2n-1}<x_{2}<x_{4}<\cdots <x_{2n}$, za BDD je potrebno 2ⁿ⁺¹ čvorova za predstavljanje funkcije. Koristeči uređenje $x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{2n-1}<x_{2n}$, potrebno je 2n+2 čvorova.

BDD za funkciju ƒ(x1, ..., x8) = x1x2 + x3x4 + x5x6 + x7x8 koristeći loše uređenje promenljivih

Koristeći dobro urešenje promenljivih

To je od kljčnog značaja da se izabere najbolji način za uređenje promenljivih za primenu ove strukture podataka u praksi. Problem pronalaženja najbljeg načina za uređenje pripada klasi "NP-teških" problema. Redosled promenljivih dovodi do OBDD koja je c puta veca od optimalne. Međutim postoje efikasne heuristike da se pozabave problemom. Postoje funkcije kojima je graf velicine uvek eksponencijalne - nezavisno od uređenja promenljivih. Ovo važi za npr. funkciju množenja.

Logičke operacije

Mnoge logičke operacije na BDD mogu se implementirati u polinomijalnom vremenu.

• Konjukcija
• Disjukcija
• Negacija
• Egzistencijalna apstrakcija
• Univerzalna apstrakcija

Međutim ponavljanjem ovih operacija više puta npr. formiranje konjukciju ili disjukciju od skupa diagrama, u najgorem slucaju se može rezultirati eksponencijalno veliki BDD. To je zato što svaka od predhodnih operacija za dva BDD može da dovede u BDD sa veličinom srazmerno proizvodu ta dva diagrama, samim tim i do eksponencijalne veličine.

Vidi još

• Bulova zadovljivost problema
• L/poli, tj. Složenost klasa koja obuhvata kompleksne probleme u polinomijalnoj veličini BDD
• Model checking
• Radiks stablo
• Binary key – metod indetifikacije vrsta u biologiji pomoću binarnih stabla
• Barrington's teorema

Reference

• R. Ubar, "Test Generation for Digital Circuits Using Alternative Graphs (in Russian)", in Proc. Tallinn Technical University, 1976, No.409, Tallinn Technical University, Tallinn, Estonia, pp. 75–81.

Dodatna literatura

• D. E. Knuth, "The Art of Computer Programming Volume 4, Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams" (Addison–Wesley Professional, March 27, 2009) viii+260pp, ISBN 0-321-58050-8. Draft of Fascicle 1b available for download.
• H. R. Andersen "An Introduction to Binary Decision Diagrams," Lecture Notes, 1999, IT University of Copenhagen.
• Ch. Meinel, T. Theobald, "Algorithms and Data Structures in VLSI-Design: OBDD – Foundations and Applications", Springer-Verlag, Berlin, Heidelberg, New York, 1998. Complete textbook available for download.
• Rüdiger Ebendt; Görschwin Fey; Rolf Drechsler (2005). Advanced BDD optimization. Springer. ISBN 978-0-387-25453-1. 
• Bernd Becker; Rolf Drechsler (1998). Binary Decision Diagrams: Theory and Implementation. Springer. ISBN 978-1-4419-5047-5. 

Spoljašnji linkovi

Dosupni BDD paketi

• ABCD: ABCD paketi Armin Biere, Johannes Kepler Universität, Linz.
• CMU BDD, BDD paket, Carnegie Mellon University, Pittsburgh
• BuDDy: A BDD paket by Jørn Lind-Nielsen
• Biddy:Akademska multiplatforma BDD paketa, University of Maribor
• CUDD: BDD paket, University of Colorado, Boulder
• JavaBDD: Java biblioteka za manipulaciju BDD
• JDD java implementcaija BDD i ZBDD.
• JBDD od istog autora koji ima slican API, ali je Java interfejs od BuDDy i CUDD
• The Berkeley CAL paketi za manipulacijom u sirinu
• DDD: C++ biblioteka koja dodatno sadrzi celobrojnu vrednot i hijerarhijske dijagrame odluke
• JINC: C++ biblioteka razvijena na University of Bonn, Germany, podrzava nekoliko BDD varijanti i visenitnio
• Fun With Binary Decision Diagrams (BDDs), lecture by Donald Knuth