libcudd is cool library to build and manipulate BDD in C. It’s used in several application in digital design such formal verification or synthsis (timing and power).

The following snipper from libcudd github repo

The CUDD package is a package written in C for the manipulation of decision diagrams. It supports binary decision diagrams (BDDs), algebraic decision diagrams (ADDs), and Zero-Suppressed BDDs (ZDDs).

For chatgpt, we get this nice one-liner

CUDD constructs Reduced Ordered Binary Decision Diagrams (ROBDDs). Key characteristics: Binary: Each node represents a decision on a variable (true/false). Ordered: Variables are tested in a fixed order say Reduced: Duplicate/redundant subgraphs are merged to minimize the graph.

Installation Link to heading

The installation works the same on linux and MacOS.

wget https://raw.githubusercontent.com/davidkebo/cudd/main/cudd_versions/cudd-3.0.0.tar.gz
tar xvf cudd-3.0.0.tar.gz
cd cudd-3.0.0
./configure --prefix=$HOME/.local
make
make install

Hello World Link to heading

The first example of boolean expression ((X0 and X1) OR X2) and dot graph from the BDD. Obviously we have to run dot to get the diagram. The Makefile has the commands linking to libcudd.a.

all:
	gcc -o bdd_example bdd_example.c -lcudd -L../../../../sources/cudd-3.0.0/cudd/.libs -I../../../../sources/cudd-3.0.0/cudd
	./bdd_example
	dot -Tpng bdd.dot -o bdd.png

clean:
	rm -f bdd_example bdd.dot bdd.png

Cudd_bddIthVar is used to create 3 variables with indices 0 to 2. Then The functions Cudd_bddAnd , Cudd_Not and Cudd_bddOr are used to build the expression.

#include <stdio.h>
#include "cudd.h"

int main() {
    // Initialize CUDD manager
    DdManager *manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);

    // Create 3 BDD variables: x0, x1, x2
    DdNode *x0 = Cudd_bddIthVar(manager, 0);
    DdNode *x1 = Cudd_bddIthVar(manager, 1);
    DdNode *x2 = Cudd_bddIthVar(manager, 2);

    // Build: (x0 AND x1)
    DdNode *and_node = Cudd_bddAnd(manager, x0, x1);
    Cudd_Ref(and_node); // Always ref after creating new node

    // Build: NOT x2
    DdNode *not_x2 = Cudd_Not(x2);  // No need to Cudd_Ref for Cudd_Not

    // Build: (x0 AND x1) OR (NOT x2)
    DdNode *f = Cudd_bddOr(manager, and_node, not_x2);
    Cudd_Ref(f);

    // Output the BDD as a DOT file
    FILE *fp = fopen("bdd.dot", "w");
    DdNode *nodes[] = {f};
    Cudd_DumpDot(manager, 1, nodes, NULL, NULL, fp);
    fclose(fp);

    printf("BDD written to bdd.dot\n");

    // Cleanup
    Cudd_RecursiveDeref(manager, and_node);
    Cudd_RecursiveDeref(manager, f);
    Cudd_Quit(manager);
    return 0;
}

Example image