Binary Decision Diagrams: from Tree Compaction to Sampling

TL;DR

This paper introduces a novel enumeration and sampling method for reduced ordered binary decision diagrams (ROBDDs), enabling efficient generation and analysis of these compact Boolean function representations.

Contribution

It presents a new approach to enumerate ROBDDs without full tree expansion and introduces an unranking and uniform sampling procedure for ROBDDs of fixed size.

Findings

Developed a method for enumerating ROBDDs by size

Created an unranking procedure for ROBDDs

Provided a uniform sampler for ROBDDs of given variables and size

Abstract

Any Boolean function corresponds with a complete full binary decision tree. This tree can in turn be represented in a maximally compact form as a direct acyclic graph where common subtrees are factored and shared, keeping only one copy of each unique subtree. This yields the celebrated and widely used structure called reduced ordered binary decision diagram (ROBDD). We propose to revisit the classical compaction process to give a new way of enumerating ROBDDs of a given size without considering fully expanded trees and the compaction step. Our method also provides an unranking procedure for the set of ROBDDs. As a by-product we get a random uniform and exhaustive sampler for ROBDDs for a given number of variables and size.

Equations

$${\mathcal{P}}_T(\nu )=\left\{\tau \in T\mid \tau {\prec }_{\text{pre}}\nu \text{ and }I(\tau )<I(\nu )\right\}\cup \left\{\perp ,\top \right\}.$$

$${\nu }_{\alpha }{\prec }_{\text{pre}}\nu \text{ and }I({\nu }_{\alpha })<I(\nu )\text{ for }\alpha \in \{\text{0},\text{1}\}\text{ and }{\nu }_{\text{0}}\ne {\nu }_{\text{1}},$$

$${\nu }_{\text{0}}{\prec }_{\text{pre}}\nu ,I({\nu }_{\text{0}})<I(\nu )\text{ and }{\nu }_{\text{1}}={\delta }^{\prime }(\nu ,\text{1}).$$

$${\nu }_{\text{1}}{\prec }_{\text{post}}\nu ,{\nu }_{\text{1}}\ne {\nu }_{\text{0}}\text{ and }I({\nu }_{\text{1}})<I(\nu ).$$

$$w_{T}(\nu)=\begin{cases}1&\text{if $\delta^{\prime}(\nu,0)\neq\textsc{nil}$ and $\delta^{\prime}(\nu,1)\neq\textsc{nil}$}\\ \lVert{p_{T}(\nu)}\rVert\big{(}\lVert{p_{T}(\nu)}\rVert-1\big{)}-s_{T}(\nu)&\text{if $\delta^{\prime}(\nu,0)=\delta^{\prime}(\nu,1)=\textsc{nil}$}\\ \lVert{p_{T}(\nu)+\operatorname*{profile}(T^{\prime})}\rVert&\text{if $\delta^{\prime}(\nu,0)\neq\textsc{nil}$ and $\delta^{\prime}(\nu,1)=\textsc{nil}$}\\ \lVert{p_{T}(\nu)}\rVert&\text{if $\delta^{\prime}(\nu,0)=\textsc{nil}$ and $\delta^{\prime}(\nu,1)\neq\textsc{nil}$}\\ \end{cases}$$

$$N(n,k)={\sum }_{T\in {\mathcal{T}}_{n-2,k}}W(T),$$

$${\mathcal{T}}_{m,\mathbf{p},s}=\{T_{\nu }\mid (\exists T\in \mathcal{T})(\exists \nu \in T)p_T(\nu )=\mathbf{p}\text{ and }{s}_T(\nu )=s\}.$$

$$T^{\prime }\in \bigcup _{k_0\in \{1,\dots ,k-1\}}{\mathcal{T}}_{i,(p_0,\dots ,p_{k_0-1}),p_{k_0}}$$

$$T^{\prime \prime }\in \bigcup _{k_1\in \{1,\dots ,k-1\}}{\mathcal{T}}_{m-i-1,(p_0^{\prime },\dots ,p_{k_1-1}^{\prime }),p_{k_1}^{\prime }},\text{ with p′=p+profile(T′)}$$

$$\displaystyle\text{if $m=1$ then $\textstyle\big{(}\sum_{i=0}^{k}p_{i}\big{)}\cdot\big{(}-1+\sum_{i=0}^{k}p_{i}\big{)}-s>0$}.$$

