Binært beslutningsdiagram

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 2. januar 2020; checks kræver 3 redigeringer .

Et binært beslutningsdiagram ( BDE ) eller et forgreningsprogram er en form for at repræsentere en boolsk funktion af variable som en rettet acyklisk graf , bestående af interne beslutningsknuder (mærket ), som hver har to børn , og to terminalknuder (mærket 0) og 1) , som hver svarer til en af de to værdier af den boolske funktion. I udenlandsk litteratur kaldes binære beslutningsdiagrammer og forgreningsprogrammer for henholdsvis binært beslutningsdiagram ( BDD ) og forgreningsprogrammer ( BP ). $f(x_{1},x_{2},...,x_{n})$ $n$ $x_{i}$

Definition

En boolsk funktion kan repræsenteres som en rettet acyklisk graf , bestående af flere interne beslutningsknuder og to terminalknudepunkter, kaldet en 0-terminal node og en 1-terminal node. Hver intern beslutningsknude på et niveau er mærket med en boolsk variabel og har to børn , kaldet et junior-barn og et senior-barn. Overgangen fra en intern knude til et yngre eller ældre barn udføres afhængigt af værdien af variablen (henholdsvis 0 eller 1). For de givne værdier svarer stien fra rodknudepunktet til 1-terminalknudepunktet til, at på disse inputværdier tager den boolske funktion værdien 1. $f(x_{1},x_{2},...,x_{n})$ $jeg$ $x_{i}$ $x_{i}$ $x_{i}$ $x_{1},x_{2},...,x_{n}$ $f(x_{1},x_{2},...,x_{n})$

En BDR siges at være ordnet, hvis forskellige variable optræder i samme rækkefølge i alle stier fra grafens rodknude til et af de terminale hjørner. Samtidig kan nogle variabler i stierne være fraværende, hvis reduktionsoperationen tidligere blev udført på grafen.

En BDR kaldes forkortet , hvis følgende to forkortelsesregler anvendes på grafen:

Sammenlægning af isomorfe undergrafer.
Fjernelse af alle noder med isomorfe børn.

I de fleste tilfælde forstås et binært beslutningsdiagram som et reduceret ordnet binært beslutningsdiagram ( SUBDR ). Fordelen ved en reduceret ordnet BDD er, at den er kanonisk (unik) for en bestemt funktion og en given rækkefølge af variable. [1] Denne egenskab gør RUBMS nyttig til at teste funktionel ækvivalens.

Eksempel

Figuren til venstre viser et binært beslutningstræ (uden at anvende reduktionsreglerne) svarende til sandhedstabellen for den boolske funktion vist i samme figur . For givne inputværdier , , kan du bestemme værdien af den boolske funktion ved at bevæge dig langs træet fra træets rodknude til terminalknuderne og vælge overgangsretningen fra noden afhængigt af inputværdien . De stiplede linjer i figuren repræsenterer overgange til et yngre barn, og de kontinuerlige linjer repræsenterer overgange til et ældre barn. For eksempel, hvis inputværdierne ( , , ) er givet, skal du fra rodnoden gå langs den stiplede linje til venstre (da værdien er 0), derefter skal du gå langs de kontinuerlige linjer til højre (da værdierne er lig med 1). Som et resultat vil vi ende i en 1-terminal node, det vil sige værdien er 1. $f(x_{1},x_{2},x_{3})$ $x_{1}$ $x_{2}$ $x_{3}$ $x_{i}$ $x_{i}$ $x_{1}=0$ $x_{2}=1$ $x_{3}=1$ $x_{1}$ $x_{1}$ $x_{2}$ $x_{3}$ $f(x_{1}=0,x_{2}=1,x_{3}=1)$

Det binære beslutningstræ i figuren til venstre kan konverteres til et binært beslutningsdiagram ved at anvende to reduktionsregler. Den resulterende BDR er vist i figuren til højre.

Historie

