Reduced Binary Circuits

Dieser Artikel wurde zur Löschung vorgeschlagen.

Falls du Autor des Artikels bist, lies dir bitte durch, was ein Löschantrag bedeutet, und entferne diesen Hinweis nicht.

Zur Löschdiskussion.

Das Familienleben der internen Knoten mag ja interessant sein, aber was dies in einer Enzyklopädie soll bleibt rätselhaft - so rätselhaft wie der Inhalt dieses Beitrages. Weissbier 17:57, 3. Sep 2006 (CEST)

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 { $\land ,\lor ,\Leftrightarrow$ } und besitzen jeweils zwei Kinder. Blätter hingegen werden mit konstanten Wahrheitswerten {TRUE,FALSE} beschrieben oder durch eine Variable v $\epsilon$ VAR, wobei VAR eine beliebige Menge boolscher Variablen darstellt.

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

Kompression wird dabei erreicht, indem zum Einen isomorphe (identische) Teilstrukturen mittels HASHING erfasst und nur einmal explizit in der Datenstruktur repräsentiert werden, zum Anderen werden konstante Werte erfasst und „gekürzt“, beispielsweise wird (b $\wedge$ 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, ISSN 0302-9743 (Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00)).