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
- auto-referencing for newly created decision diagrams,
- type safety for BDDs, ADDs, and ZDDs, and
- XDDs to allow users to use custom algebraic structures.
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
- a zero element
zeroElement
, - a one element
oneElement
, - conjunction
and
, - disjunction
or
, and - negation
not
.
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 email was received recently (if this is not the case we are unsure about whether or not to consider the email urgent)
- the email sender is listed in our address book.
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:
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:
- For group-like algebraic structures
- Groups
GroupDDManager
- Magmas
MagmaDDManager
- Monoids
MonoidDDManager
- Groups
- For ring-like algebraic structures
- Fields
FieldDDManager
- Rings
RingDDManager
- Semirings
SemiringDDManager
- Fields
- For lattices
- Boolean lattices
BooleanLatticeDDManager
- Bounded lattices
BoundedLatticeDDManager
- Complementable lattices
ComplementedLatticeDDManager
- Complete lattices
CompleteLatticeDDManager
- Powerset lattices
PowerSetLatticeDDManager
- Boolean lattices
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:
- Distinguished elements: neutral element
neutralElement
, least elementleastElement
, greatest elementgreatestElement
zero elementzeroElement
, and one elementoneElement
. - Monadic/unary operations: inverse element
inverse
, complementcompl
, negationnot
, multiplicative inversemultInverse
, and additive inverseaddInverse
. - Binary operations: meet
meet
, infimuminf
, intersectionintersect
, conjunctionand
, multiplicationmult
, joinjoin
, supremumsup
, unionunion
, disjunctionor
, and additionadd
.
Some Examples
We have some algebraic structures prepared for you and we will add many more in the near future:
- Group-like algebraic structures
- Permutation group (
PermutationGroupDDManager
) - String monoid (
StringMonoidDDManager
)
- Permutation group (
- Ring-like algebraic structures
- Square matrix ring (
SquareMatrixRingDDManager
)
- Square matrix ring (
- Lattices
- Cartesian Boolean logic (
BNLogicDDManager
) - Power set lattice (
ComplementableSetLatticeDDManager
) - Kleene-Priest logic (
KleenePriestLogicDDManager
) - Partition lattice (
PartitionLatticeDDManager
)
- Cartesian Boolean logic (
If you have implemented your own algebraic structure and you want to share it with other users of the ADD-Lib please contact us.