Reduced Binary Circuits

Reduced Binary Circuit stellen eine Möglichkeit dar, digitale Schaltkreise mit wenig Overhead kompakt zu repräsentieren. Resultat ist ein gerichteter azyklischer Graph G bestehend aus Knoten und Kanten.

Interne Knoten repräsentieren einen binären Operator aus der Menge {<math> \land , \lor, \Leftrightarrow </math>} und besitzen jeweils zwei Kinder. Blätter hingegen werden mit konstanten Wahrheitswerten {TRUE,FALSE} beschrieben oder durch eine Variable v <math> \epsilon </math> VAR, wobei VAR eine beliebige Menge boolescher Variablen darstellt.

Kanten enthalten ein sign-Attribut, das Negierung des Targets, des Zielknotens abgibt.

Kompression wird dabei erreicht, indem zum einen isomorphe (identische) Teilstrukturen mittels einer Hash-Funktion erfasst und nur einmal explizit in der Datenstruktur repräsentiert werden, zum anderen werden konstante Werte erfasst und „gekürzt“, beispielsweise wird (b <math> \wedge </math>TRUE) dargestellt als b.

Quellen

P. A. Abdullah, P. Bjesse, N. Een: Symbolic Reachability Analysis based on SAT-Solvers. In: Lecture Notes in Computer Science (LNCS). Band 1785/2000, S. 411–425, {{#invoke:URIutil|{{#ifeq:1|1|linkISSN|targetISSN}}|0302-9743|0}}{{#ifeq:1|0|[!]

}}{{#ifeq:0|1

        |{{#switch:00
                  |11= (print/online)
                  |10= (print)
                  |01= (online)
          }}

}}{{#ifeq:0|0

        |{{#ifeq:0|0
              |{{#if:{{#invoke:URIutil|isISSNvalid|1=0302-9743}}
                    |
                    |{{#invoke:TemplUtl|failure|ISSN ungültig}}}}}}

}} (Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00)).