Bináris döntési diagram

A bináris döntési diagram ( BDE ) vagy egy elágazó program a változók Boole-függvényének egy irányított aciklikus gráfként való megjelenítésének egyik formája , amely belső döntési csomópontokból (címkével ) áll, amelyek mindegyikének két gyermeke és két terminális csomópontja van (0-val jelölve ). és 1) , amelyek mindegyike megfelel a Boole-függvény két értékének valamelyikének. A külföldi szakirodalomban a bináris döntési diagramokat és az elágazó programokat bináris döntési diagramnak ( BDD ), illetve elágazó programnak ( BP ) nevezik.

Definíció

A Boole-függvény egy irányított aciklikus gráfként ábrázolható , amely több belső döntési csomópontból és két terminális csomópontból áll, amelyeket 0-terminális csomópontnak és 1-terminális csomópontnak neveznek. Egy szinten minden belső döntési csomópont egy logikai változóval van címkézve, és két gyermeke van , ezek az úgynevezett junior gyermek és idősebb gyermek. A belső csomópontról egy fiatalabb vagy idősebb gyermekre való áttérés a változó értékétől (0 vagy 1) függően történik . A megadott értékeknél a gyökércsomóponttól az 1-terminális csomópontig vezető út megfelel annak, hogy ezeken a bemeneti értékeken a Boole-függvény az 1 értéket veszi fel.

A BDR -ről azt mondjuk , hogy rendezett , ha a különböző változók ugyanabban a sorrendben jelennek meg a gráf gyökércsomópontjától a terminális csúcsok egyikéig tartó összes útvonalon . Ugyanakkor előfordulhat, hogy az útvonalak egyes változói hiányoznak, ha a redukciós műveletet korábban elvégezték a grafikonon.

A BDR -t rövidítettnek nevezzük, ha a következő két rövidítési szabályt alkalmazzuk a grafikonra:

• Tetszőleges izomorf részgráfok összevonása .
• Az összes izomorf gyermek csomópont eltávolítása .

A legtöbb esetben a bináris döntési diagramon egy redukált rendezett bináris döntési diagramot ( SUBDR ) kell érteni . A redukált rendezett BDD előnye, hogy kanonikus (egyedi) egy adott függvényhez és a változók adott sorrendjéhez. [1] Ez a tulajdonság a RUBMS-t hasznossá teszi a funkcionális egyenértékűség tesztelésére.

Példa

A bal oldali ábra egy bináris döntési fát mutat (a redukciós szabályok alkalmazása nélkül), amely megfelel az ugyanazon az ábrán látható Boole-függvény igazságtáblázatának . Adott bemeneti értékeknél a Boole - függvény értékét úgy határozhatja meg , hogy a fa gyökércsomópontjától a végcsomópontokig halad a fa mentén, a bemeneti értéktől függően kiválasztva a csomóponttól való átmenet irányát . Az ábrán látható szaggatott vonalak egy fiatalabb gyermekhez, a folyamatos vonalak pedig egy idősebb gyermekhez való átmenetet jelölnek. Például, ha a bemeneti értékek ( , , ) adottak, akkor a gyökércsomóponttól a szaggatott vonalon kell menni balra (mivel az érték 0), ezután a folytonos vonalakon kell haladni. jobbra (mivel az és az értékek egyenlőek 1-gyel). Ennek eredményeként egy 1-terminális csomópontba kerülünk, azaz az érték 1.

A bal oldali ábrán látható bináris döntési fa két redukciós szabály alkalmazásával bináris döntési diagrammá alakítható . Az eredményül kapott BDR a jobb oldali ábrán látható.

Történelem

Az ilyen adatstruktúra létrehozásának fő ötlete a Shannon-dekompozíció volt . Bármely Boole-függvény az egyik bemeneti változón két alfüggvényre osztható, ezeket pozitív és negatív komplementernek nevezzük, amelyek közül csak egy alfüggvény kerül kiválasztásra az if-then-else elv szerint, a bemeneti változó értékétől függően (amelyen végrehajtották a Shannon-kiterjesztést). Minden egyes ilyen alfüggvényt részfaként ábrázolva, és folytatva a bővítést a többi bemeneti változóban, egy döntési fa állítható elő , melynek redukálásával bináris döntési diagramot kapunk . A bináris döntési diagramok vagy bináris elágazó programok használatára vonatkozó információk először 1959-ben jelentek meg a Bell Systems Technical Journal [2] [3] [4] című folyóiratban . A kanonikus zárójeles formának nevezett BDD-t Mamrukov [5] valósította meg CAD-ben sebességfüggetlen áramkörök elemzésére. Az ezen az adatstruktúrán alapuló hatékony algoritmusok létrehozásának lehetőségét Randal Bryant , a Carnegie Mellon Egyetem kutatója tárta fel : az ő megközelítése a változók rögzített sorrendjének alkalmazása volt (az egyes Boole-függvények egyedi kanonikus ábrázolásához), valamint a közös részgráfok újrafelhasználása (a tömörség érdekében). ). E két kulcsfogalom alkalmazása lehetővé teszi a halmazok és a köztük lévő kapcsolatok ábrázolására szolgáló adatstruktúrák és algoritmusok hatékonyságának növelését. [6] [7] A közös részgráfok több BDR általi használata a Shared Reduced Ordered Binary Decision Diagram adatstruktúra megjelenéséhez vezetett . [8] A BDR nevet manapság elsősorban erre a sajátos adatszerkezetre használják.

