A Canonical Generalization of OBDD(arxiv.org)
arxiv.org
A Canonical Generalization of OBDD
https://arxiv.org/abs/2604.05537
14 comments
When I was writing biochemistry papers, it was a rule that you had to introduce the full spelling of a phrase along with the first use of its acronym in the full text. Is that not a thing anymore? This abstract reads like something out of a deep immunology subfield, and the first few paragraphs of the introduction didn’t help me out much either.
Well that is the norm if you use acronyms that are not well-known for the target audience. The paper you see is a submission to the SAT'26 conference, a conference dedicated to the problem SAT and related questions. For most people there, especially the ones interested in this paper, OBDD (Ordered Binary Decision Diagrams), FPT (Fixed Parameter Tractable), DNNF (Decomposable Negation Normal Form) and CNF (Conjunctive Normal Form) are pretty standard acronyms and you do not redefine them in every paper. Plus, conference format forces you to fit everything in a bounded number of pages, so you have to choose where to save space.
That said, Knowledge Compilation is one of the worst subfield of computer science regarding acronyms, so I understand your feeling...
That said, Knowledge Compilation is one of the worst subfield of computer science regarding acronyms, so I understand your feeling...
Makes sense, and thank you for the expansions! Makes it easier to look them up
Can someone give a quick explanation of why this is important? It looks interesting but that it would take a lot of background to really understand it.
Hey, author here, so clearly I'm biased.
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.
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.
Thanks, I'll have to take your word that this TDD minimization is useful in practice, the way SAT solvers are useful despite SAT being NP-hard. The general problem of Boolean function minimization is of course horrendously intractable; as you say, way harder than SAT.
How does this relate to OTDDs - Ternary Decision Diagrams?
I did not know about Ternary Decision Diagrams, sorry for the name clash. I had a look. You can always reencode Ternary Decision Diagrams into Binary ones by just encoding variable x with two bits x^1 and x^2, so Ordered Ternary Decision Diagrams are the same (modulo encoding) as OBDD, hence less succinct that our Tree Decision Diagrams. If you consider Read-Once Ternary Decision Diagrams, then you get something roughly equivalent to FBDD (modulo encoding). So this is incomparable with our TreeDD (that is, some functions are easy for TreeDD and hard for RO-TernaryDD like a low treewidth/high pathwidth CNF formula and some functions are easy for RO-TernaryDD and hard for TreeDD ; take anything separating FBDD from OBDD for example).
Positively surprised to see stuff like these on HN first page!
If any author is around, do you have an implementation that can be compared with CUDD and similar BDD libraries?
If any author is around, do you have an implementation that can be compared with CUDD and similar BDD libraries?
Hi, author here! Also positively surprised to see this on HN haha
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.
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.