Since Randy Bryant’s 1986 seminal paper on Binary Decision Diagrams, a data structure that can compactly encode many boolean functions of interest, BDDs have had enormous success in practical applications, including hardware and software verification, model checking, and general exhaustive search problems in discrete domains. Indeed, in his Stanford Lecture Fun With Binary Decision Diagrams (BDDs), Donald Knuth stated that BDDs are "one of the only really fundamental data structures that came out in the last twenty-five years". However, as researchers tackle the analysis of increasingly challenging systems, even BDD-based algorithms may require enormous memory and time. Gianfranco Ciardo and Andrew Miner, both faculty in the Department of Computer Science, have been working with Junaid Babar, who recently earned his Ph.D. in Computer Science at ISU, to improve the efficiency of BDDs. The three coauthored the paper CESRBDDs: binary decision diagrams with complemented edges and edge-specified reductions, which has recently been accepted for publication in the journal Software Tools for Technology Transfer.
CESRBDDs extend and improve BDDs by automatically recognizing and eliminating certain substructures in the traditional BDD encoding, leading to more compact representations that require less memory and computation time. After an extensive theoretical development, which includes proofs of correctness and complexity comparisons with previous classes of BDDs, the paper presents extensive experimental results supporting the conclusion that CESRBDDs are extremely competitive, while still being simple to use, since they do not require users to have a-priori knowledge of what boolean functions (thus special BDD substructures) a specific application will need to encode.
The next step in this work is to implement a robust software library for building and manipulating CESRBDDs, with the goal of having CESRBDDs become the go-to standard for any application using BDDs in its core algorithms.
The following table (from the paper) provides relative scores for the memory or time requirements using CESRBDDs (last column) versus other variants of BDDs proposed in the literature (a smaller score is better).