19. Dez 2007, 01:26

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 {} und besitzen jeweils zwei Kinder. Blätter hingegen werden mit konstanten Wahrheitswerten {TRUE,FALSE} beschrieben oder durch eine Variable v ε 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 TRUE) dargestellt als b.

[Bearbeiten] 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, ISSN 0302-9743 (Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00)).

Dieser Artikel ist eine Kopie aus der freien Enzyklopädie Wikipedia. Am Originalartikel kann jeder Korrekturen und Ergänzungen vornehmen. Zudem kann man frühere Versionen einsehen.

Abkürzungen • Dateiendungen • Netzjargon