imported>Saure: /* Einleitung */

2022-11-29T08:28:32Z

Einleitung

Neue Seite

'''Reduced Binary Circuit''' stellen eine Möglichkeit dar, digitale [[Integrierter Schaltkreis|Schaltkreise]] mit wenig [[Overhead (EDV)|Overhead]] kompakt zu repräsentieren. Resultat ist ein [[Graph_%28Graphentheorie%29#Gerichteter_azyklischer_Graph|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 [[Wahrheitswert]]en {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 [[Isomorphismus|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, {{ISSN|0302-9743}} (Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00)).

[[Kategorie:Programmierbare Logik]]

Reduced Binary Circuits - Versionsgeschichte

imported>Saure: /* Einleitung */