Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)

Steffan Christ Sølvsten, Jaco van de Pol

TL;DR

This work introduces nested sweeping to extend IO-efficient BDD manipulation to multi-variable quantification within the Adiar framework. By coordinating an outer Apply/Reduce sweep with nested inner Apply/Reduce sweeps, the method computes existential (and universal) quantifications and supports the relational product in an external-memory setting. The authors provide formal complexity bounds, a suite of optimisations, and an implementation in Adiar v2.0, accompanied by extensive experiments showing notable improvements (approximately 1.7x average speedups and ~21% total time reduction) over prior approaches and competitive performance against CAL and depth-first BDD packages on larger instances. The results demonstrate practical impact for solving QBFs and GoE problems with BDDs that exceed main memory, and the framework lays groundwork for broader IO-efficient, multi-recursive BDD operations and future extensions such as variable reordering and other decision diagram variants.

Abstract

Previous research on the Adiar BDD package has been successful at designing algorithms capable of handling large Binary Decision Diagrams (BDDs) stored in external memory. To do so, it uses consecutive sweeps through the BDDs to resolve computations. Yet, this approach has kept algorithms for multi-variable quantification, the relational product, and variable reordering out of its scope. In this work, we address this by introducing the nested sweeping framework. Here, multiple concurrent sweeps pass information between eachother to compute the result. We have implemented the framework in Adiar and used it to create a new external memory multi-variable quantification algorithm. Compared to conventional depth-first implementations, Adiar with nested sweeping is able to solve more instances of our benchmarks and/or solve them faster.

Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)

TL;DR

This work introduces nested sweeping to extend IO-efficient BDD manipulation to multi-variable quantification within the Adiar framework. By coordinating an outer Apply/Reduce sweep with nested inner Apply/Reduce sweeps, the method computes existential (and universal) quantifications and supports the relational product in an external-memory setting. The authors provide formal complexity bounds, a suite of optimisations, and an implementation in Adiar v2.0, accompanied by extensive experiments showing notable improvements (approximately 1.7x average speedups and ~21% total time reduction) over prior approaches and competitive performance against CAL and depth-first BDD packages on larger instances. The results demonstrate practical impact for solving QBFs and GoE problems with BDDs that exceed main memory, and the framework lays groundwork for broader IO-efficient, multi-recursive BDD operations and future extensions such as variable reordering and other decision diagram variants.

Abstract

Previous research on the Adiar BDD package has been successful at designing algorithms capable of handling large Binary Decision Diagrams (BDDs) stored in external memory. To do so, it uses consecutive sweeps through the BDDs to resolve computations. Yet, this approach has kept algorithms for multi-variable quantification, the relational product, and variable reordering out of its scope. In this work, we address this by introducing the nested sweeping framework. Here, multiple concurrent sweeps pass information between eachother to compute the result. We have implemented the framework in Adiar and used it to create a new external memory multi-variable quantification algorithm. Compared to conventional depth-first implementations, Adiar with nested sweeping is able to solve more instances of our benchmarks and/or solve them faster.
Paper Structure (35 sections, 5 theorems, 2 equations, 16 figures, 2 tables)

This paper contains 35 sections, 5 theorems, 2 equations, 16 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Contributions
  3. Preliminaries
  4. The I/O-Model
  5. Binary Decision Diagrams
  6. I/O-efficient BDD Manipulation
  7. I/O-efficient Multi-variable Quantification
  8. Outer Apply:
  9. Outer Reduce:
  10. Inner Apply:
  11. Inner Reduce:
  12. Complexity of Nested Sweeping
  13. Optimisations for Nested Sweeping
  14. Terminal Arcs:
  15. Bail-out of Inner Sweep:
  16. ...and 20 more sections

Key Result

lemma thmcounterlemma

A single BDD $f$ with $N$ nodes can be transposed in $\Theta(\text{sort} ( N ))$ I/Os and time and $\Theta(N)$ space.

Figures (16)

  • Figure 1: Examples of Reduced Ordered Binary Decision Diagrams. Terminals are drawn as boxes surrounding their Boolean value. Internal nodes are drawn as circles and contain their decision variable. Arcs to the high and low child are respectively drawn solid and dashed.
  • Figure 2: A recursive multi-variable exists operation.
  • Figure 3: BDD Representations in Adiar.
  • Figure 4: The Apply--Reduce pipeline of or in Adiar.
  • Figure 5: Step-by-step example of the or of $x_1$ (\ref{['fig:bdd_example:x1']}) and $x_0 \land \neg x_1$ (\ref{['fig:bdd_example:x0&-x1']}) with time-forward processing; subfigures show the state after processing each level. Arcs in gray are pushed to the algorithm's priority queue whereas the ones in black have been written to the output file.
  • ...and 11 more figures

Theorems & Definitions (9)

  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • corollary thmcountercorollary
  • lemma thmcounterlemma
  • proof
  • proposition thmcounterproposition
  • proof