ADD-Lib API

With the ADD-Lib API we aim to provide an easy-to-use, object-oriented, Java-like interface to the extensive CUDD functionality. The API introduced, in particular

The ADD-Lib API distinguishes between 4 basic types/classes of decision diagrams, BDDs, ADDs, ZDDs, and XDDs each of which bundle the associated CUDD functions to make them accessible easily and quickly. Note that this high-level API will never constrain you as you can always go back to the CUDD-like API and work with pointers directly.

Disjunction: A Minimal BDD Example

Analogously to the examples for the use of our CUDD-like API, let’s start with a minimal BDD example: the disjunction of two variables, var0 and var1:

/* Initialise DDManager with default values */
BDDManager ddManager = new BDDManager();

/* Get the variables */
BDD var0 = ddManager.ithVar(0);
BDD var1 = ddManager.ithVar(1);

/* Build the disjunction */
BDD disjunction = var0.or(var1);
var0.recursiveDeref();
var1.recursiveDeref();

/* Evaluate disjunction for assignment var0 := 1, var1 := 0 */
BDD terminal = disjunction.eval(true, false);

/* See if the terminal is what we expect it to be */
BDD one = ddManager.readOne();
System.out.println("[[ terminal.equals(one) ]] = " + terminal.equals(one));

/* Release memory */
disjunction.recursiveDeref();
one.recursiveDeref();
ddManager.quit();

After instantiation of the BDDManager, we use it to obtain the primitive BDDs for the 0th respectively the 1st variable. Newly instantiated BDDs like these will automatically be referenced for you. With the variables we build their disjunction and can dereference the two variables as they are no longer needed. The remainder of the code snipped evaluates the disjunction for an exemplary variable assignment (var0 := 1, var1 := 0) and checks its equality to the constant 1-BDD. Finally, remaining references are released before we quit the BDDManager to release its memory.

The ADD-Lib API references newly instantiated BDDs automatically in method calls like ithVar() and or() where new BDDs are created. However, methods like eval that return BDDs that exists prior to the call will not affect any references.

Method names are chosen analogously to those of CUDD so you can always refer to the original CUDD documentation on BBDs, ADDs, and ZDDs for a more detailed description of the provided functionality. If you are missing any of CUDD’s functionality in the ADD-Lib API you can always go back to the CUDD-like API using the ptr() method.

The Exact ADD Example from the CUDD Manual

Just like in CUDD and through the CUDD-like API you can use ADDs over real numbers (i.e. double values). For a comparison consider the following example that implements the exact ADD example from the CUDD manual using the ADD-Lib API:

/* Initialise DDManager with default values */
ADDManager ddManager = new ADDManager();

/* Get a constant */
ADD f = ddManager.constant(5);

/* Multiply constant with some variables */
for (int i = 3; i >= 0; i--) {

    /* Get the variable */
    ADD var = ddManager.ithVar(i);

    /* Multiply the variable to the product */
    ADD tmp = var.times(f);
    f.recursiveDeref();
    var.recursiveDeref();
    f = tmp;
}

/* ... */

/* Release memory */
f.recursiveDeref();
ddManager.quit();

Custom Operations by Callback

The ADD-Lib API also allows you to define your own operations directly on terminal values. The apply and monadicApply methods accept lambda functions defining operations directly on double values and apply it to the decision diagram. The below example realises an operation that sums its operands and adds the constant 8 to it:

/* Initialise DDManager with default values */
ADDManager ddManager = new ADDManager();

/* Get some variables */
ADD var0 = ddManager.ithVar(0);
ADD var1 = ddManager.ithVar(1);

/* Build sum8: var0 + var1 + 8 */
ADD sum8 = var0.apply((a, b) -> a + b + 8, var1);
var0.recursiveDeref();
var1.recursiveDeref();

/* ... */

/* Release memory */
sum8.recursiveDeref();
ddManager.quit();

If for some reason you want to define operations on internal nodes consider using the apply2 and monadicApply2 methods.

Custom Algebraic Structures with XDDs

The key advantage of the ADD-Lib is its support for your algebraic structure! May it be fuzzy logic or permutation groups that you want as the terminals of your decision diagram – XDDs are the way to go. Define the carrier-set of your algebraic structure as a Java type and implement distinguished elements, monadic/unary operations, and binary operations in a subclass of the XDDManager<T>.

Three-valued Logic with XDDs

For a start let’s consider the three-valued Kleene-Priest Logics. The logic is defined over the carrier-set { TRUE, FALSE, UNKNOWN } with the distinguished one-element TRUE, the zero-element FALSE, and the operations conjunction, disjunction, and negation.

