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:

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 .[1] 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,[2] i daljim istraživanjem Sheldon B. Akers[3] i Raymond T. Boute[4]. 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.[5] [6] Proširujući na nekoliko dijagrama, tj. jedan podgraf korišćen za nekoliko dijagrama, definisana je struktura podataka Shared Reduced Ordered Binary Decision Diagram.[7] Pojam BDD se sada uglavnom koristi da označi tu strukturu podataka. U ovoj video lekciji Fun With Binary Decision Diagrams (BDDs),[8]"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[9] [10]. 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_1x_2 + x_3x_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 2n+1 č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.[11] Međutim postoje efikasne heuristike koje se bave ovim problemom.[12] 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.

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

Reference[уреди]

  1. Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986
  2. C. Y. Lee. "Representation of Switching Circuits by Binary-Decision Programs". Bell Systems Technical Journal, 38:985–999, 1959.
  3. Sheldon B. Akers. Binary Decision Diagrams, IEEE Transactions on Computers, C-27(6):509–516, June 1978.
  4. Raymond T. Boute, "The Binary Decision Machine as a programmable controller". EUROMICRO Newsletter, Vol. 1(2):16–22, January 1976.
  5. Randal E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation". IEEE Transactions on Computers, C-35(8):677–691, 1986.
  6. R. E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.
  7. Karl S. Brace, Richard L. Rudell and Randal E. Bryant. "Efficient Implementation of a BDD Package". In Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990), pages 40–45. IEEE Computer Society Press, 1990.
  8. http://scpd.stanford.edu/knuth/index.jsp
  9. R.M. Jensen. "CLab: A C+ + library for fast backtrack-free interactive product configuration". Proceedings of the Tenth International Conference on Principles and Practice of Constraint Programming, 2004.
  10. H.L. Lipmaa. "First CPIR Protocol with Data-Dependent Computation". ICISC 2009.
  11. Detlef Sieling. "The nonapproximability of OBDD minimization." Information and Computation 172, 103–138. 2002.
  12. Rice, Michael. „A Survey of Static Variable Ordering Heuristics for E?cient BDD/MDD Construction”. 
  • 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[уреди]

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