CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams

TL;DR

CFLOBDDs introduce a novel, context-free-language-inspired extension of BDDs that enables heavy substructure reuse through a hierarchical, procedure-call viewpoint. By formalizing a matched-path principle and enforcing structural invariants, CFLOBDDs achieve canonicity and can, in the best cases, double-exponentially compress the representation of Boolean functions relative to decision trees, and exponentially more compactly than ROBDDs for certain families like Hadamard matrices. The framework supports a rich set of operations (including Kronecker products, matrix/vector representations, and quantum-gate constructs) and yields dramatic performance gains in quantum circuit simulations, with large-scale instances (e.g., many-qubit Grover/DJ/BV) outperforming traditional BDD-based approaches. Empirical evidence from microbenchmarks and quantum-simulation tasks demonstrates substantial compression and scalability advantages, though results vary by problem, with tensor-network methods sometimes competitive. Overall, CFLOBDDs offer a powerful, canonical, and reusable substrate for representing and manipulating large discrete structures, with clear applicability to quantum algorithms and beyond.

Abstract

This paper presents a new compressed representation of Boolean functions, called CFLOBDDs (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-compatible alternative to BDDs (Binary Decision Diagrams), and hence useful for representing certain classes of functions, matrices, graphs, relations, etc. in a highly compressed fashion. CFLOBDDs share many of the good properties of BDDs, but--in the best case--the CFLOBDD for a Boolean function can be exponentially smaller than any BDD for that function. Compared with the size of the decision tree for a function, a CFLOBDD--again, in the best case--can give a double-exponential reduction in size. They have the potential to permit applications to (i) execute much faster, and (ii) handle much larger problem instances than has been possible heretofore. CFLOBDDs are a new kind of decision diagram that go beyond BDDs (and their many relatives). The key insight is a new way to reuse sub-decision-diagrams: components of CFLOBDDs are structured hierarchically, so that sub-decision-diagrams can be treated as standalone ''procedures'' and reused. We applied CFLOBDDs to the problem of simulating quantum circuits, and found that for several standard problems the improvement in scalability--compared to simulation using BDDs--is quite dramatic. In particular, the number of qubits that could be handled using CFLOBDDs was larger, compared to BDDs, by a factor of 128x for GHZ; 1,024x for BV; 8,192x for DJ; and 128x for Grover's algorithm. (With a 15-minute timeout, the number of qubits that CFLOBDDs can handle are 65,536 for GHZ, 524,288 for BV; 4,194,304 for DJ; and 4,096 for Grover's Algorithm.)

Figures (35)

• Figure 1: $H_2$ and $H_4$, the first two members of the family of Hadamard matrices ${\mathcal{H}} = \{ H_{2^i} \mid i \geq 1 \}$.
• Figure 2: Decision trees and BDDs for $H_2$ and $H_4$, with plies in interleaved most-significant-bit order---$\langle x_0, y_0 \rangle$ and $\langle x_0, y_0, x_1, y_1 \rangle$, respectively. The bold paths show the assignments $[{x_0} \mapsto F, {y_0} \mapsto T]$ (for $H_2[0,1]$) and $[{x_0} \mapsto F, {y_0} \mapsto T, {x_1} \mapsto F, {y_1} \mapsto T]$ (for $H_4[0,3]$), respectively.
• Figure 3: (a) CFLOBDD for $H_2$ using the variable ordering $\langle x_0, y_0 \rangle$. The bold path is for the assignment $[{x_0} \mapsto F, {y_0} \mapsto T]$ for $H_2[0,1]$. (b) Guide to the terminology introduced in Defn. \ref{['De:MockCFLOBDD']}.
• Figure 4: (a) Datatypes for Grouping, InternalGrouping, DontCareGrouping, ForkGrouping, and CFLOBDD. (b) The CFLOBDD for $H_2$ (repeated from Fig. \ref{['Fi:walsh1']}a). (c) An instance of class CFLOBDD that represents $H_2$.
• Figure 5: CFLOBDD for the Boolean function $\lambda {x_0}{x_1}{x_2}{x_3} . (x_0 \oplus x_1) \lor (x_0 \land x_1 \land x_2)$. (For clarity, some of the level-0 groupings have been duplicated.)

Theorems & Definitions (20)

• definition 1: Mock-CFLOBDD; see Fig. \ref{['Fi:walsh1']}b
• definition 2: Mock-proto-CFLOBDD
• definition 3: Proto-CFLOBDD and CFLOBDD
• Proposition 4.1: Lexicographic-Order Proposition
• theorem 1: Canonicity
• definition 4
• theorem 2: Exponential separation for the equality relation
• theorem 3: Exponential separation for the Hadamard relation
• definition 5
• theorem 4: Exponential separation for the addition relation