Reduced Binary Circuits

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 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 {$\land ,\lor ,\Leftrightarrow$} und besitzen jeweils 2 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 Andern 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)).