$$N(n,k)=\sum _{(\mathbf{t},w)\in \text{count(n−2,(2,0,…,0),0)}}w,$$

Full text

1 Introduction

The representation of a Boolean function as a binary decision tree has been used for decades. Its main benefit, compared to other representations like a truth table or a Boolean circuit, comes from the underlying divide-and-conquer paradigm. Thirty years ago a new data structure emerged, based on the compaction of binary decision tree, and hereafter denoted as Binary Decision Diagrams (or bdds) [1]. Its takeoff has been so spectacular that many variants of compacted structures have been developed, and called through many acronyms as presented in [14]. One way to represent the different diagrams consists in their embedding as directed acyclic graphs (or dags). One reason for the existence of all these variants of diagrams is due to the fact that each dag correspondence has its own internal agency of the nodes and thus each representation is oriented towards a specific constraint. For example, the case of Reduced Ordered Binary Decision Diagrams (robdds) is such that the variables do appear at most once and in the same order along any path from the source to a sink of the dag, and furthermore, no two occurrences of the same subgraph do appear in the structure. For such structures and others, like qobdds or zbdds for example, there is a canonical representation of each Boolean function.

In his book [9] Knuth proves or recalls combinatorial results, like properties for the profile of a bdd, or the way to combine two structures to represent a more complex function. However, one notes an unseemly fact. There are no results about the distribution of the Boolean functions according to their robdd size. In fact in contrast to (e.g.) binary trees where there is a recursive characterization that allows to well specify the trees, we have no local-constraint here for robdds ans thus a similar recurrence is unexpected. Very recently, there is a first study exploring experimentally, numerically, and theoretically the typical and worst-case robdd sizes in [12]. We aim at obtaining the same kind of combinatorial results but here we design a partition of the decision diagrams that allows us to go much further in terms of size. In particular we obtain an exhaustive enumeration of the diagrams according to their size up to 9 variables. This was unreachable through the exhaustive approach proposed in [12] due to the double exponential complexity of the problem: there are $2^{2^{k}}$ Boolean functions with $k$ variables. Our c++ implementation fully manages the case of $9$ variables (see Fig 2) that corresponds to $2^{512}\approx 10^{154}$ functions. In particular for 9 Boolean variables, our implementation shows one seventh of all robdds are of size 132 (the possible sizes range from $3$ to $143$). Furthermore, robdds of size between $125$ and $143$ represents more than $99.8\%$ of all robdds, in accordance with theoretical results from [13, 8].

Starting from the well-known compaction process (that takes a binary decision tree and outputs its compacted form, the robdd), our combinatorial study gives a way of construction for robdds of a given size, but without the compaction step. We further define a total order over the set of robdds and we propose both an unranking and an exhaustive generation algorithm. The first one gives as a by-product a uniform random sampler for robdds of a given number of variables and size. One strength of our approach is that it allows to sample uniformly robdds of “small” size, for instance of linear size w.r.t the number $k$ of variables, very efficiently in contrast to a naive rejection algorithm. The usual uniform distribution on Boolean functions [13] yields with high probability robdds of near maximal size of order $2^{k}/k$, although robdds encountered in applications, when tractable, are smaller. As a perspective, once the unranking method is well understood, and in particular the poset underlying the robdds, then we might be able to bias the distribution to sample only in a specific subclass, e.g. robdds corresponding to a particular class of formulas (e.g. read-once formulas).

Our results have practical applications in several contexts, in particular for testing structures and algorithms. The study given in [3] executes tests for an algorithm whose parameter is a binary decision diagram. It is based on QuickCheck [2], the famous software, taking as an entry a random generator and generating test cases for test suites. Using our uniform generator, we aim at obtaining statistical testing, in the sense that the underlying distribution of the samples is uniform, thus allowing to extract statistics thanks to the tests. Another application of our approach allows to derive exhaustive testing for small structures, like the study in [10], that we also can conduct inside QuickCheck.

In this paper, we focus exclusively on robdds which is one of the first and simplest variants. Section 2 introduces the combinatorics underlying the decision tree compaction, leading in Section 3 to a way to unambiguously specify the structure of reduced ordered binary decision diagrams. We apply this strategy in Section 4 and obtain an unranking algorithm for robdds.

2 Decision diagrams as compacted trees

This section defines precisely our combinatorial context. Many definitions are detailed in the monograph of Wegener [14] and in the dedicated volume [9] of Knuth.

