A Canonical Generalization of OBDD

There is a branch of computer science (close to SAT/constraints solving communities) studying data structures allowing to represent Boolean functions succinctly yet in a way that allows you to do something with it. Like, quickly finding how many models you have where x1=true and x2=false. Of course, if you list every model, that is easy, but not succinct. So we are looking to tradeoff between succinctness and tractability.

OBDDs are one of the earliest such data structure. You can see it in many different ways depending on your taste/background (automata for finite language, decision-trees with sharing, flowcharts, nested if-then-else...), but they are a very natural way of representing a Boolean function. Plus, they have nice properties. One of them being that you can take any OBDD and minimize it in linear time into a canonical form, that is, a given Boolean function has exactly one minimal canonical OBDD (like every regular language have a canonical minimal DFA, this is actually the same result).

The problem with OBDD is that they are not the most succinct-yet-tractable thing you can come up with and Knowledge Compilation has studied many interesting, more succinct, generalization of them. But almost all such generalizations loose the canonicity, that is, there is no way of naturally definining a minimal and unique representation of the Boolean function with these data structures. Nor any way of "minimizing" them. You get better succinctness but you also loose somewhere else.

There is SDD which are also canonical in some sense but the canonical version may be way bigger than the smallest SDD, which is not satisfactory (though they are interesting in practice).

TDD, introduced in this paper, give such a generalization of OBDD, where you can minimize it toward a canonical form. The idea is to go from "testing along a path" to "testing along a tree" which allows to compute more compact circuits. For example, one big limitation of OBDD is that they cannot efficiently represent Cartesian product, that is, function of the form f(X,Y) = f1(X) AND f2(Y) with X and Y disjoint. You can do this kind of things with TDDs.

That said, they are less succinct than SDDs or other generalizations, so canonicity is not free. The main advantage of having canonicity and minimization is to unlock the following algorithm (used in practice for OBDD) to transform a CNF formula (the standard input of SAT solver) into a TDD:

Let F = C1 AND ...AND Cn where each Ci is a clause: - Build a small TDD Ti for each Ci (that is not too hard, clauses are just disjunction of variables or negated variables) - Combine T1 and T2 into a new TDD T' and minimize. - Iteratively combine T' with T3 ... Tn and minimize at each step.

In the end, you have a TDD computing F. The fact that you can minimize at each step helps the search space to stay reasonable (it will blow up though, we are solving something way harder than SAT) and it may give you interesting practical performances.

We (well mainly Guy, if he's around) are working on an implementation, which will be made open source at some point (still rounding the edges a bit). We have very encouraging preliminary results, it does compare well wrt SDD and CUDD. There is still some ideas we would like to try, specifically for model counting.