Donald Knuth a Fun With Binary Decision Diagrams (BDDs) című videoelőadásában a bináris döntési diagramokat " az egyik igazán alapvető adatszerkezetnek nevezte, amely az elmúlt huszonöt évben alakult ki ", és megjegyezte, hogy Randal Bryant 1986 -os publikációja [6 ] , amely a bináris döntési diagramok használatát emelte ki a Boole-függvények manipulálására, egy ideig a legtöbbet idézett számítástechnikai publikáció volt.

Alkalmazás

A BDR-eket széles körben használják számítógépes tervezési (CAD) rendszerekben logikai áramkörök szintézisére és formális ellenőrzésére .

Az elektronikában minden egyes meghatározott BDR (még nem is csökkentett és nem megrendelt) közvetlenül megvalósítható úgy, hogy minden csomópontot egy multiplexerre cserélünk , két bemenettel és egy kimenettel.

Változók sorrendje

A BDR méretét egy logikai függvény és a bemeneti változók sorrendjének megválasztása egyaránt meghatározza. Boole-függvény gráfjának összeállításakor a csomópontok száma a legjobb esetben lineárisan függhet -tól , a legrosszabb esetben pedig a függőség exponenciális lehet a bemeneti változók sorrendjének sikertelen megválasztása esetén. Például egy logikai függvény esetén Ha változók sorrendjét használjuk , akkor 2 n +1 csomópontra van szükség a függvény BDD formájában történő megjelenítéséhez. A bal oldali ábrán egy szemléltető BDD látható egy 8 változós függvényhez. És ha a sorrendet használja , akkor 2 n +2 csomópontból egyenértékű BDR-t kaphat . A jobb oldali ábrán egy szemléltető BDD látható 8 változós függvényhez.

A változó sorrend megválasztása kritikus az ilyen adatstruktúrák gyakorlati alkalmazásakor. A változók legjobb sorrendjének megtalálásának problémája NP-teljes probléma. [9] Sőt, még a változók szuboptimális sorrendjének megtalálásának problémája is NP-teljes , így bármely c > 1 konstans esetén a BDD mérete legfeljebb c-szer nagyobb, mint az optimális. [10] Ennek a problémának a megoldására azonban léteznek hatékony heurisztikák.

Ezen kívül vannak olyan függvények, amelyeknél a grafikon mérete mindig exponenciálisan növekszik a változók számának növekedésével, függetlenül a változók sorrendjétől. Ez a szorzófüggvényekre vonatkozik, jelezve a faktorizáció puszta összetettségét .

A bináris döntési diagramokkal kapcsolatos kutatások számos kapcsolódó grafikon megjelenését eredményezték, mint például a BMD ( bináris pillanatdiagramok ), a ZDD ( zéró elnyomott döntési diagramok ), az FDD ( szabad bináris döntési diagramok ), a PDD ( paritási döntési diagramok ) és MTBDD-k (több terminálos BDD-k).

Logikai műveletek bináris döntési diagramokon

Számos logikai művelet ( konjunkció , diszjunkció , negáció ) végrehajtható közvetlenül a BDR-en olyan algoritmusok segítségével, amelyek polinomiális időben hajtanak végre gráfmanipulációkat. Azonban ezeknek a műveleteknek a többszöri megismétlése, például egy BDD halmaz konjunkcióinak vagy diszjunkcióinak képzésekor, a legrosszabb esetben exponenciálisan nagy BDD-hez vezethet. Ennek az az oka, hogy a két BDR-en végzett korábbi műveletek általában az előző méretek szorzatával arányos BDR-t eredményezhetnek, így több BDR esetén a méret exponenciálisan nőhet.

Lásd még