In this section we first recall a one-to-one correspondence between the representation of a Boolean function as a binary decision tree (built on a specific variable ordering and seen as a plane tree, i.e. the children of an internal nodes are ordered) and a reduced ordered binary decision diagram (robdds) also seen as a plane structure. This approach is non-classical in the context of bdds, but it allows the formalization of an equivalence relationship on robdds that is the key of our enumeration: in fact our approach foundation relies on breaking down the symmetry in robdds. We consider Boolean function on $k$ variables. We recall there are $2^{2^{k}}$ such Boolean functions. The compaction process is now formalized.

Compaction and plane decision diagrams A Boolean function can be represented thanks to a binary decision diagram, which is a rooted, directed, acyclic graph, which consists of decision nodes and terminal nodes. There are two types of terminal nodes $\top$ and $\bot$ corresponding to truth values (resp. 1 and 0 ). Each decision node $\nu$ is labeled by a Boolean variable $x_{\nu}$ and has two child nodes (called low child and high child). The edge from node $\nu$ to a low (or high) child represents an assignment of $x_{\nu}$ to 0 and is represented as a dotted line (respectively 1, represented as a solid line). In the following we represent robdds and decision trees (or bdds in general) as plane structures, i.e. for a node we consider its low child to be its left child and the high child to be its right child.

In a (plane) full binary decision tree, no subtree is shared. By contrast we may decrease the number of decision nodes by factoring and sharing common substructures. Representing a function with its full decision tree is not space efficient. In Fig. 3 we depict, on top, a decision tree of a Boolean function on 4 variables. In the bottom of the figure we represent the compaction of the latter decision tree by using the classical common subexpression recognition notion (cf. e.g. [4, 7]) based on a postorder traversal of the tree.

Definition 1 (Compaction)

Let $T$ be the (plane) binary decision tree of a function $f$. The dag $T$ is modified through a postorder traversal. When the node $\nu$ is under visit, $\nu$ being a child of a node $\rho$. If an identical subtree than $T_{\nu}$, the one rooted in $\nu$, has already be seen during the traversal, rooted in a node $\mu$, then $T_{\nu}$ is removed from $T$ and the node $\rho$ gets a pointer to $\mu$ (replacing the edge to $\nu$). Once $T$ has been traversed, the resulting dag is the plane robdd of $f$.

In our figures of robdds we draw the pointers in red (there is an exception for the edges to the terminal nodes as we remark in Fig. 3 also drawn in red).

In a classical setting, robdds are obtained by applying repetitively reduction rules (well detailed in [14]) to obdds, and the process is confluent. Our approach conceptually takes as a starting point a full decision tree with a given ordering on variables (meaning all nodes at the same level are labeled by the same variable) and applies the compaction rules by examining nodes of the tree in postorder.

For example the plane robdd in Fig. 3 corresponds to the leftmost robdd depicted (in the classical way) in Fig.1. Note that for a given Boolean function, using two distinct variable orderings can lead to two robdds of different sizes (see Fig. 1 for such a situation). Nonetheless, an ordering of the variables being fixed, each Boolean function is represented by exactly one single robdd obtained through the compaction of its decision tree for this order.

In the rest of the paper, we consider only plane robdds. From now we thus call them bdds. We also assume the set of variables $X=\{\ldots>x_{k}>\ldots>x_{1}\}$ is totally ordered.

Our first goal aims at giving an effective method to enumerate bdds with a chosen number $k$ of variables and size $n$. A first naive approach is: (1) enumerate all the $2^{2^{k}}$ Boolean functions by construction of the decision trees; (2) apply the compaction procedure; and (3) finally filter the bdds of size equal to the target size $n$. This algorithm ceases to be practical for $k$ larger than $4$ (see [12]).

In this paper, we propose a new combinatorial description of bdds providing the basis for an enumeration algorithm avoiding the enumeration of all Boolean functions on $k$ variables.

3 Recursive decomposition

This section introduces a canonical and unambiguous decomposition of the bdds yielding a recursive algorithm for their enumeration.

Automaton point of view Let us introduce an equivalent representation for a bdd. A bdd can indeed be described as a deterministic finite automaton with additional constraints and properties. This point of view gives a convenient formal characterization of the decomposition of bdds used in our algorithms.

Definition 2 (BDD as an automaton)

