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 predstavljanje skupova и relacija. Za razliku od ostalih kompresovanih predstavljanje, 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 krajnji (cvorovi koji nemaju sinova) 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:

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). Prednost ROBD dijagrama je da može biti kanonski (jedinstven) predstavnik za određene funkcije i promenljivog redosleda .[1] Ovo svojstvo čini korisnim u funkcionalnom proveravanju ekvivalencije i drugih operacija kao što su funkcionalne tehnologije mapiranja.

Putanja od korena do krajnjeg čvora 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,[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 kanoničku prezentaciju) i deljeni podgrafovi (za kompresiju). Primenjujuci 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 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[9] [10]. 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_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

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.[11] Međutim postoje efikasne heuristike da se pozabave problemom.[12] 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.

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 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[уреди]

  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