Binarni dijagrami odluke

Из Википедије, слободне енциклопедије
Jump to navigation Jump to search

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 se dodeljuje jedna Bulovska promenljiva koja ima dva sina i koji se nazivaju niži(low) i viši(high). Od krajnjeg čvora do nižeg(višeg) sina predstalja vrednost od 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
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 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 Koristeći uređenje , za BDD je potrebno 2n+1 čvorova za predstavljanje funkcije. Koristeći uređenje , 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. ^ Stanford Center for Professional Development
  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” (PDF). 

Литература[уреди]

  • 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