A bdd $B$ of index $k$ is a tuple $(Q,I,r,\delta)$ where

• •

$Q$ is the set of nodes of the bdd. $Q$ contains two special sink nodes $\bot$ and $\top$.

• •

$I:Q\to\{0,\dots,k\}$ is the index function which associates with every node its index. By convention the index of both sink nodes is [math].

• •

$r\in Q$ is the root and has index $I(r)=k$.

• •

$\delta:Q\setminus\{\bot,\top\}\times\{{\texttt{0}},{\texttt{1}}\}\to Q$ is the full transition function.

There are constraints on $\delta$ translating the classical ones of the bdds:

• •

for any node $\nu\in Q\setminus\{\bot,\top\}$, $\delta(\nu,{\texttt{0}})\neq\delta(\nu,{\texttt{1}})$.

• •

for any distinct nodes $\mu$ and $\nu$ with the same index, we have $\delta(\mu,{\texttt{0}})\neq\delta(\nu,{\texttt{0}})$ or $\delta(\mu,{\texttt{1}})\neq\delta(\nu,{\texttt{1}})$.

• •

the graph underlying $\delta$ forms a dag with a unique node of in-degree 0, the root $r$.

• •

if $\tau=\delta(\nu,\alpha)$ for some $\alpha\in\{{\texttt{0}},{\texttt{1}}\}$ then $I(\tau)<I(\nu)$.

We say $\tau$ is the low child of $\nu$ (respectively high child of $\nu$) if $\delta(\nu,{\texttt{0}})=\tau$ (resp. $\delta(\nu,{\texttt{1}})=\tau$).

Definition 3 (Spine of a BDD, tree and non-tree edges)

Let a bdd $B=(Q,I,r,\delta)$ of root-index $k$. The spine of $B$ is the spanning tree obtained by a depth-first search of the (plane) bdd (where low child is accessed before the high one), and omitting the sinks $\bot$ and $\top$. For a bdd $B$, the edges of the spine forms the set of tree edges (drawn in black). The other edges form the set of non-tree edges (drawn in red). We describe the spine $T$ as a tuple $T=(Q^{\prime},I,r,\delta^{\prime})$ with set of nodes $Q^{\prime}=Q\setminus\{\bot,\top\}$ (with the same index function $I$ as for $B$). The edges of the spine are described using a partial transition function $\delta^{\prime}:Q^{\prime}\times\{{\texttt{0}},{\texttt{1}}\}\to Q^{\prime}\cup\{\textsc{nil}\}$ where nil is a special symbol designating an undefined transition.

Using standard terminology for depth-first search, non-tree edges are either forward or cross edges. We remark that, by definition, a dag admits no cycles and still in the standard notation, it has no backward edges.

Undefined values of the transition function $\delta^{\prime}$ can conveniently be seen as half edges. Since in a bdd every non-sink node has two children, the spine of a bdd of size $n$ has $(n-2)$ nodes and $(n-1)$ half edges (drawn in red in Fig. 1). The four possible types of a node are depicted, as the roots in Fig. 4.

Definition 4 (Valid tree)

A binary tree is said to be valid if it is the spine of some bdd. The set of spines of size $n$ is denoted as $\mathcal{T}_{n}$.

See Fig. 5 for examples of valid and invalid trees. To the best of our knowledge, there is no way to characterize valid trees, apart from exhibiting a robdd admitting this tree as a spine. We will discuss this point later.

For enumerating bdds it will prove convenient to introduce the profile list of a set of nodes and some other useful notation for lists manipulation.

Definition 5

The profile of $\mathcal{N}$, denoted by $\operatorname*{profile}(\mathcal{N})$, is a list with $(k+1)$ components $\boldsymbol{p}=(p_{0},\dots,p_{k})$ where $k=\max_{\nu\in\mathcal{N}}I(\nu)$ is the maximal index and $p_{i}$ is the number of nodes of index $i$ in $\mathcal{N}$.

This definition extends naturally to trees, graphs, etc. We also equip the set of lists with a ‘$+$’ operation: let two lists $\boldsymbol{v}=(v_{0},\dots,v_{m})$ and $\boldsymbol{v}^{\prime}=(v^{\prime}_{0},\dots,v^{\prime}_{n})$ with $n\geq m$ (w.l.o.g.), the sum $\boldsymbol{v}+\boldsymbol{v}^{\prime}$ is equal to $\boldsymbol{w}=(w_{0},\dots,w_{n})$ where for all $0\leq i\leq m,\;w_{i}=v_{i}+v^{\prime}_{i}$ and otherwise, when $m<i\leq n,\;w_{i}=v^{\prime}_{i}$.