Hovedideen til at skabe en sådan datastruktur var Shannon-nedbrydningen . Enhver boolsk funktion på en af inputvariablerne kan opdeles i to underfunktioner, kaldet positivt og negativt komplement, hvorfra kun én underfunktion vælges efter if-then-else princippet afhængigt af værdien af inputvariablen (hvorpå Shannon-udvidelsen blev udført). Ved at repræsentere hver sådan underfunktion som et undertræ og fortsætte udvidelsen i de resterende inputvariabler, kan der opnås et beslutningstræ , hvis reduktion vil give et binært beslutningsdiagram . Information om brugen af binære beslutningsdiagrammer eller binære forgreningsprogrammer blev først offentliggjort i 1959 i Bell Systems Technical Journal [2] [3] [4] . En BDD kaldet den kanoniske parentes blev implementeret af Mamrukov [5] i CAD til analyse af hastighedsuafhængige kredsløb. Potentialet for at skabe effektive algoritmer baseret på denne datastruktur blev undersøgt af Randal Bryant fra Carnegie Mellon University : hans tilgang var at bruge en fast rækkefølge af variabler (for en unik kanonisk repræsentation af hver boolesk funktion) og genbrug af almindelige undergrafer (for kompakthed) ). Anvendelsen af disse to nøglekoncepter gør det muligt at øge effektiviteten af datastrukturer og algoritmer til at repræsentere sæt og relationer mellem dem. [6] [7] Brugen af fælles undergrafer af flere BDR'er har ført til fremkomsten af datastrukturen Shared Reduced Ordered Binary Decision Diagram . [8] Navnet BDR bruges nu primært til netop denne datastruktur.

Donald Knuth kaldte i sin videoforelæsning Fun With Binary Decision Diagrams (BDD'er) binære beslutningsdiagrammer " en af de virkelig fundamentale datastrukturer, der er opstået i de sidste femogtyve år " og bemærkede, at Randal Bryants 1986 -publikation [6 ] , som fremhævede brugen af binære beslutningsdiagrammer til manipulation af boolske funktioner, var i nogen tid den mest citerede publikation inden for datalogi.

Ansøgning

BDR'er bruges i vid udstrækning i computerstøttet design (CAD) systemer til syntese af logiske kredsløb og til formel verifikation .

Inden for elektronik kan hver specifik BDR (selv ikke reduceret og ikke bestilt) implementeres direkte ved at erstatte hver node med en multiplekser med to indgange og en udgang.

Rækkefølgen af variabler

Størrelsen af BDR bestemmes både af en boolsk funktion og af valget af rækkefølgen af inputvariablerne. Ved kompilering af en graf for en boolesk funktion kan antallet af noder i bedste tilfælde lineært afhænge af , og i værste fald kan afhængigheden være eksponentiel med et mislykket valg af rækkefølgen af inputvariablerne. For eksempel givet en boolesk funktion Hvis du bruger rækkefølgen af variable , så skal du bruge 2 n +1 noder til at repræsentere funktionen i form af en BDD. En illustrativ BDD for en funktion af 8 variable er vist i figuren til venstre. Og hvis du bruger ordren , så kan du få en tilsvarende BDR fra 2 n +2 noder. En illustrativ BDD for en funktion af 8 variable er vist i figuren til højre. $f(x_{1},\ldots,x_{{n}})$ $n$ $f(x_{1},\ldots ,x_{{2n}})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{{2n-1}}x_{{ 2n}}.$ $x_{1}<x_{3}<\cdots <x_{{2n-1}}<x_{2}<x_{4}<\cdots <x_{{2n}}$ $x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{{2n-1}}<x_{{2n}}$

Valget af variabel rækkefølge er afgørende, når sådanne datastrukturer anvendes i praksis. Problemet med at finde den bedste rækkefølge af variable er et NP-komplet problem. [9] Desuden er selv problemet med at finde en suboptimal rækkefølge af variabler NP-komplet , således at for enhver konstant c > 1 er størrelsen af BDD højst c gange større end den optimale. [10] Der er dog effektive heuristika til at løse dette problem.

Derudover er der funktioner, hvor størrelsen af grafen altid vokser eksponentielt i takt med, at antallet af variable stiger, uanset rækkefølgen af variablerne. Dette gælder for multiplikationsfunktioner, der angiver den store kompleksitet af faktorisering .

Forskning i binære beslutningsdiagrammer har ført til fremkomsten af mange relaterede typer grafer, såsom BMD ( Binary Moment Diagrams ), ZDD ( Zero Suppressed Decision Diagram ), FDD ( Free Binary Decision Diagrams ), PDD ( Parity decision Diagrams ) og MTBDD'er (Multiple terminal BDD'er).

Logiske operationer på binære beslutningsdiagrammer

Mange logiske operationer ( konjunktion , disjunktion , negation ) kan udføres direkte på BDR ved hjælp af algoritmer, der udfører grafmanipulationer i polynomisk tid. Men at gentage disse operationer mange gange, for eksempel når der dannes konjunktioner eller disjunktioner af et sæt BDD'er, kan i værste fald føre til en eksponentielt stor BDD. Dette skyldes, at alle tidligere operationer på to BDR'er generelt kan resultere i en BDR med en størrelse, der er proportional med produktet af de tidligere størrelser, så for flere BDR'er kan størrelsen stige eksponentielt.

