Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Binary Decision Diagram Manipulation in External Memory

Steffan Christ Sølvsten, Jaco van de Pol, Anna Blume Jakobsen, Mathias Weller Berg Thomasen

TL;DR

This work tackles the bottleneck of manipulating large BDDs that exceed main memory by introducing time-forward processing for I/O-efficient BDD algorithms. It presents Adiar, a new BDD package that implements simplified and improved Apply/Reduce and extends the approach to additional operators, leveraging an arc-based representation and a levelized priority queue. The experimental results show Adiar can handle BDDs larger than memory and achieve competitive performance, with slowdown factors that are acceptable given the memory savings and disk-based scalability; equality checks are improved to $O(\text{sort}(N))$-type bounds. The practical impact is a viable external-memory BDD tool suitable for symbolic model checking and other applications requiring very large BDDs, with clear directions for future enhancements such as deeper equality optimization and broader operator support.

Abstract

We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply. These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD packages that use recursive depth-first algorithms. For instances larger than 8.2 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages.

Efficient Binary Decision Diagram Manipulation in External Memory

TL;DR

This work tackles the bottleneck of manipulating large BDDs that exceed main memory by introducing time-forward processing for I/O-efficient BDD algorithms. It presents Adiar, a new BDD package that implements simplified and improved Apply/Reduce and extends the approach to additional operators, leveraging an arc-based representation and a levelized priority queue. The experimental results show Adiar can handle BDDs larger than memory and achieve competitive performance, with slowdown factors that are acceptable given the memory savings and disk-based scalability; equality checks are improved to -type bounds. The practical impact is a viable external-memory BDD tool suitable for symbolic model checking and other applications requiring very large BDDs, with clear directions for future enhancements such as deeper equality optimization and broader operator support.

Abstract

We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply. These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD packages that use recursive depth-first algorithms. For instances larger than 8.2 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages.

Paper Structure

This paper contains 46 sections, 16 theorems, 14 equations, 14 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Contributions
  4. Overview
  5. Preliminaries
  6. The I/O-Model
  7. Cache-Oblivious Algorithms
  8. TPIE
  9. Binary Decision Diagrams
  10. I/O-Complexity of Binary Decision Diagrams
  11. BDD Manipulation by Time-forward Processing
  12. Apply
  13. Pruning by Short Circuiting the Operator
  14. Reduce
  15. Other Algorithms
  16. ...and 31 more sections

Key Result

Proposition 3.1

The Apply algorithm in Fig. fig:apply has I/O complexity $O(\text{sort}(N_f \cdot N_g))$ and $O((N_f\cdot N_g) \cdot \log (N_f \cdot N_g))$ time complexity, where $N_f$ and $N_g$ are the respective sizes of the BDDs for $f$ and $g$.

Figures (14)

  • Figure 1: Examples of Reduced Ordered Binary Decision Diagrams. Leaves are drawn as boxes with the boolean value and internal nodes as circles with the decision variable. Low edges are drawn dashed while high edges are solid.
  • Figure 2: Running time of BuDDy Lind1999 solving Tic-Tac-Toe for $N=21$ on a laptop with $8$ GiB memory and $8$ GiB swap (lower is better).
  • Figure 3: In-order representation of BDDs of Fig. \ref{['fig:bdd_example']}
  • Figure 4: The Apply--Reduce pipeline of our proposed algorithms
  • Figure 5: Unreduced output of Apply when computing $x_2 \Rightarrow (x_0 \wedge x_1)$
  • ...and 9 more figures

Theorems & Definitions (28)

  • Proposition 3.1: Following Arge 1996 Arge1996
  • proof
  • Lemma 3.2
  • proof
  • Proposition 3.3: Following Arge 1996 Arge1996
  • proof
  • Lemma 3.4
  • Proposition 3.5
  • proof
  • Proposition 3.6
  • ...and 18 more