Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
- PDF / 1,051,378 Bytes
- 31 Pages / 439.37 x 666.142 pts Page_size
- 68 Downloads / 304 Views
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams Randal E. Bryant1 Received: 18 June 2020 / Accepted: 26 June 2020 © Springer Nature B.V. 2020
Abstract Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zerosuppressed binary decision diagrams (ZDDs) to each take advantage of the other’s ability to symbolically represent Boolean functions in compact form. For any Boolean function, its chain-reduced ZDD (CZDD) representation will be no larger than its ZDD representation, and at most twice the size of its BDD representation. The chain-reduced BDD (CBDD) of a function will be no larger than its BDD representation, and at most three times the size of its CZDD representation. Extensions to the standard algorithms for operating on BDDs and ZDDs enable them to operate on the chain-reduced versions. Experimental evaluations on representative benchmarks for encoding word lists, solving combinatorial problems, and operating on digital circuits indicate that chain reduction can provide significant benefits in terms of both memory and execution time. The experimental results are further validated by a quantitative model of how decision diagrams scale when encoding sets of sequences. This model explains why the combination of a one-hot encoding of the symbols in the sequences, plus a CBDD, CZDD, or ZDD representation of the set, yields the most compact form. Keywords Binary decision diagrams · Zero-suppressed binary decision diagrams · Boolean functions
1 Introduction Decision diagrams (DDs) encode sets of values in compact forms, such that operations on the sets can be performed on the encoded representation, without expanding the sets into their individual elements. In this paper, we consider two classes of decision diagrams: reduced ordered binary decision diagrams (BDDs) [5] and zero-suppressed binary decision diagrams (ZDDs) [20,21]. These two representations are closely related to each other, with each achieving more compact representations for different classes of applications. We present extensions to both representations, such that BDDs can take advantage of the source of compaction provided by ZDDs, and vice-versa.
B 1
Randal E. Bryant [email protected] Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA
123
R. E. Bryant Fig. 1 Size bound relations between different representations
n/2 BDD
1
n/2
ZDD
2
1
CBDD
CZDD 3
Both BDDs and ZDDs encode sets of binary sequences of some fixed length n, defining a Boolean function over n variables. We can bound their relative sizes as follows. Suppose for some function, we encode it according to the different DD types. For function f , let T ( f ) indicate the number of nodes (including leaf nodes) in the representation of type T . Let R f (T1 , T2 ) denote the relative sizes when representing f using types T1 and T2 : R f (T1 , T2 ) =
T1 ( f ) T2 ( f )
Comparing BDDs and ZDDs, Knuth [17] has shown that for any function f : R f (BDD, ZDD) ≤ n/2 + o(n)
(1)
R f (ZDD, BDD) ≤ n/2 + o(n)
(2)
Data Loading...
