In the last blog post, I explained what are Binary Decision
Diagrams. From an implementation point of view, I presented how to
implement *maximal sharing* via hash-consing.

In this blog post, we will look at the implementation of the usual
operations on logical formulas, and how they translate on BDDs. One of
the meaty part of this blog post will be the discussion of
*memoization* of operations. As we will see, memoization of BDD
operations is necessary to get decent performances out of a BDD
library; yet there are many ways to implement this memoization, and
their mileage may vary under the circumstances.

### A primer on Shannon's expansion

Recall that the term BDDs refers *reduced ordered binary decision
diagrams* and that these are canonical representations of Boolean
functions. The big question about BDDs is the following one: suppose
that I have the BDDs for two functions $ f $ and $ g $, how do we
compute the BDD for functions like $ f \vee g $ or $ f \oplus g $?
It turns out that there is an efficient way to compose BDDs to build
new BDDs that are reduced and ordered by construction and this one of
the reason why BDDs became so popular.

The idea is quite elegant. Recall that any function $f(x_1, ..., x_n)$ can be decomposed as $$ x_1 \cdot f (1, ..., x_n) + \overline{x_1} \cdot f (0, ..., x_n)$$ The two terms that appear in this expression are called the Shannons's cofactors of $ f $ and we will denote them by $~f_{x_1}$ and $~f_{\overline{x_1}}$. What is interesting here is that the decision diagram for $f$ starts with a node for the variable $x_1$ if and only if the two cofactors of $f$ with respect to $x_1$ are different; and there is a clear correspondence between cofactors and sub-diagrams.

Now, let's consider two functions $f$ and $g$. To compute the diagram
for $f \vee g$, we first find what's the variable that should appear
at the root of the diagram: that's either the head variable of $f$ or
the head variable of $g$, and we pick the one which has the lowest
index $i$. Now, we compute the cofactors of $f$ and $g$ with respect
to this variable. We have $$ f \vee g = x_i \cdot (f_{x_i} \vee
g_{x_i}) + \overline{x_i} \cdot (f_{\overline{x_i}} \vee
g_{\overline{x_i}}) $$ That equation means that the diagram for $f
\vee g$ can be expressed in terms of the diagrams for two recursive
calls on "smaller" diagrams, and this nice property holds for any
(binary) Boolean operation. Without going too much into details, all
these operations can be expressed in terms of *node melding*, which
corresponds to an in-order traversal of BDD nodes. This combinator
boils down to the ideas above plus the fact that its behavior is
entirely defined by the results on the leaves of diagrams.

### Intermezzo: implementing the conjunction of BDDs

In this section, we depart from general considerations on the
implementation of BDD operations to actually implement one. Doing so,
we will illustrate the ideas above and highlight the shortcomings of
this first try. (**Note**: if you are interested in *good* implementations
of BDD operations, make sure to read the remainder of this post too.)

```
let rec andb x y =
match x, y with
| F, _ | _, F -> F (* false is the zero element for andb *)
| T, r | r, T -> r (* true is the identity element for andb *)
| N {var = var1; low = low1; high = high1; _},
N {var = var2; low = low2; high = high2; _} ->
let cmp = Var.compare var1 var2 in
if cmp < 0
then (* var1 < var2 *)
mk_node var1 (andb low1 y) (andb high1 y)
else if cmp = 0
then (* var1 = var2 *)
mk_node var1 (andb low1 low2) (andb high1 high2)
else (* var1 > var2 *)
mk_node var2 (andb x low2) (andb x high2)
```

The first two lines of the pattern matching are direct consequences of
the definition of the conjunction: false is the zero element for the
logical and (false and anything is equal to false), and true is its
neutral element. The interesting part of this function is the last
case of the pattern-matching. in this code, we check what is the order
between the head variables of the two arguments to pick the smallest
one. Then, we compute the the cofactors of `x`

and `y`

with respect to
this variable and perform recursive calls on these cofactors, and
re-assemble the results by constructing a new node using our smart
constructor `mk_node`

