Reduced binary circuits

Reduced binary circuits represent a possibility of compactly representing digital circuits with little overhead . The result is a directed acyclic graph G consisting of nodes and edges.

Internal nodes represent a binary operator from the set { } and each have two children. Leaves, however, are described with constant truth values {TRUE, FALSE} or by a variable v VAR, where VAR represents any set of Boolean variables. ${\displaystyle \land ,\lor ,\Leftrightarrow }$ ${\displaystyle \epsilon }$

Edges contain a sign attribute that negates the target, the target node.

Compression is achieved in that, on the one hand, isomorphic (identical) substructures are recorded using a hash function and only explicitly represented once in the data structure; on the other hand, constant values ​​are recorded and “shortened”, for example (b TRUE) is shown as b. ${\displaystyle \wedge }$

swell

• PA Abdullah, P. Bjesse, N. Een: Symbolic Reachability Analysis based on SAT-Solvers . In: Lecture Notes in Computer Science (LNCS) . Volume 1785/2000, pp. 411-425, ISSN  0302-9743 (Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00)).