„Reduced Binary Circuits“ – Versionsunterschied
| [gesichtete Version] | [gesichtete Version] |
Xario (Diskussion | Beiträge) K linkfix |
Trg (Diskussion | Beiträge) K LInk auf BKL aufgelöst |
||
| Zeile 1: | Zeile 1: | ||
'''Reduced Binary Circuit''' stellen eine Möglichkeit dar, digitale [[Schaltkreis]]e mit wenig [[Overhead]] kompakt zu repräsentieren. Resultat ist ein [[Graph_%28Graphentheorie%29#Gerichteter_azyklischer_Graph|gerichteter azyklischer Graph]] ''G'' bestehend aus Knoten und Kanten. |
'''Reduced Binary Circuit''' stellen eine Möglichkeit dar, digitale [[Schaltkreis]]e 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. |
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. |
||
Version vom 18. April 2009, 18:25 Uhr
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.
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)).