Polynomial Bounds of CFLOBDDs against BDDs

TL;DR

This article shows that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function h cannot be far worse than the size of the BDD for h.

Abstract

Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs -- roughly, they are BDDs augmented with a certain form of procedure call. A natural question to ask is, ``For a given family of Boolean functions $F$, what is the relationship between the size of a BDD for $f \in F$ and the size of a CFLOBDD for $f$?'' Sistla et al. established that there are best-case families of functions, which demonstrate an inherently exponential separation between CFLOBDDs and BDDs. They showed that there are families of functions $\{ f_n \}$ for which, for all $n = 2^k$, the CFLOBDD for $f_n$ (using a particular variable order) is exponentially more succinct than any BDD for $f_n$ (i.e., using any variable order). However, they did not give a worst-case bound -- i.e., they left open the question, ``Is there a family of functions $\{ g_i \}$ for which the size of a CFLOBDD for $g_i$ must be substantially larger than a BDD for $g_i$?'' For instance, it could be that there is a family of functions for which the BDDs are exponentially more succinct than any corresponding CFLOBDDs. This paper studies such questions, and answers the second question posed above in the negative. In particular, we show that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function $h$ cannot be far worse than the size of the BDD for $h$. The bound that relates their sizes is polynomial: If BDD $B$ for function $h$ is of size $|B|$ and uses variable ordering $\textit{Ord}$, then the size of the CFLOBDD $C$ for $h$ that also uses $\textit{Ord}$ is bounded by $O(|B|^3)$. The paper also shows that the bound is tight: there is a family of functions for which $|C|$ grows as $Ω(|B|^3)$.

Figures (15)

• Figure 1: (Color online.) The BDD for $f_0 = \lambda b_0, b_1, b_2 \,.\,(\text{if } b_0 \text{ then }1 \text{ else }0) + (\text{if } b_2 \text{ then }1 \text{ else }0)$.
• Figure 2: (Color online.) The CFLOBDD for $f_1 \buildrel \hbox{\tiny\rm def} \over = \lambda b_0, b_1 \,.\, (\text{if (} b_0 \land \neg b_1\text{) then 7 else 5})$.
• Figure 3: Guide to the modifiers on the term "CFLOBDD(s)."
• Figure 4: (Color online.) (a) An illustration of "3/4-depth duplication." (b) A hypothetical scenario where "3/4-depth duplication" propagates, causing the size of $C$ to grow exponentially compared with the size of $B$. The middle vertices enclosed in purple rectangles in (b) indicate the duplicates caused by the hypothesized propagation of "3/4-depth duplication" to groupings at the next-lower level, which could potentially propagate to still further lower levels. (To reduce clutter, return edges are elided in these diagrams.)
• Figure 5: (Color online.) The BDD (left) and the CFLOBDD (right) for the function "$\textit{if}\ (\neg x_0)\ \textit{then}\ (\textit{if}\ (\neg x_1)\ \textit{then}\ v_0\ \textit{else}\ v_1)\ \textit{else}\ v_2$."

Theorems & Definitions (35)

• definition 1: Mock-CFLOBDD
• definition 2: Mock-proto-CFLOBDD
• theorem 1: Canonicity
• definition 3
• theorem 2
• proof
• definition 4
• lemma 1
• lemma 2
• proof