Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper)

TL;DR

This paper introduces a method to predict the memory demands of BDD operations using maximum graph cuts, enabling more efficient external memory management and significantly reducing computation times.

Contribution

It formalizes the shape of graph cuts in BDD operations and implements upper bounds to predict memory needs, improving performance in external memory BDD manipulation.

Findings

Average reduction of 86.1% in computation time for moderate-sized BDDs

Median time reduction of 89.7%

Case study: 52 hours saved in hardware circuit equivalence checking

Abstract

The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized BDDs. This is mostly due to initializing expensive external memory data structures, even if their contents can fit entirely inside internal memory. The contents of these auxiliary data structures always correspond to a graph cut in an input or output BDD. Specifically, these cuts respect the levels of the BDD. We formalise the shape of these cuts and prove sound upper bounds on their maximum size for each BDD operation. We have implemented these upper bounds within Adiar. With these bounds, it can predict whether a faster internal memory variant of the auxiliary data structures can be used. In practice, this improves Adiar's running time across the board. Specifically for the moderate-sized BDDs, this results in an average reduction of the computation time by 86.1% (median of 89.7%). In some cases, the difference is even 99.9\%. When checking equivalence of hardware circuits from the EPFL Benchmark Suite, for one of the instances the time was decreased by 52 hours.