. (To understand how it works, it might be useful
to convince yourself that the cofactors of `y`

w.r.t. `var1`

in the
first `then`

branch are indeed `y`

. The other cases are similar.)

**Exercise** How would you modify the code above to implement the
logical or rather than the logical and?

### Getting things right: memoizing functions

There is one huge problem with the above implementations: it's runtime
cost is exponential w.r.t. the size of the diagrams. The problem comes
from the fact that the function might end up evaluated exponentially
often on the same couple of subterms. Indeed, our implementation is
oblivious to the fact that there is some sharing in the BDDs, and ends
up processing BDDs as if they were mere Binary Decision Trees. The
goal of this section is to present an example of the *memoization
techniques* that are needed to get efficient implementations of BDD
operations.

In a nutshell, each time we perform a call to `andb`

, we want to check
in a cache whether this particular problem has been solved already. If
it is the case, we can just return the cached value. If it is not the
case, then we perform the computations as described above and perform
recursive calls on the sub-problems. Note that there is nothing
specific to a particular caching strategy in this story, thus our code
should abstract from the strategy. One nice way to achieve that is to
use a programming pattern called *open recursion*.

```
let andb andb x y =
match x, y with
| F, _ | _, F -> F (* false is the zero element for andb *)
| T, r | r, T -> r (* true is the identity element for andb *)
| N {var = var1; low = low1; high = high1; _},
N {var = var2; low = low2; high = high2; _} ->
let cmp = Var.compare var1 var2 in
if cmp < 0
then (* var1 < var2 *)
mk_node var1 (andb low1 y) (andb high1 y)
else if cmp = 0
then (* var1 = var2 *)
mk_node var1 (andb low1 low2) (andb high1 high2)
else (* var1 > var2 *)
mk_node var2 (andb x low2) (andb x high2)
```

The code above is not recursive anymore; rather, we delayed the definition of the way this function calls itself to a later point.

The most simple memoization strategy consists in storing the values
that have been computed in an hash-table, whose keys are pairs of BDDs
and whose values are other BDDs. It is trivial to instanciate the
`Hashtbl.Make`

functor to get hash tables that are specialized for our
efficient equality test and hash functions.

```
type bdd = t
module H2 = struct
type t = bdd * bdd
let equal (a1,b1) (a2,b2) =
uid a1 = uid a2 && uid b1 = uid b2
let hash (a,b) = uid a * 17 + uid b
end
module HT2 = Hashtbl.Make(H2)
```

We are now ready to implement the function that tie the knot of an open recursive function.

```
let memo_rec2 f =
let h = HT2.create 1337 in
let rec g x y =
try HT2.find h (x,y)
with Not_found ->
let r = f g x y in
HT2.add h (x,y) r;
r
in
g
let andb = memo_rec2 andb
```

**Exercise** How would you modify the code above to implement the
logical or rather than the logical and?

**Exercise** How would you modify the code above to implement the
logical exclusive-or? (Hint: you may want to implement the negation
operation first.)

### Going further

There are many different ways to implement the memoizing combinators,
with different performance and memory consumption profiles. For
instance, the combinator that we used above ensures that the
memoization tables are complete, but have an ever increasing memory
footprint. We could also reset the memoization tables from one run of
an operation to the other (that is, recreating the table `h`

for each
top-level call of `memo_rec2 f x y`

). Or, we could add alarms to
OCaml's GC to clear the memoization tables. Or we could have a fixed
size table and knock out the existing key-value pairs when there is a
collision (this corresponds to a degenerate hash table in which
buckets are not lists nor trees, but singletons). These are really
simple variations and your mileage using them may vary.

One more advanced memoization strategy involves the use of something called ephemerons, which make it possible to automatically reclaim the stale bindings that are stored in the memoization tables. We will come back to this subject in a future post.

**Update** Corrected a mistake in the `memo_rec2`

code (thanks to a redditer). Never post when tired.