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

• 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)).