ban_sdd is a package that implements the Sentential Decision Diagram (SDDs) proposed by Adnan Darwiche and his team at UCLA. This document is not meant to explain the theory of SDDs, the interested reader should look at the references given at the end of this document. SDDs form a family of objects that allows to represent propositional formulas (like BDDs).
For implementation reasons, and despite the garbage collector of Java, a number of objects need to be explicitly collected. These objects (VtreeNode and SDD, described later) are equipped with a counter that records the number of uses of the objects. When an object is created, its counter is set to one; when a new copy of an object is created through one of the methods of the API, its counter is increased by one. When the user no longer needs an object, it is required to decrease its counter by one by using method unwatch().
obj.unwatch();
If that object is used somewhere else, it won't be destroyed because its counter will be above one.One needs to be careful about temporary objects that can be created as a by-product of a complex manipulation. The following code, for instance, introduces a memory leak:
SDD a,b,c;
//
// ... initialising a, b, and c
//
SDD z = a.and(b).and(c);
SDD a,b,c;
// initialising a, b, and c
SDD z;
{
final SDD tmp = a.and(b);
z = tmp.and(c);
z.unwatch();
}
The user needs to be careful to make sure that any copy he makes of an SDD sees its counter increased by one. This can be done using method watch(). For instance, this is the implementation of a method that, in general, could return any SDD. Because the returned object could be a new object, it will later need to be unwatched. In this particular implementation, it is not a new object, but since it will be unwatched in the future, it needs to be watched:
@Override
public SDD getNewSDD(SDD sdd) {
sdd.watch();
return sdd;
}
A way to verify that your code is not leaking is to check the state of the counters when you expect them to be zero. The following methods should not print out anything if there is no SDD and no Vtree being monitored:
sdd.VtreeNode.printBuffer(System.out);
sdd.SDD.printBuffer(System.out);
A vtree is a binary ordered tree defined on the set of variables. A leaf of a vtree is defined by the VtreeLeaf class. A node in the vtree is defined by the VtreeNode class. Both VtreeLeaf and VtreeNode implement the Vtree interface. Do not forget to unwatch the intermediate vtrees.
final sdd.Variable a,b,c;
// ...
final sdd.VtreeLeaf la = sdd.VtreeLeaf.create(a);
final sdd.VtreeLeaf lb = sdd.VtreeLeaf.create(b);
final sdd.VtreeLeaf lc = sdd.VtreeLeaf.create(c);
final sdd.VtreeNode ab = sdd.VtreeNode.create(la,lb);
final sdd.VtreeNode abc = sdd.VtreeNode.create(ab,lc);
la.unwatch();
lb.unwatch();
lc.unwatch();
ab.unwatch();
There are three types of operations that one may want to do with an SDD:
There are several methods to create an SDD. An SDD is always associated with a vtree.
The most basic methods to create an SDD are constant(boolean,Vtree), which creates the SDD representing the specified Boolean constant, and variable(Variable,Vtree), which creates the SDD representing the logical formula where the specified variable evaluates to true and all other variables are free. Together with the manipulation operators described next, these two construction methods are sufficient. At this time, there is no real alternative to these methods, but this is the next action item on the TODO list.
The natural operations on SDD are implemented. It is possible to use the methods and(SDD) and or(SDD), but this requires both SDDs to be defined over the same vtree. The negation is implemented with neg(). The existencial operator and the universal operator, resp. exists(Variable) and forall(Variable), are also available. Finally the last method of interest is replace(Variable,Variable), which assumes that the SDD is independent from the second variable and replace the constraints on the first variable by constraints on the second one.
The questions that can be asked to an SDD are the following ones:
final SDDFunction
final double proba = sdd.apply(f);
The vtree can affect dramatically the size of the SDD, and consequently the performance of any algorithm that uses SDDs. The sdd_package comes with methods to tentatively optimise the vtree.
Remember that operations on several SDDs require these SDD to be defined on the same vtree. Therefore a collection of SDD can only be optimised together.
To optimise a collection of SDDs, first create an Optimisation object through the constructor Optimisation(List<SDD>). The list in parameter is the collection of SDDs to optimise; the order is relevant because their optimised versions will be returned in the same order. Second, calling to the localOptimal() method on the optimisation should trigger the optimisation procedure. Finally, the list of optimised SDDs can be retrieved with getSDDs().
Here is an example:
SDD a, b, c;
//
// ...
//
final List<SDD> toOptimise = new ArrayList<SDD>();
toOptimise.add(a);
toOptimise.add(b);
toOptimise.add(c);
final Optimisation opt = new Optimisation(toOptimise);
opt.localOptimal();
final List<SDD> optimised = opt.getSDDs();
a.unwatch();
a = optimised.get(0);
b.unwatch();
b = optimised.get(1);
c.unwatch();
c = optimised.get(2);
This section targets more advanced users who would like to improve the SDD package (for instance, defining custom vtree operations or optimisation procedures).
The class SDDMemory is used to collect ``known results'' that might be reused later. For instance, as part of a disjunction operation between two SDDs, the conjunction of two specific SDDNode (explained later) might be required several times. The first time that this conjunction is computed, it is stored in the SDDMemory so that any subsequent conjunction call with the same parameters will be quickly solved by a lookup in the SDDMemory object. Most SDD operation create and delete a memory, so that successive calls to the SDD operations will use different memories. Memories need to be explicitely emptied (failure to do so will lead to memory leak).
{
final SDDMemory mem = new SDDMemory();
//
// ... (using the memory)
//
mem.empty();
}
The abstract class SDDTree is the one that represents the data structure inside the SDD. There are three implementations of the SDDTree :
Vtree operations are operations that change the shape of vtrees (but do not change their set of variables) and also adapt the SDDTree according to the new vtree. An example for a vtree operation is the one where the left and right branches of a vtree are swapped.
There are three methods for the VtreeOperation interface:
The package sdd.ope comes with a set of vtree operations that make it possible to change any vtree in any other vtree (that share the same set of variables):
The methods for optimisation are not currently designed to easily plug-in custom optimisation operations. The plan will be to improve this aspect in the future.
The two important classes that the optimisation uses are
This work is based on the theory of SDDs developed by Adnan Darwiche's team from UCLA. The best resource on UCLA is its webpage, which also contains a C library of SDD:
This lists the features that I am hoping to add to the SDD package in the future.