In the following, we will use two orderings on the nodes of a plane bdd induced by depth-first search, and called postordering and preordering. Since the structure is plane these orderings correspond exactly with the classical postorder traversal and the preorder traversal of its spanning tree. In a tree, for a node $\nu$ with low child $\nu_{\texttt{0}}$ and high child $\nu_{\texttt{1}}$, the postorder traversal visits the subtree rooted at $\nu_{\texttt{0}}$ then, the one rooted at $\nu_{\texttt{1}}$ and finally $\nu$. The preorder traversal first visits the node $\nu$, then the subtree rooted at $\nu_{\texttt{0}}$ and finally the subtree rooted at $\nu_{\texttt{1}}$. We use the notation $\mu\prec_{\text{post}}\nu$ (resp. $\mu\prec_{\text{pre}}\nu$) if the node $\mu$ is visited before $\nu$ using the postorder (resp. preorder) traversal.

We characterize now how the partial transition function of the spine is related to the full transition function of the bdd. Introducing the pool and level set of a node, we describe the valid choices for non-tree edges to yield a bdd.

Definition 6 (Pool and level set)

Let $T$ be the spine of a bdd. The pool of a node $\nu\in T$ is

[TABLE]

The pool profile $p_{T}(\nu)$ of a node $\nu$ in a spine $T$ is $p_{T}(\nu)=\operatorname*{profile}(\mathcal{P}_{T}(\nu))$.

The level set of $\nu$ is $\mathcal{S}_{T}(\nu)=\{\tau\in T\mid\tau\prec_{\text{pre}}\nu\text{ and }I(\tau)=I(\nu)\}$, and the level rank $s_{T}(\nu)=\lvert{\mathcal{S}_{T}(\nu)}\rvert$ of a node $\nu$ is the rank of $\nu$ among the set of nodes with the same index.

Informally the pool of a node $\nu$ of a tree $T$ is the set of nodes we could choose as a low child for $\nu$ without invalidating the spine. The first component of a pool profile is always $2$ since both sinks $\bot$ or $\top$ are present in the pool of any node of the spine (providing the underlying bdd is not reduced to 1 or 0).

Proposition 1

Let $T=(Q^{\prime},I,r,\delta^{\prime})$ be a valid spine with set of nodes $Q^{\prime}$, root $r$ and partial transition function $\delta^{\prime}:Q^{\prime}\times\{{\texttt{0}},{\texttt{1}}\}\to Q^{\prime}\cup\{\textsc{nil}\}$. The full transition function $\delta:Q^{\prime}\times\{{\texttt{0}},{\texttt{1}}\}\to Q^{\prime}\cup\{\bot,\top\}$ is the transition function of a bdd with spine $T$ if and only for any node $\nu\in Q^{\prime}$, noting $\nu_{\texttt{0}}=\delta(\nu,{\texttt{0}})$ and $\nu_{\texttt{1}}=\delta(\nu,{\texttt{1}})$, the pair $(\nu_{\texttt{0}},\nu_{\texttt{1}})$ satisfies

• (i)

if $\delta^{\prime}(\nu,{\texttt{0}})\neq\textsc{nil}$ and $\delta^{\prime}(\nu,{\texttt{1}})\neq\textsc{nil}$ then $\nu_{\alpha}=\delta^{\prime}(\nu,\alpha)$ for $\alpha\in\{{\texttt{0}},{\texttt{1}}\}$.

• (ii)

if $\delta^{\prime}(\nu,{\texttt{0}})=\delta^{\prime}(\nu,{\texttt{1}})=\textsc{nil}$, then

[TABLE]

and there is no node $\tau\neq\nu$ with the same index as $\nu$ such that $\delta(\tau,\cdot)=\delta(\nu,\cdot)$.

• (iii)

if $\delta^{\prime}(\nu,{\texttt{0}})=\textsc{nil}$ and $\delta^{\prime}(\nu,{\texttt{1}})\neq\textsc{nil}$, then

[TABLE]

• (iv)