• Kielégíthetőségi probléma Boole-képleteknél
• Boole-algebra

Jegyzetek

1. ↑ Graph-Based Algorithms for Boolean Function Manipulation, Randal E. Bryant, 1986
2. ↑ Cy Lee. "Kapcsoló áramkörök ábrázolása bináris döntési programokkal". Bell Systems Technical Journal, 38:985-999, 1959.
3. ↑ Sheldon B. Akers. Bináris határozati diagramok archiválva 2007. augusztus 7-én a Wayback Machine -nél  (2013. 05. 13. óta lefelé irányuló kapcsolat [3458 nap] - előzmények ) , IEEE Transactions on Computers, C-27(6):509-516, 1978. június.
4. ↑ Raymond T. Boute, "A bináris döntési gép, mint programozható vezérlő". EUROMICRO Hírlevél, 1. évf. 1(2):16-22, 1976. január
5. ↑ Yu. V. Mamrukov, Aperiodikus áramkörök és aszinkron folyamatok elemzése. Értekezés Ph.D. LETI, 1984, 219p.
6. ↑ 1 2 Randal E. Bryant. " Graph-Based Algorithms for Boolean Function Manipulation Archivált : 2015. szeptember 23. a Wayback Machine -nél ." IEEE Transactions on Computers, C-35(8):677-691, 1986.
7. ↑ RE Bryant, " Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams" Archiválva : 2015. szeptember 23., a Wayback Machine , ACM Computing Surveys, Vol. 24. sz. 3 (1992. szeptember), pp. 293-318.
8. ↑ Karl S. Brace, Richard L. Rudell és Randal E. Bryant. " BDD-csomag hatékony megvalósítása" . In Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990), 40-45. oldal. IEEE Computer Society Press, 1990.
9. ↑ Beate Bollig, Ingo Wegener. Az OBDD-k változó sorrendjének javítása NP-Complete , IEEE Transactions on Computers, 45(9):993-1002, 1996. szeptember.
10. ↑ Detlef Seeling. "Az OBDD minimalizálás megközelíthetetlensége." Információ és számítás 172, 103-138. 2002.

• R. Ubar, "Tesztgenerálás digitális áramkörökhöz alternatív grafikonokat használva (orosz nyelven)", in Proc. Tallinn Technical University, 1976, No.409, Tallinn Technical University, Tallinn, Estonia, pp. 75–81.

Javasolt olvasmány

• DE Knuth, "A számítógépes programozás művészete, 4. kötet, 1. fascicle: Bitenkénti trükkök és technikák; Bináris döntési diagramok" (Addison-Wesley Professional, 2009. március 27.) viii+260pp, ISBN 0-321-58050-8 . A Fascicle 1b tervezete letölthető.
• H.R. Andersen " Bevezetés a bináris döntési diagramokba ", előadásjegyzetek, 1999, Koppenhágai IT Egyetem.
• Ch. Meinel, T. Theobald, " Algoritmusok és adatstruktúrák a VLSI-tervezésben: OBDD - Alapítványok és alkalmazások" , Springer-Verlag, Berlin, Heidelberg, New York, 1998. A teljes tankönyv letölthető.
• Rüdiger Ebendt; Gorschwin Fey; Rolf Drechsler. Fejlett BDD optimalizálás  . — Springer, 2005. - ISBN 978-0-387-25453-1 .
• Bernd Becker; Rolf Drechsler. Bináris döntési diagramok : elmélet és megvalósítás  . — Springer, 1998. - ISBN 978-1-4419-5047-5 .

Linkek

• ABCD : Armin Biere, Johannes Kepler Universität, Linz ABCD-csomagja.
• CMU BDD , BDD csomag, Carnegie Mellon Egyetem, Pittsburgh
• CUDD : BDD csomag, Colorado Egyetem, Boulder
• CUDD telepítése Windows/Visual Studio környezetekben.
• Biddy : többplatformos akadémiai BDD csomag, Maribori Egyetem, Szlovénia
• JavaBDD , a BuDDy Java portja, amely CUDD-hez, CAL-hoz és JDD-hez is kapcsolódik
• A Berkeley CAL csomag, amely széleskörű manipulációt végez
• A. Costa BFunc , tartalmaz egy BDD logikai egyszerűsítőt, amely akár 32 bemenetet/32 kimenetet is támogat (függetlenül)
• DDD : C++ könyvtár, amely támogatja az egész értékű és hierarchikus döntési diagramokat.
• JINC : A Bonni Egyetemen (Németország) kifejlesztett C++ könyvtár, amely számos BDD-változatot és többszálas feldolgozást támogat.