Introduction to CUDD

Published on the

CUDD stands for Colorado University Decision Diagrams. Over my summer I’ve been working on the model checker, MCMAS, created by Imperial’s VAS (Verification of Autonomous Systems) research group. This uses CUDD extensively, so I thought I’d write a blog post about it. CUDD is a C library for manipulating binary decision diagrams. A binary decision diagram is a data structure to encode a Boolean function. The first advantage of using them is that in practice they are efficient in terms of memory usage. The second advantage is that in practice it is efficient to perform Boolean operations such as conjunction (AND) between BDDs.

Be aware that, I will use “multiply” to mean logical conjunction (AND), and “add” to mean logical disjunction (OR). If you have a BDD representing a three-argument Multiply \(f\) by \(x_3\). To substitute \(x_3 = 0\), you simplify multiply \(f\) by the negation of \(x_3\). Observe if the resulting function is the zero function, i.e. you have a function that always equals 0, then you know that for \(f\) to return 1, \(x_3\) cannpt be the value you substituted in. If it doesn’t equal 0, then there is a solution where \(f\) returns 1, in which \(x_3\) is the value you substituted in.

BDDs can also be used to encode sets. Possible elements of the set can be given a binary encoding, and if the function encoded as a BDD, \(f\), which represents the set, returns 1 given the binary encoding of an element, this signifies the element is present, otherwise it signifies the element isn’t present. Because, BDDs can be used to represent sets, they can be used to represent relations, since relations are just sets whose elements are tuples.

I won’t go into the internals of how BDDs are implemented here. But one thing to bear in mind is that the order in which the variables are stored by the BDD internally impacts performance and memory usage. Each BDD that is a function over the same set of variables must of course, store the variables in the same order, so operations can be performed between these BDDs. In CUDD, each BDD variable is given an index. This index lets you obtain the variable, which you can then use to build more complex functions. By default, the index of the variable is the position of the variable in the internal representation of the BDD. But CUDD allows dynamic reordering, which I will come to later. This means CUDD will adjust the position of variable, through some reordering algorithm, to try and obtain a more efficient ordering. This leaves the indices used to interact with CUDD unchanged, however.

Basic C API

MCMAS uses the C++ API, but this post will discuss the C API.

You can clone CUDD 3.0 from an unofficial GitHub repository here.

To build the library, you can use the following commands, in the root folder of the repository:

The library file produced will be stored in cudd/.libs/libcudd.a. To compile this library file with your own C program, main.c, you can use the following C command:

The -I tells it to look for header files in the cudd directory.

A simple program looks like this:

With the header file:

This creates a BDD manager, which consists of a set of variables, that are the parameters to the function encoded by your BDDs. The first argument indicates the number of BDD variables you want at the beginning. The second argument indicate the number of ZDD variables, which is another type of data structure provided by CUDD, which we won’t go into. The third and fourth parameters are related to how CUDD operates internally. The default values are provided as constants, CUD_UNIQUE_SLOTS and CUDD_CACHE_SLOTS. The fifth parameter is the target value of maximum memory. By giving 0, this asks CUDD to try to figure this out for itself.

To get the ith BDD variable, you can use Cudd_bddIthVar:

If the ith variable doesn’t exist, Cudd will create it. If you just want to create a new variable, you can use, Cudd_bddNewVar:

The index of this variable will be 1 greater than the previous biggest. There are functions to create BDDs from Boolean operations:

This demonstrates AND, there also exist other functions such as: Cudd_bddOr, Cudd_bddXor, Cudd_bddNand, Cudd_bddNor, Cudd_bddXnor. There is also a negation function Cudd_Not, but this doesn’t get passed a DdManager *, only a DdNode *:

The Cudd_Ref is where it gets interesting. CUDD implements its own garbage collection mechanism using reference counts. Variables will never be garbage collected, while the BDD manager is alive. But, BDDs built from them, such as from Cudd_bddAnd start out with a reference count of 0. Every place where bdd1 is stored and used from, needs to increment the reference count. Otherwise, CUDD will destroy it. Incrementing its reference count is done using Cudd_Ref. When a place which stores a BDD, no longer needs it, it is necessary to decrement the reference count.

Note that BDDs are essentially graphs, so a DdNode may have child nodes, which are also DdNode structures. But you don’t need to worry about incrementing the reference count of these child nodes, as CUDD will handle that for you.

There are two ways of decrementing reference counts: Cudd_Deref and Cudd_RecursiveDeref. Cudd_Deref reduces the reference count of the root node, whereas Cudd_RecursiveDeref will also recursively reduce the reference count of any children, if the root node’s reference count becomes 0. Normally you’d use the latter. However, sometimes you have a function that constructs a BDD, and wants to return it with a reference count of 0. In this case, you don’t want to destroy its child nodes, as the reference count may be incremented to 1, as soon as its returned. In this case, Cudd_Deref is used.

The call to Cudd_Quit, gets rid of all remaining nodes belonging to DdManager, which haven’t been freed yet. You can verify yourself with valgrind, that without Cudd_Quit there is a memory leak.

More Complex Stuff

One thing about CUDD, is that two identical BDDs will always be represented by the same DdNode, even if they are constructed separately, and in different ways. This means checking if two nodes are the same, is as simple as comparing the pointers:

It can often be useful to compare BDDs to the always true function, and the always false function. Here’s how you’d obtain them in CUDD:

Another useful comparison operation is Cudd_bddLeq, which takes in a manager and two BDDs, \(a\) and \(b\). It tells you if \(a \to b\). I find it intuitive to think of it in the context of BDDs representing relations. In which case, it tells you whether the set of tuples, that satisfy the first BDD, is a subset of the set of tuples, that satisfy the second BDD.

The final function provided by the API, I want to touch upon is Cudd_bddPickOneMinterm. A minterm is a conjunction of literals that will satisfy a function. For instance if the function is \(f(x_1, x_2, x_3) = x_1 \wedge x_3\), there are two literals:

The function will only return one minterm. You can combine it with a loop to obtain all the minterms. After obtaining one minterm, you can multiply the original BDD with the negation of the minterm. This means the next minterm will be different. The function takes a list of variables, which are the variables you want the minterm over.

Here’s an example of code that enumerates all the minterms of the function \(x_1 \wedge x_3\).

For more information about CUDD, see here. Also check out MCMAS.