The `ban_sdd` Package

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).

A Word on Memory

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);

This code should be replaced by the following one:

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);

vtrees

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();

It is possible to navigate through a vtree by using the VtreeNode methods getLeft() and getRight().

SDDs

There are three types of operations that one may want to do with an SDD:

create the SDD;
manipulate the SDD;
ask questions about the SDD.

Create 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.

Manipulate the SDD

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.

Ask questions about the SDD

The questions that can be asked to an SDD are the following ones:

getOneAssignment() returns an assignment of the variables that is consistent with the SDD.
isValid() indicates whether the SDD is equivalent to true.
isSat() indicates whether the SDD is satisfiable, i.e., whether it differs from false.
nbModels() computes the number of satisfying models of the SDD.
apply(SDDFunction) allows to apply general functions, such as the one computing the probability of an SDD to evaluate to true given an a priori probability for each variable to evaluate to true:
final SDDFunction f = new SDDProbabilityFunction(aprioriProba));
final double proba = sdd.apply(f);

Optimisation

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);

Advanced Users

This section targets more advanced users who would like to improve the SDD package (for instance, defining custom vtree operations or optimisation procedures).

SDDMemory

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();
}

SDDTree

The abstract class SDDTree is the one that represents the data structure inside the SDD. There are three implementations of the SDDTree :

SDDConstant, which represents either the true or false value
SDDVariable, which represents a literal
SDDTreeDisjunction, which represents a more complex node.

A SDDTree object does not have an explicit reference to the vtree, but the vtree is explicit from the outside. The SDDTree is an SDDVariable object if and only if the vtree is a leaf. Otherwise, it is an SDDTreeDisjunction except if it can be replaced by an SDDConstant (in which case it always is). An SDDTreeDisjunction is defined as a set of SDDTreeConjunction objects, which are pairs of SDDTrees called the prime and the sub. If an SDDTreeDisjunction is defined on a vtree node, its primes (the primes of its SDDTreeConjunctions) are defined on the left vtree and its subs on the right vtree. They also have the property that

the disjunction of all the primes is logically equivalent to true;
no two subs are logically equivalent (or == equivalent, for that matter).

The class SDDTrees contains many (static) methods that implement the core methods on SDDs (such as conjunction, disjunction, etc.).

Vtree Operations

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:

isApplicable(Vtree) indicates whether the operation is applicable on the specified vtree. For instance, the swap operation is not possible on tree leaves.
apply(Vtree) returns the new vtree after the application of the vtree operation.
applyToSDD(SDDTree,SDDMemory) returns the SDDTree equivalent to the specified one, but that matches the vtree obtained after applying this vtree operation on the vtree that the specified SDDTree is defined on.

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):

Swap is the operation that replaces a vtree of the form (A,B) with the vtree of the form (B,A).
LeftRotation is the operation that replaces a vtree of the form ((A,B),C) with the vtree of the form (A,(B,C)).
RightRotation is the operation that replaces a vtree of the form (A,(B,C)) with the vtree of the form ((A,B),C).
Identity is the operation that leaves the vtree unchanged.
ChildrenOperation is the operation, defined on top of two operations O1 and O2 and that replaces a vtree of the form (A,B) with the vtree of the form (O1(A),O2(B)).
ConsecutiveOperations is the operation, defined on top of a sequence of operations O1,. . .,On that replaces a vtree of the form A with the vtree of the form O1 ∘ On(A).

Optimisation Procedures

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

OptimisationProblem which is essentially a set of SDDTree objects defined over a vtree that we want to optimise.
OptimisationReport which is essentially a vtree operation that maps each original SDDTree object to their new representation. An optimisation report also implicitely represents a new optimisation problem.

References

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:

Road Map

This lists the features that I am hoping to add to the SDD package in the future.

Save/load SDD files.
CNF reading capabilities.
An extra layer that deals with the vtree optimisation without implicit calls from the user.
More optimisation tuning.

The ban_sdd Package