Chain Reduction for Binary and Zero-Suppressed Decision Diagrams

TL;DR

This paper introduces chain reduction techniques for BDDs and ZDDs, enabling more compact representations and improved efficiency in symbolic Boolean function manipulation.

Contribution

It proposes chain reduction methods for BDDs and ZDDs, with algorithms and experimental validation demonstrating significant memory and time improvements.

Findings

Chain reduction produces smaller BDD and ZDD representations.

Experimental results show reduced memory usage and faster computation.

Chain reduction benefits are evident across various benchmark problems.

Abstract

Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the others' 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.