if $\delta^{\prime}(\nu,{\texttt{0}})\neq\textsc{nil}$ and $\delta^{\prime}(\nu,{\texttt{1}})=\textsc{nil}$, then $\nu_{\texttt{0}}=\delta^{\prime}(\nu,{\texttt{0}})$ and

[TABLE]

Proof

Since $\delta(\cdot,\cdot)$ must extend $\delta^{\prime}(\cdot,\cdot)$, case $(i)$ is trivial since we must only extend the transition function where $\delta(\nu,\alpha)=\textsc{nil}$. In case $(ii)$, we have to choose for $(\nu_{\texttt{0}},\nu_{\texttt{1}})$ two nodes in the pool of $\nu$ ($\nu$ is an external node of the spine). We use the preorder traversal (but since $\nu$ is an external node, the postorder would also be fine). Moreover $\nu_{\texttt{0}}\neq\nu_{\texttt{1}}$ and no node with the same index as $\nu$ can have the exact same descendants $(\nu_{\texttt{0}},\nu_{\texttt{1}})$ in accordance with Definition 2. In case $(iii)$, the low child must be chosen in the pool of $\nu$ since we preserve the spine. In case $(iv)$, the high child of $\nu$ is also chosen in the pool $\nu$ or in the descendants of $\nu_{\texttt{0}}$ in the spine $T$ (still different from $\nu_{\texttt{0}}$ by Definition 2). $\hfill\square$

4 Counting and Generating BDDs

In this section, we sketch algorithms in order to count and sample bdds of a given size $n$ and given number $k$ of variables.

Counting BDDs

Given a spine $T$, we can compute the number of bdds corresponding with this spine. Thus counting bdds of a certain size $n$ will consists in building all valid spines of size $(n-2)$ and completing the transition function of the spine in all possible ways according to Proposition 1.

Definition 7 (Weight)

Let $T=(Q^{\prime},I,\delta^{\prime},r)$ be a spine, the weight $w_{T}(\nu)$ of a node $\nu\in Q^{\prime}$ is the number of possibilities for completing the transition function $\delta^{\prime}(\mu,\cdot)$ and yielding a bdd with spine $T$. The cumulated weight of a subtree $T_{\nu}$ rooted at $\nu\in T$ is $W_{T}(\nu)=\prod_{\tau\in T_{\nu}}w_{T}(\tau)$. We write $W(T)=W_{T}(r)$ to denote the cumulated weight of the whole spine $T$ rooted at $r$.

Note that the number of choices for the missing transitions out of a node $\nu$ are the ones remaining after previous choices have been made for other nodes of the spine.

Proposition 2 (Weight of a node)

Let $T$ be a spine $T$, the weight of a node $\nu\in T$ is

[TABLE]

where $p_{T}(\nu)$ is the pool profile of node $\nu$, $T^{\prime}=T_{\nu_{0}}$ is the subtree (when defined) rooted at $\nu_{0}=\delta^{\prime}(\nu,{\texttt{0}})$, and, for a list $\boldsymbol{p}=(p_{0},\dots,p_{k})$, we denote $\lVert{\boldsymbol{p}}\rVert=\sum_{i=0}^{k}p_{i}$.

In the third case, by $p_{T}(\nu)+\operatorname*{profile}(T^{\prime})$, we mean the profile of the set of nodes visited before $\nu$ with the postorder traversal of $T$ and of index strictly smaller than $I(\nu)$.

Proof

This is a direct application of Proposition 1. $\hfill\square$

This formula allows to detect if a tree is a valid spine. Indeed as soon as the weight of a node is zero or negative, there is no way to define a total transition function $\delta$ for a bdd. Note that this situation can only happen for external nodes having two half edges, since for any node $\nu\in Q^{\prime}$ and any spine $T$, $\lVert{p_{T}(\nu)}\rVert\geq 2$.

In Fig. 5, the binary tree on the left is invalid and cannot be the spine of any bdd. The two other trees on the right have weights $4$ and $24$, i.e., are resp. the spines of exactly $4$ and $24$ bdds. It is an open problem to characterize the set of valid trees (apart from exhibiting corresponding bdds).

Proposition 2 gives access to the total weight of the spine $W(T)$ using a recursive procedure. A natural way to proceed algorithmically is to use a recursive postorder traversal of the tree maintaining at each node the weight in a multiplicative manner. To do so we need to keep track in the traversal of the pool profile and level rank of the current node.