Se også

Noter

↑ Graf-baserede algoritmer for boolesk funktionsmanipulation, Randal E. Bryant, 1986
↑ Cy Lee. "Repræsentation af skiftekredsløb ved binære beslutningsprogrammer". Bell Systems Technical Journal, 38:985-999, 1959.
↑ Sheldon B. Akers. Binære beslutningsdiagrammer arkiveret 7. august 2007 på Wayback Machine (downlink siden 05/13/2013 [3458 dage] - historie ) , IEEE Transactions on Computers, C-27(6):509-516, juni 1978.
↑ Raymond T. Boute, "Den binære beslutningsmaskine som en programmerbar controller". EUROMICRO Nyhedsbrev, Vol. 1(2):16-22, januar 1976
↑ Yu. V. Mamrukov, Analyse af aperiodiske kredsløb og asynkrone processer. Afhandling Ph.D. LETI, 1984, 219 s.
↑ 1 2 Randal E. Bryant. " Grafbaserede algoritmer til boolesk funktionsmanipulation arkiveret 23. september 2015 på Wayback Machine ." IEEE Transactions on Computers, C-35(8):677-691, 1986.
↑ RE Bryant, " Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams" Arkiveret 23. september 2015 på Wayback Machine , ACM Computing Surveys, Vol. 24, nr. 3 (september, 1992), s. 293-318.
↑ Karl S. Brace, Richard L. Rudell og Randal E. Bryant. " Effektiv implementering af en BDD-pakke" . I Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990), side 40-45. IEEE Computer Society Press, 1990.
↑ Beate Bollig, Ingo Wegener. Forbedring af den variable rækkefølge af OBDD'er er NP-Complete , IEEE Transactions on Computers, 45(9):993-1002, september 1996.
↑ Detlef Seeling. "Utilnærmeligheden af OBDD-minimering." Information and Computation 172, 103-138. 2002.

R. Ubar, "Test Generation for Digital Circuits Using Alternative Graphs (på russisk)", i Proc. Tallinn Technical University, 1976, nr. 409, Tallinn Technical University, Tallinn, Estland, pp. 75-81.

Foreslået læsning

DE Knuth, "The Art of Computer Programming Volume 4, Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams" (Addison-Wesley Professional, 27. marts 2009) viii+260pp, ISBN 0-321-58050-8 . Udkast til Fascicle 1b tilgængelig til download.
H.R. Andersen " An Introduction to Binary Decision Diagrams ", Lecture Notes, 1999, IT-Universitetet i København.
Ch. Meinel, T. Theobald, " Algorithms and Data Structures in VLSI-Design: OBDD - Foundations and Applications" , Springer-Verlag, Berlin, Heidelberg, New York, 1998. Komplet lærebog tilgængelig for download.
Rüdiger Ebendt; Gorschwin Fey; Rolf Drechsler. Avanceret BDD- optimering . — Springer, 2005. - ISBN 978-0-387-25453-1 .
Bernd Becker; Rolf Drechsler. Binære beslutningsdiagrammer : teori og implementering . — Springer, 1998. - ISBN 978-1-4419-5047-5 .

Links

ABCD : ABCD-pakken af Armin Biere, Johannes Kepler Universität, Linz.
CMU BDD , BDD-pakke, Carnegie Mellon University, Pittsburgh
CUDD : BDD-pakke, University of Colorado, Boulder
Installation af CUDD i Windows/Visual Studio-miljøer.
Biddy : akademisk BDD-pakke med flere platforme, Maribor Universitet, Slovenien
JavaBDD , en Java-port af BuDDy, der også har grænseflader til CUDD, CAL og JDD
Berkeley CAL -pakken, der udfører bredde-første manipulation
A. Costa BFunc , inkluderer en BDD boolesk logikforenkling, der understøtter op til 32 indgange / 32 udgange (uafhængigt)
DDD : Et C++-bibliotek med understøttelse af heltalsværdier og hierarkiske beslutningsdiagrammer.
JINC : Et C++-bibliotek udviklet ved universitetet i Bonn, Tyskland, der understøtter flere BDD-varianter og multi-threading.

Datastrukturer
Lister	array enkelt linket liste dobbelt linket liste Beståelsesliste
Træer	B-træ Binært søgetræ AVL træ Rød-sort træ dynge
Tæller	Instrueret graf rettet acyklisk graf Binært beslutningsdiagram Hypergraf
Andet	Hash bord Stak