Setting up

0 Include the given JBDD class in your project. At runtime, it will try to load a dynamic loadable library (DLL) which must be in your path (see the end of this page).

In Windows, the DLLs normally goes into the same directory as your binary. In Linux, you might need to put the current directory in the library-path. For example (assuming Main.class is your main file):

env LD_LIBRARY_PATH=. java Main

You will also need to change the JDK memory limits:

java -Xms1024m -Xmx4096m Main   (start at/max MBs of memory)

Initialisation

1 Initialise the package by creating a new JBDD object. Note that you are not allowed to have multiple JBDD objects (you shouldn't need it anyway!):

JBDD jbdd = new JBDD(10);  // <-- we will use at most 10 variables

Clean up when you are done using the jbdd.kill() function!

2 BDD variables are created from the JBDD object:

int v1 = jbdd.createBDD();
int v2 = jbdd.createBDD();

As you have noticed, a variable is represented by a java integer. This also applies to BDD trees (a BDD variable is in fact a tree, but that's another discussion).

Simple operations

3 Doing (binary) operations on BDD:s is a matter of a function call:

int v1andv2 = jbdd.and(v1,v2);
int v1orv2 = jbdd.or(v1,v2);

Note that the returned BDD is already referenced (see 4 below) by the interface, but you need to de-ref it yourself!. Note that the extra andTo and orTo operations de-ref the first operand and then ref the returned value. That is

tmp = jbdd.andTo(tmp,v1);

actually equals

int tmp1 = jbdd.and(tmp,v1);
jbdd.deref(tmp);
tmp = tmp1;

Reference counting

4 We use reference-counting for garbage collection. Note that this is "your problem" as the programmer has the complete responsibility for this task. Javas internal garbage collection is not involved!

jbdd.ref(v1);            // <-- ADD a reference to this BDD
System.out.println("v1.refs = " + jbdd.internal_refcount(v1));

jbdd.deref(v1);          // <-- REMOVE our reference
System.out.println("v1.refs = " + jbdd.internal_refcount(v1));

When the ref-count of a BDD tree reaches zero it may get garbage collected at anytime. The debug version of JBDD has extra error checking to prevent you from working with zero-ref BDD:s.

4.b CUDD uses two calls for de-referencing, in BuDDy they are equal. In CUDD, you can also de-ref the current node only (otherwise it will be recursive):

jbdd.localDeref(v1);

Unless you know what you are doing, use deref() at all time.

Performance note: In BuDDy ref() and deref() run in O(1), while they run in O(n) in CUDD (n is the number of nodes in the BDD). This a result of using different garbage collection algorithm (i.e. mark-sweep vs. Ref16).

Permutations and renaming

5 To change the BDD variables in a tree, you first need to create a permutation:

// test replace
int []s = new int[2];
int []sp = new int[2];
s[0] = v1;              s[1] = v2;
sp[0] = v3;             sp[1] = v4;
int s2sp = jbdd.createPair(s,sp);     // <-- this is our S -> Sp "permutation"

The permutation works as the following: any variable s[i] is replaced with the corresponding variable sp[i]. When you have created the permutation "pair", you can use like this:

int rep = jbdd.replace(v1andv2, s2sp); // <-- we have now: rep = v3 & v4

Dont forget to cleanup your permutation-pairs later:

jbdd.deletePair(s2sp);   // must clean up permutation before exit!

6 Similarly, quantification operations requires bdd cubes. These are regular BDDs (cube v = v1 & v2 & ...):

int [] set = new int[2];
set[0] = v1;
set[1] = v2;
int cube = jbdd.makeSet(set,2); // cube = v1 & v2

int f = jbdd.exists(v1andv2,cube); // E v1,v2. (v1 & v2) = 1
int g = jbdd.forall(v1andv2,cube); // A v1,v2. (v1 & v2) = 0

Dont forget to de-ref your cubes when you are done as they are ordinary BDDs!