For the ADD-Lib, the three-valued carrier-set is easily defined as an enumeration of its values in Java:

public enum KleenePriestValue {
    TRUE, UNKNOWN, FALSE;
}

The Kleene-Priest Logics forms a Boolean lattice with

The ADD-Lib supports various sorts of algebraic structures including Boolean lattices. To implement decision diagrams over Kleene-Priest Logics you can simply extend the abstract class BooleanLatticeDDManager<T> where T defines the Java type of your carrier-set. In this case we want to extend BooleanLatticeDDManager<KleenePriestValue> and implement the required methods:

public class KleenePriestLogicDDManager extends BooleanLatticeDDManager<KleenePriestValue> {

    /* Inherit all three constructors */

    public KleenePriestLogicDDManager(int numVars, int numVarsZ, int numSlots, int cacheSize, long maxMemory) {
        super(numVars, numVarsZ, numSlots, cacheSize, maxMemory);
    }

    public KleenePriestLogicDDManager(int numVars, int numVarsZ, long maxMemory) {
        super(numVars, numVarsZ, maxMemory);
    }

    public KleenePriestLogicDDManager() {
        super();
    }

    /* Implement required distinguished elements and operations */

    @Override
    protected KleenePriestValue zeroElement() { return FALSE; }

    @Override
    protected KleenePriestValue oneElement() { return TRUE; }

    @Override
    protected KleenePriestValue and(KleenePriestValue left, KleenePriestValue right) {
        if (left == FALSE || right == FALSE) return FALSE;
        else if (left == TRUE && right == TRUE) return TRUE;
        else return UNKNOWN;
    }

    @Override
    protected KleenePriestValue or(KleenePriestValue left, KleenePriestValue right) { ... }

    @Override
    protected KleenePriestValue not(KleenePriestValue x) { ... }
}

Email Classification Example

Now that we have the three-values Kleene-Priest Logics implemented we can use it just like any other decision diagram. For an example let’s consider email classification: for every email in our inbox we want to decide whether the email is urgent, potentially urgent, or not urgent. With Kleene-Priest Logics we express this as the conjunction of necessity criteria:

The following Java code realises the example using our newly implemented Kleene-Priest decision diagrams:

/* Initialize DDManager with default values */
KleenePriestLogicDDManager ddManager = new KleenePriestLogicDDManager();

/* A weak necessary criterion  */
XDD<KleenePriestValue> recent = ddManager.namedVar("recentlyReceived", TRUE, UNKNOWN);

/* A strong necessary criterion */
XDD<KleenePriestValue> addrBook = ddManager.namedVar("senderInAddressBook", TRUE, FALSE);

/* The conjunction of all necessary criteria */
XDD<KleenePriestValue> urgentMail = recent.and(addrBook);
recent.recursiveDeref();
addrBook.recursiveDeref();

/* Using DotViewer to display XDD in a Popup */
DotViewer<XDD<KleenePriestValue>> viewer = new DotViewer<>();
viewer.view(urgentMail,"urgentMail");

/* Release memory */
urgentMail.recursiveDeref();
ddManager.quit();

The DotViewer can be used as shown above and will open the following window:

An Algebraic Decision Diagram utilising Kleene-Priest Logic to classify emails.

Schrödingers Cat (Wigner’s Friend) Example

/* Initialize DDManager with default values */
KleenePriestLogicDDManager ddManager = new KleenePriestLogicDDManager();

/* A strong necessary criterion */
XDD<KleenePriestValue> friendHappy = ddManager.namedVar("friendIsHappy", TRUE, FALSE);

/* A weak necessary criterion  */
XDD<KleenePriestValue> opened = ddManager.namedVar("boxOpened", TRUE, UNKNOWN);

/* The conjunction of all necessary criteria */
XDD<KleenePriestValue> catAlive = opened.and(friendHappy).or(opened.compl());
friendHappy.recursiveDeref();
opened.recursiveDeref();

/* Using DotViewer to display XDD in a Popup */
DotViewer<XDD<KleenePriestValue>> viewer = new DotViewer<>();
viewer.view(catAlive,"CatAlive");

/* Release memory */
catAlive.recursiveDeref();
ddManager.quit();

Other Algebraic Structures

There are various categories of algebraic structures for many of which we have created abstract classes requiring the associated distinguished elements and operations:

If your algebraic structure is none of the above you can always extend the XDDManager directly and override only the distinguished elements and operations you need:

Some Examples

We have some algebraic structures prepared for you and we will add many more in the near future:

If you have implemented your own algebraic structure and you want to share it with other users of the ADD-Lib please contact us.