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 negacijska normalna forma ili kao iskazni usmereni aciklični graf, PDAG . Takođe na višem apstraktnom nivo, BDD se može razmatrati kao kompresovano predstavljanje skupova i relacija. Za razliku od ostalih kompresovanih predstavljanja, operacije se direktno primenjuju na kompresovnu reprezentaciju bez potrebe za dekompresovanje.

Definicija

Bulove funkcije se mogu predstaviti kao korenski, usmereni, acikličani grafovi, koji sadrže odlučujuće i krajnje (čvorovi koji nemaju sinova) čvorove. Postoje dve vrste krajnjih čvorova koji imaju vrednost ili 0 ili 1. Svakom čvoru $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 tekuća 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 bi aspekti uređivanja i uprosćavanja trebalo da budu naglašeni). Prednost ROBDD dijagrama je da može biti kanonski (jedinstven) predstavnik za određene funkcije i promenljivog redosleda . Ovo svojstvo je korisno u funkcionalnom proveravanju ekvivalencije i drugih operacija kao što su funkcionalne tehnologije mapiranja.

Putanja od korena do krajnjeg čvora sa vrednošću 1 predstavlja (moguće delimičnu) vrednosti promenljive za koju je Bulova funkcija tačna. Kako se spuštamo 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 pravila za uprošćavanje), i tablica istinitosti, oba predstavljaju funkciju f(x1, x2, x3). U stablu, sa leve strane, vrednost funkcije može biti određen za date vrednosti promenljivih prateći putanju od korena ka krajnjim čvorovima. U figuri ispod, isprekidane linije predstavljaju putanju ka nižim sinovima, dok neisprekidane predstaljaju putanje ka višim sinovima. Dakle, da bi našli vrednost 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što vrednosti promenljivih x2 i x3 su jednaki 1) što vodi do krajnjeg čvora sa vrednošću jedan, što predstavlja 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 promenljivu(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 kanonsku reprezentaciju) i deljene podgrafove (za kompresiju). Primena 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 jedno vreme bio jedan od 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 . Svaki 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

Veličina BDD je određena i funkcijom kojom je reprezentovana i izabranog uređivanja promenljivih. Postoje Bulove funkcije $f(x_{1},\ldots ,x_{n})$ za koje od izbora uređivanja promenljivih zavisi da li će broj čvorova biti linearan (in n) u najboljem slučaju ili eksponencijalan 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

U praksi, za primenu ove strukture podataka, je od kljčnog značaja da se izabere najbolji način za uređenje promenljivih. Problem pronalaženja najboljeg 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 koje se bave ovim problemom. Postoje funkcije kojima je graf uvek eksponencijalne veličine - 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 slučaju se može rezultirati eksponencijalno veliki BDD. To je zato što svaka od prethodnih 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

Литература

• 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. Knuth, Donald Ervin (1997). The Art of Computer Programming: Fasc. 0. Introduction to combinatorial algorithms and boolean functions. Addison-Wesley. ISBN 978-0-321-58050-4. Архивирано из оригинала 12. 03. 2016. г. Приступљено 18. 04. 2014. 
• 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.
• Ebendt, Rüdiger; Fey, Görschwin; Drechsler, Rolf (2005). Advanced BDD optimization. Springer. ISBN 978-0-387-25453-1. 
• Becker, Bernd; Drechsler, Rolf (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