Initially the pool of the root is reduced to the set $\{\bot,\top\}$. Thus the initial pool profile of the root of index $k$ is initialized to $(2,0,\dots,0)$ of length $k$. The level rank of the root of the spine is [math].

Proposition 3

Let $N(n,k)$ be the number of bdds of index $k$ and size $n$

[TABLE]

where $\mathcal{T}_{m,k}$ is the set of valid spines with $m$ nodes for bdds of index $k$.

Proof

The weight of a spine is the number of ways of extending the transition function of $T$ (Proposition 1), hence the number of bdds for this given spine. $\hfill\square$

Combinatorial description of spines

The set of spines is not straightforward to characterize in a combinatorial way. Indeed we need context to decide if the weight of a particular node in a tree is [math] or less, which in turn yields that the tree is not valid . To enumerate spines, we build recursively binary trees, and, while computing weights for its nodes, as soon we can decide the (partially built) tree is not valid, the tree is discarded.

To decompose (or count) spines of any size or index, $\mathcal{T}=\bigcup_{n\geq 1}\bigcup_{k\geq 1}\mathcal{T}_{n,k}$, we introduce a partition over subtrees which can occur in a spine $T\in\mathcal{T}$. The goal is to identify identical subtrees occurring within different spines and with the same weight to avoid redundant computations.

The combinatorial description we are about to present originates from the following observation: let us fix a spine $T$ and a node $\nu\in T$. From Proposition 2, to compute the cumulated weight of the subtree $T_{\nu}$ rooted at $\nu$, the sole knowledge of the pool profile $p_{T}(\nu)$ and the level rank $s_{T}(\nu)$ is sufficient.

Let $S$ and $S^{\prime}$ be two subtrees with respective roots $\nu$ and $\nu^{\prime}$ in some spines $T$ and $T^{\prime}$, we denote $S\equiv S^{\prime}$ if the following three conditions are satisfied:

• •

both trees have the same size: $\lvert{S}\rvert=\lvert{S^{\prime}}\rvert$;

• •

the roots of both trees have the same pool profile: $p_{T}(\nu)=p_{T^{\prime}}(\nu^{\prime})$;

• •

the roots of both trees have the same level rank: $s_{T}(\nu)=s_{T^{\prime}}(\nu^{\prime})$.

The set $\mathcal{T}_{m,\boldsymbol{p},s}$ is the class equivalence for the relation ‘$\equiv$’ and gathers trees (as a set, without multiplicities) which are possible subtrees of size $m$ in any spine, knowing only the pool profile $\boldsymbol{p}$ and level rank $s$ of the root of the subtree. More formally:

[TABLE]

Note that we have $\mathcal{T}_{n,k}=\mathcal{T}_{n,(2,0,\dots,0),0},$ where $(2,0,\dots,0)$ has $k$ components.

Proposition 4

*The set $\mathcal{T}_{m,\boldsymbol{p},s}$ of subtrees of size $m$ rooted at a node having pool profile $\boldsymbol{p}=(p_{0},\dots,p_{k-1})$ and level rank $s$ occurring in the set of spines $\mathcal{T}$ is decomposed without any ambiguity. We decompose a subtree $T\in\mathcal{T}_{m,\boldsymbol{p},s}$ as a tuple $(\nu,T^{\prime},T^{\prime\prime})$ where the root $\nu$ has index $k$ and $T^{\prime}$ and $T^{\prime\prime}$ are its left and right (possibly empty) subtrees of respective sizes $i$ and $m-1-i$, with $0\leq i\leq m-1$, and verifying (when non empty) *

[TABLE]

This proposition ensures that we can decompose unambiguously subtrees occurring in spines in accordance with the equivalence relation ‘$\equiv$’. Practically this means that instead of considering all possible subtrees for all possible spines, we can compute cumulative weights for each representative of the equivalence relation (which are fewer although still of exponential cardinality).

Algorithm count($n,\boldsymbol{p},s$) in Algorithm 1 enumerates spines of bdds and, at the same time, computes their cumulated weights. It takes as arguments a size $n$ for considering all subtrees of size $n$, assuming an initial pool profile $\boldsymbol{p}=(p_{0},\dots,p_{k-1})$, level rank $s$ and index $k$ for the root of these trees. It returns in an associative array a list of pairs $(\boldsymbol{t},w)$ where

• •

$\boldsymbol{t}=(t_{0},t_{1},\dots,t_{k-1},t_{k})$ ranges over the set of profiles of trees in $\mathcal{T}_{m,\boldsymbol{p},s}$, i.e., $\boldsymbol{t}\in\{\operatorname*{profile}(T)\mid T\in\mathcal{T}_{m,\boldsymbol{p}=(p_{0},\dots,p_{k-1}),s}\}$.

• •

$w$ is the sum over all equivalent trees of size $m$ with profile $\boldsymbol{t}$ of their cumulated weights when the root has pool profile $\boldsymbol{p}$ and level rank $s$ (which gives enough information to compute the cumulated weight for each tree using Proposition 2).

Note that any subtree $T$ with a root of index $i$ has a profile $\boldsymbol{t}=(t_{0},\dots,t_{i})$ with $t_{0}=0$ and $t_{i}=1$.

Proposition 5

The number $N(n,k)$ of bdds of size $n$ and of index $k$ is computed thanks to Algorithm count()* and is equal to*

[TABLE]

where $(2,0,\dots,0)$ has $k$ components and corresponds with a pool reduced to the two sink nodes $\bot$ and $\top$ of index [math].

Proof

Indeed $\boldsymbol{t}$ ranges over all possible profiles for spines of size $(n-2)$ and we sum the weights of all spines for these profiles. Hence we compute exactly the number of bdds of size $n$. $\hfill\square$

An important refinement for this algorithm is to remark when summing over all spines, we consider subtrees of the same size whose root shares the same pool profile and same level rank, hence the same context. In order to avoid performing the same exact computations twice (or more) we can use memoization technique (that is storing intermediary results). It is an important trick to reduce the time complexity, although at the cost of some memory consumption.

Complexity of the counting algorithm

First, we remark the numbers involved in the computations are (very) big numbers (as seen before, of order $2^{2^{k}}$).

Proposition 6

The complexity (in the number of arithmetic operations) of the computations of the Algorithm 1 to evaluate $N(n,k)$ is $O\left(\frac{1}{k}2^{3k^{2}/2+k}\right)$.

For Boolean functions in $k$ variables, although the time complexity of our algorithm is of exponential growth $2^{3k^{2}/2}$. However the state space of Boolean functions is $2^{2^{k}}$ thus our computation is still much better than the exhaustive construction.

Unranking BDDs

Using the classical recursive method for the generation of structures [15] we base our generation approach on the combinatorial counting approach. Since the class of objects under study seems not admissible in the sense given in Analytic Combinatorics [6], we cannot directly apply the advanced techniques presented in [5] nor the approaches by Martínez and Molinero [11]. Thus we devise an unranking algorithm for bdds and get as by-products algorithms for uniform random sampling and exhaustive generation.

The ranking/unranking techniques for objects of a combinatorial class $\mathcal{C}$ of size $N$ consists in building a bijection between any $c\in\mathcal{C}$ and an integer (its rank) in the interval $[0\mathinner{\ldotp\ldotp}N-1]$ (if we starts from [math]). This leads trivially to a uniform sampling algorithm by drawing uniformly first an integer and then building the corresponding object.

Proposition 7

Once the pre-computations are done, the unranking (or uniform random sampling) algorithm needs $O\left(n\cdot|\mathcal{T}_{n,k}|\right)$ arithmetic operations to build a bdd of index $k$ and size $n$.

First, remark that the worst case happens when $n$ is of order the largest possible size of a bdd over $k$ variables $O(\frac{2^{k/2}}{k})$ (cf. [9, p. 102]) which corresponds to the generic case according to Fig. 2. Furthermore, the number of profiles is of order $2^{\frac{k^{2}}{2}}$. To generate a bdd given its rank, we first identify the correct profile of its spine (by enumeration). Then according to this target profile, recursively, for each node, we traverse at most all spines with this profile, in order to decompose the substructures in its left and right part, yielding the upper bound.

As a conclusion, note the process of enumerating, counting and sampling we introduced can be adapted to subclasses of functions (for instance those for which all variables are essential), but also to other strategies of compaction, like those used for Quasi-Reduced bdds and Zero-suppressed bdds. A natural question is also to provide an algorithm enumerating valid spines and not all invalid ones as well to get more efficient enumeration and unranking algorithms for robdds. These questions will be addressed in future work.

Acknowledgement. We thank the anonymous reviewers whose comments and suggestions helped improve and clarify this manuscript.