SDD: A New Canonical Representation of Propositional Knowledge Bases

1 Introduction

Many areas of computer science have shown a great interest in tractable and canonical representations of propositional knowledge bases (aka, Boolean functions). The Ordered Binary Decision Diagram (OBDD) is one example representation that received much attention and proved quite influential in a variety of areas [Bryant, 1986]. Reduced OBDDs are canonical and can be combined using any Boolean operator in polytime, making them an indispensable tool in many research areas such as diagnosis, verification, system design, and planning.

Within AI, the study of tractable representations has become more systematic since [Darwiche and Marquis, 2002], which showed that many known representations of propositional knowledge bases are subsets of Negation Normal Form (NNF), and correspond to imposing specific properties on NNF. The most fundamental of these properties are decomposability and determinism, which lead to d-DNNF representations that proved influential in probabilistic reasoning applications (e.g., [Chavira and Darwiche, 2008]). Interestingly enough, OBDDs satisfy these two properties, but they also satisfy additional properties, making them a strict subset of d-DNNFs.

A fundamental concept highlighted by [Darwiche and Marquis, 2002] is the tension between the succinctness and tractability of a given representation. Here, succinctness refers to the size of a knowledge base once it is compiled into the representation, while tractability refers to the set of operations that have polytime implementations on the given representation. As one would expect, the more tractable a representation is, the less succinct it tends to be. Hence, in principle, one should first identify the operations needed by a certain application, and then use the most succinct representation that provides polytime support for those operations.

The practice can be a bit different, however, for two reasons. First, some operations may not be strictly needed for certain applications, yet they can significantly facilitate the development of software systems for those applications. For example, the ability to combine compilations efficiently using Boolean operators, such as conjoin, disjoin and negate, has proven to be quite valuable in system development. Moreover, the canonicity of a representation can be a critical factor when adopting a representation as it facilitates the search for optimal compilations. For example, the canonicity of OBDDs allows one to reduce the process of searching for an optimal compilation (OBDD) into one of identifying an optimal variable order (a reduced OBDD is completely determined by the used variable order). Hence, in practice, one may adopt a less succinct representation than one can afford, motivated by canonicity and the ability to perform Boolean combinations in polytime. This compromise is quite characteristic of many applications in which OBDDs are used (despite the availability of more succinct representations).

This paper is motivated by these practical considerations, where the goal is to identify a tractable representation that lies between d-DNNF and OBDD in terms of generality, yet maintains the properties that make OBDDs quite attractive in practical system development. In particular, we propose a new representation of propositional knowledge bases, called SDD, which results from imposing two properties on NNF that have been recently introduced: structured decomposability and strong determinism. These properties are stronger than decomposability and determinism which characterize d-DNNF, making SDDs a strict subset of d-DNNFs. On the other hand, these properties are weaker than the ones satisfied by OBDDs, making SDDs a strict superset of OBDDs.

Despite their generality, SDDs maintain the key properties of OBDDs, including canonicity and a polytime support for Boolean combinations. They also come with a tighter bound on their size in terms of treewidth.

The SDD is inspired by two recent discoveries. The first is structured decomposability [Pipatsrisawat and Darwiche, 2008], which is based on the notion of vtrees that generalize variable orders. The second is strongly deterministic decompositions [Pipatsrisawat and Darwiche, 2010a], which generalize the Shannon decomposition on which OBDDs are based. Combining vtrees and this class of decompositions leads to the new representation. The foundations of SDDs are presented in Section 2; their syntax and semantics in Section 3; their canonicity in Section 4; their Boolean combination in Section 5; their relation to OBDDs in Section 6; and their upper bound based on treewidth in Section 7. Preliminary empirical results and a discussion of related work appear in Section 8. We will provide proofs or proof sketches for many of our results in this paper, leaving some to the full technical report.

2 Strongly deterministic decompositions

We start with some technical and notational preliminaries. Upper case letters (e.g., X) will be used to denote variables and lower case letters to denote their instantiations (e.g., x). Bold upper case letters (e.g., X) will be used to denote sets of variables and bold lower case letters to denote their instantiations (e.g., x).

A Boolean function f over variables Z maps each instantiation z to 0 or 1. The conditioning of f on instantiation x, written f|x, is a subfunction that results from setting variables X to their values in x. A function f essentially depends on variable X iff f|X ̸=f|¬X. We write f(Z) to mean that f can only essentially depend on variables in Z. A trivial function maps all its inputs to 0 (denoted false) or maps them all to 1 (denoted true).

Consider a Boolean function f(X, Y) with non-overlapping variables X and Y. If f = (p1(X) ∧ s1(Y)) ∨ . . . ∨ (pn(X) ∧ sn(Y)), then {(p1, s1), . . . , (pn, sn)} is called an (X, Y)- decomposition of function f as it allows one to express f in terms of functions on X and on Y only [Pipatsrisawat and Darwiche, 2010a]. If pi∧pj = false for i ̸=j, the decomposition is said to be strongly deterministic on X [Pipatsrisawat and Darwiche, 2010a]. In this case, we call each ordered pair (pi, si) an element of the decomposition, each pi a prime and each si a sub. The decomposition size is the number of its elements.

SDDs utilize a more structured decomposition type.

Definition 1 Let α = {(p1, s1), . . . , (pn, sn)} be an (X, Y)-decomposition of function f that is strongly deterministic on X. Then α is called an X-partition of f iff its primes form a partition (each prime is consistent, every pair of distinct primes are mutually exclusive, and the disjunction of all primes is valid). Moreover, α is compressed iff its subs are distinct (si ̸= sj for i ̸=j).

Consider decompositions {(A,B), (¬A, false)} and {(A,B)} of f = A ∧ B. The first is an A-partition. The second is not. Decompositions {(true,B)} and {(A, B), (¬A, B)} are both A-partitions of f = B. The first is compressed. The second is not since its subs are not distinct. A decomposition is compressed by repeated replacement of elements (p, s) and (q, s) with (p ∨ q, s).

Following are useful observations about X-partitions. First, false can never be prime by definition. Second, if true is prime, then it is the only prime. Third, primes determine subs. Hence, if two X-partitions of a function f are distinct, their primes must form different partitions.

Ordered Binary Decision Diagrams (OBDDs) are based on the Shannon decomposition of a function f, {(X, f |X), (¬X, f |¬X)}, which is an X-partition of f . Here, decisions are binary since they are based on the value of literal primes (X or ¬X). On the other hand, Sentential Decision Diagrams (SDDs) are based on Xpartitions, where X is a set of variables instead of being a single variable. As a result, decisions are not binary as they are based on the value of sentential primes.

The following property of partitioned decompositions is responsible for many properties of SDDs.

Theorem 2 Let ◦ be a Boolean operator and let {(p1, s1), . . . , (pn, sn)} and {(q1, r1), . . . , (qm, rm)} be X-partitions of f(X, Y) and g(X, Y). Then {(pi ∧ qj , si◦ rj) | pi ∧ qj ̸= false} is an X-partition of f ◦g.

Proof Since p1, . . . , pn and q1, . . . , qm are partitions, then pi ∧ qj is also a partition for i = 1, . . . , n, j = 1, . . . ,mand pi∧pj ̸= false. Hence, the given decomposition is an X-partition of some function. Consider now an instantiation xy of variables XY. There must exist a unique i and a unique j such that x |= pi and y |= qj. Moreover, f(xy) = si(y), g(xy) = rj(y) and, hence, [f ◦g](xy) = si(y)◦rj(y). Evaluating the given decomposition at instantiation xy also gives si(y)◦rj(y). □

According to Theorem 2, the X-partition of f ◦g has size O(nm), where n and m are the sizes of X-partitions for f and g. This is the basis for a future combination operation on SDDs that has a similar complexity.

Let f = A ∨ B, g = A ∧ B and consider the corresponding A-partitions {(A, true), (¬A,B)} and {(A,B), (¬A, false)}. The following is an A-partition for f⊕g: {(A, true⊕B), (¬A, B⊕false)} which equals {(A, ¬B), (¬A, B)}.

Let f = A ∨ C , g = B ∨ C and consider the corresponding {A,B}-partitions {(A, true), (¬A,C)} and {(B, true), (¬B,C)}. Theorem 2 gives {(A ∧ B, true), (A ∧ ¬B, true), (¬A ∧ B, true), (¬A ∧ ¬B,C)} as an {A,B}-partition for f ∨ g. This is not compressed since its subs are not distinct. We compress it by simply disjoining the primes of equal subs, leading to {(A ∨ B, true), (¬A ∧ ¬B, C)}.

The canonicity of SDDs is due to the following result.

Theorem 3 A function f(X, Y) has exactly one compressed X-partition.

Proof Let x1, . . . , xk be all instantiations of variables X. Then {(x1, f|x1), . . . , (xk, f|xk)} is an Xpartition of function f. Let s1, . . . , sn be the distinct subfunctions in f|x1, . . . , f|xk. For each si, define pi = ∨f|xj=si xj. Then α = {(p1, s1), . . . , (pn, sn)} is a compressed X-partition of f. Suppose that β = {(q1, r1), . . . , (qm, rm)} is another compressed Xpartition of f. Then α and β must have different partitions. Moreover, there must exist a prime pi of α that overlaps with two different primes qj and qk of β. That is, x |= pi, qj and x′ |= pi, qk for some instantiations x ̸=x′ . We have f|x = α|x = si = rj = β|x and f |x′ = α|x′ = si = rk = β|x′ . Hence, rj = rk. This is impossible as β is compressed. □

Let α = {(p1, s1), . . . , (pn, sn)} be an X-partition for function f. Then β = {(p1, ¬s1), . . . , (pn, ¬sn)} is an X-partition for its negation ¬f. This follows from Theorem 2 while noticing that ¬f = f ⊕ true. Moreover, if α is compressed, then β must be compressed as well. Consider function f = A ∨ B and A-partition {(A, true), (¬A,B)}. Then {(A, false), (¬A, ¬B)} is an A-partition of function ¬f = ¬A ∧ ¬B.

Following is the second key notion underlying SDDs.

Definition 4 A vtree for variables X is a full binary tree whose leaves are in one-to-one correspondence with the variables in X.

Figure 1(a) depicts a vtree for variables A, B, C and D. As is customary, we will often not distinguish between node v and the subtree rooted at v, referring to v as both a node and a subtree. Moreover, vl and vr denote the left and right children of node v.

The vtree was originally introduced in [Pipatsrisawat and Darwiche, 2008], but without making a distinction between left and right children of a node. In this paper, the distinction is quite important for the following reason. We will use a vtree to recursively decompose a Boolean function f, starting at the root of a vtree. Consider node v = 6 in Figure 1(a) which is root. The left subtree contains variables X = {A,B} and the right subtree contains Y = {C,D}. Decomposing function f at this node amounts to generating an X-partition of function f. The result is quite different from generating a Y-partition of the function. The SDD representation we shall present next is based on a recursive application of this decomposition technique. In particular, if {(p1, s1), . . . , (pn, sn)} is the decomposition of function f at node v = 6, then each prime pi will be further decomposed at node vl = 2 and each sub si will be further decomposed at node vr = 5. The process continues until we have constants or literals.

The formal definition of SDDs is given next, after one more comment about vtrees. Each vtree induces a total variable order that is obtained from a left-right traversal of the vtree. The vtree in Figure 1(a) induces the total variable order 〈B,A,D,C〉. We will have more to say about these total orders when we discuss the relationship between SDDs and OBDDs.

3 The syntax and semantics of SDDs

We will use 〈.〉 to denote a mapping from SDDs into Boolean functions. This is needed for semantics.

Definition 5 α is an SDD that respects vtree v iff:

• α = ⊥ or α = ⊤. Semantics: 〈⊥〉 = false and 〈⊤〉 = true.
• α = X or α = ¬X and v is a leaf with variable X. Semantics: 〈X〉 = X and 〈¬X〉 = ¬X.
• α = {(p1, s1), . . . , (pn, sn)}, v is internal, p1, . . . , pn are SDDs that respect subtrees of vl , s1, . . . , sn are SDDs that respect subtrees of vr , and 〈p1〉, . . . , 〈pn〉 is a partition.

Semantics: 〈α〉 = ∨ni=1 〈pi〉 ∧ 〈si〉.

The size of SDD α, denoted |α|, is obtained by summing the sizes of all its decompositions.

A constant or literal SDD is called terminal. Otherwise, it is called a decomposition. An SDD may respect multiple vtree nodes. Consider the vtree in Figure 1(a). The SDD {(⊤, C)} respects nodes v = 5 and v = 6. However, if an SDD respects node v, it will only mention variables in subtree v.

For SDDs α and β, we will write α = β to mean that they are syntactically equal. We will write α ≡ β to mean that they represent the same Boolean function: 〈α〉 = 〈β〉. It is possible to have α ≡ β and α ̸=β: α = {(X, γ), (¬X, γ)} and β = {(⊤, γ)} is one such example. However, if α = β, then α ≡ β by definition. We will later provide further conditions on SDDs which guarantee α = β iff α ≡ β (i.e., canonicity).

SDDs will be notated graphically as in Figure 1(b), according to the following conventions. A decomposition is represented by a circle with outgoing edges pointing to its elements (numbers in circles will be explained later). An element is represented by a paired box p s , where the left box represents the prime and the right box represents the sub. A box will either contain a terminal SDD or point to a decomposition SDD. The top level decomposition in Figure 1(b) has three elements with primes representing A ∧ B, ¬A ∧ B, ¬B and corresponding subs representing true, C, and C ∧D. Our graphical depiction of SDDs, which also corresponds to how they are represented in computer memory, will ensure that distinct nodes correspond to syntactically distinct SDDs (i.e., ̸=). This is easily accomplished using the unique-node technique from the OBDD literature; see, e.g., [Meinel and Theobald, 1998].

If one adjusts for notation, by replacing circle-nodes with or-nodes, and paired-boxes with and-nodes, one obtains a structured DNNF [Pipatsrisawat and Darwiche, 2008] that satisfies strong determinism [Pipatsrisawat and Darwiche, 2010a]. The SDD has more structure, however, since its decompositions are not only strongly deterministic, but also partitioned (see Definition 1).

4 Canonicity of SDDs

We now address the canonicity of SDDs. We will first state two key definitions and assert some lemmas about them (without proof). We will then use these lemmas in proving our main canonicity theorem.

Definition 6 A Boolean function f essentially depends on vtree node v if f is not trivial and if v is a deepest node that includes all variables that f essentially depends on.

By definition, a trivial function does not essentially depend on any vtree node.

Lemma 7 A non-trivial function essentially depends on exactly one vtree node.

Definition 8 An SDD is compressed iff for all decompositions {(p1, s1), . . . , (pn, sn)} in the SDD, si ̸≡ sj when i ̸=j. It is trimmed iff it does not have decompositions of the form {(⊤, α)} or {(α, ⊤), (¬α, ⊥)}.

An SDD is trimmed by traversing it bottom up, replacing decompositions {(⊤, α)} and {(α, ⊤), (¬α, ⊥)} with α.

Lemma 9 Let α be a compressed and trimmed SDD. If α ≡ false, then α = ⊥. If α ≡ true, then α = ⊤. Otherwise, there is a unique vtree node v that SDD α respects, which is the unique node that function 〈α〉 essentially depends on.

Hence, two equivalent SDDs that are compressed and trimmed respect the same, unique vtree node (assuming the SDDs are not equal to ⊥ or ⊤). This also implies that SDDs which are not equal to ⊥ or ⊤ can be grouped into equivalence classes, depending on the unique vtree node they respect. The SDD in Figure 1(b) is compressed and trimmed. Each of its decomposition nodes is labeled with the unique vtree node it respects.

Theorem 10 Let α and β be compressed and trimmed SDDs respecting nodes in the same vtree. Then α ≡ β iff α = β.

Proof If α = β, then α ≡ β by definition. Suppose α ≡ β and let f = 〈α〉 = 〈β〉. We will next show that α = β, while utilizing Lemmas 7 and 9. If f = false, then α = β = ⊥. If f = true, then α = β = ⊤. Suppose now that f is not trivial and essentially depends on vtree node v, which must be unique. SDDs α and β must both respect Algorithm 1 Apply(α, β, ◦) : α and β are SDDs normalized for the same vtree node and ◦ is a Boolean operator.

Cache(., ., .) = nil initially. Expand(γ) returns {(⊤, ⊤)} if γ = ⊤; {(⊤, ⊥)} if γ = ⊥; else γ. UniqueD(γ) returns ⊤ if γ = {(⊤, ⊤)}; ⊥ if γ = {(⊤, ⊥)}; else the unique SDD with elements γ. 1: if α and β are constants or literals then 2: return α◦β {must be a constant or literal} 3: else if Cache(α, β, ◦) ̸= nil then 4: return Cache(α, β, ◦) 5: else 6: γ←{} 7: for all elements (pi, si) in Expand(α) do 8: for all elements (qj, rj) in Expand(β) do 9: p←Apply(pi, qj , ∧) 10: if p is consistent then 11: s←Apply(si, rj , ◦) 12: add element (p, s) to γ 13: end if 14: end for 15: end for 16: end if 17: return Cache(α, β, ◦)←UniqueD(γ)

this unique node v. The proof continues by induction on node v.

Suppose node v is a leaf. Only terminal SDDs respect leaf nodes, yet α and β cannot be ⊥ or ⊤ by assumption. Hence, α and β must be literals. Since α ≡ β, they must be equal literals, α = β. Suppose now that node v is internal and that the theorem holds for SDDs that respect descendants of v. Let X be the variables in subtree vl , Y be the variables in subtree vr , α = {(p1, s1), . . . , (pn, sn)} and β = {(q1, r1), . . . , (qm, rm)}. By definition of an SDD, primes pi and qi respect nodes in subtree vl and can only mention variables in X. Similarly, subs si and ri respect nodes in subtree vr and can only mention variables in Y. Hence, {(〈p1〉, 〈s1〉), . . . , (〈pn〉, 〈sn〉)} and {(〈q1〉, 〈r1〉), . . . , (〈qn〉, 〈rn〉)} are both X-partitions of function f . They are also compressed by assumption. By Theorem 3, the decompositions must be equal. That is, n = m and there is a one-to-one ≡-correspondence between their primes and between their subs. By the induction hypothesis, there is a one-to-one =-correspondence between their primes and their subs. This implies α = β. □

5 The Apply operation for SDDs

If one looks carefully into the proof of canonicity, one finds that it depends on two key properties beyond compression. First, that trivial SDDs ⊥ and ⊤ are the only ones that represent trivial functions. Second, that nontrivial SDDs respect unique vtree nodes, which depend on the functions they represent. Although trimming gives us both of these properties, one can also attain them using alternative conditions. For example, the first property can be ensured using only light trimming: excluding decompositions of the form {(⊤, ⊤)} or {(⊤, ⊥)} by replacing them with ⊤ and ⊥. The second property can be ensured by normalization. If α is a decomposition that respects node v, normalization requires that its primes respect vl and its subs respect vr (instead of respecting subtrees in vl and vr ; see Definition 5). Figure 2 depicts a normalized SDD of the one in Figure 1(b). Note how C was replaced by {(⊤, C)} and ¬B by {(¬B, ⊤), (B, ⊥)} in the normalized SDD.

A Boolean function has a unique SDD that is compressed, lightly trimmed and normalized for a given vtree node. Even though normalization and light trimming lead to SDDs that are redundant compared to trimmed SDDs, the difference in size is only linear in the number of vtree nodes. Moreover, working with normalized SDDs can be very convenient as we shall see next.

Given SDDs α and β that are lightly trimmed and normalized for the same vtree node, and given any Boolean operator ◦, Algorithm 1 provides pseudocode for the function Apply(α, β, ◦), which returns an SDD with the same properties for the function 〈α〉◦〈β〉 and in O(|α||β|) time. The correctness of Algorithm 1 follows from Theorem 2 and a simple induction argument. Its time complexity follows using an argument similar to the one showing the complexity of Apply for OBDDs. 1

The simplicity of Algorithm 1 is due to normalization, which guarantees that the operands of every recursive call are normalized for the same vtree node if neither is trivial. The same function for trimmed SDDs will have to consider four cases depending on the relationship between the vtree nodes respected by its operands (i.e., equal, left descendant, right descendant, and neither).

Given Apply, two SDDs can be conjoined or disjoined in polytime. This also implies that an SDD can be negated in polytime by doing an exclusive-or with ⊤. This is similar to the Apply function for OBDDs, which is largely responsible for their widespread applicability. Using Apply, one can convert a CNF to an SDD by first converting each of its clauses into an SDD (which can be done easily) and then conjoining the resulting SDDs.

1 The consistency test on Line 10 can be implemented in linear (even constant) time since SDDs are DNNFs.

Similarly, one can convert a DNF into an SDD by disjoining the SDDs corresponding to its terms.

The SDD returned by Apply(α, β, ◦) is not guaranteed to be compressed even if the input SDDs α and β are compressed. In a compressed SDD, the subs of every decomposition must be distinct. This is potentially violated on Line 12 as the computed sub s may already exist in γ. One can easily modify Apply so it returns a compressed SDD. In particular, when adding element (p, s) on Line 12, if an element (q, s) already exists in γ, simply replace it with (Apply(p, q, ∨), s) instead of adding (p, s). 2 The augmented version of Apply has proved harder to analyze though since the additional recursive call involves SDDs that may not be part of the input SDDs α and β. In our implementation, however, compression has proved critical for the efficiency of Apply. We have identified strong properties of the additional recursive call Apply(p, q, ∨), but do not yet have a characterization of the complexity of Apply with compression. We will, however, provide in Section 7 an upper bound on the size of compressed SDDs.

6 Every OBDD is an SDD

A vtree is said to be right-linear if each left-child is a leaf. The vtree in Figure 3(a) is right-linear. The compressed and trimmed SDD in Figure 3(b) respects this right-linear vtree. Every decomposition in this SDD has the form {(X, α), (¬X, β)}, which is a Shannon decomposition. This is not a coincidence as it holds for every compressed and trimmed SDDs that respects a rightlinear vtree. In fact, such SDDs correspond to reduced OBDDs in a precise sense; see Figure 3(c). In particular, consider a reduced OBDD that is based on the total variable order induced by the given right-linear vtree. Then every decomposition in the SDD corresponds to a decision node in the OBDD and every decision node in the OBDD corresponds to a decomposition or literal in the SDD. In a reduced OBDD, a literal is represented by a decision node with 0 and 1 as its children (e.g., the literal D in Figure 3(c)). However, in a compressed and trimmed SDD, a literal is represented by a terminal SDD (e.g., the literal D in Figure 3(b)).

2 Line 10 can be replaced with p ̸= ⊥ in this case.

7 An upper bound on SDDs

Consider the vtree in Figure 4(b) and node v = 8. Variable A is an ancestor's left child of node v and will be called an ALC variable of v. Variable B is also an ALC of v. Consider now the CNF in Figure 4(a). If we condition the CNF on the ALC variables of v = 8, the simplified CNF will decompose into independent components, one over variables in vl = 4 and the other over variables in vr = 7. For example, if we condition on A, ¬B, the first component will be C ∨ D and the second component will be F. When a function f(X, Y) decomposes into independent components over variables X and Y, it can be written as f = (∃Xf) ∧ (∃Yf), where ∃Xf is the Y-component and ∃Yf is the X-component. This motivates the following definition, identified in [Pipatsrisawat and Darwiche, 2010b].

Definition 11 Let f be a Boolean function. A vtree for function f is nice if for each internal node v in the vtree, either vl is a leaf or f|z = ∃X(f |z) ∧ ∃Y(f |z), where X are the variables of vr , Y are the variables of vl and Z are the ALC variables of node v. The width of node v is the number of distinct sub-functions f|z. The width of the nice vtree is the maximum width of any node.

The vtree in Figure 4 is nice for the CNF in that figure, since the left child of every internal node is leaf, except for node v = 8 which satisfies the second condition of a nice vtree. Nicety comes with the following guarantee.

Theorem 12 Let f be a Boolean function and v be a nice vtree with width w. There is a compressed and trimmed SDD for function f with size O(nw), where n is the number of variables in the vtree.

Proof Algorithm 2 computes such an SDD. In particular, the call sdd(f, v, true) returns two compressed and trimmed SDDs α, β such that 〈α〉 = f and 〈β〉 = ¬f . The correctness of the algorithm can be shown by induction on node v, using the properties of nice vtrees Algorithm 2 sdd(f, v, z) : f is a Boolean function, v is a nice vtree and z is a variable instantiation.

UniqueD(γ) removes an element from γ if its prime is ⊥. It then returns s if γ = {(p1, s), (p2, s)} or γ = {(⊤, s)}; p1 if γ ={(p1, ⊤), (p2, ⊥)}; else the unique decomposition with elements γ.

1: if v is a leaf node then 2: return α, β: terminal SDDs, 〈α〉 = f and 〈β〉 = ¬f 3: else if vl is a leaf node with variable X then 4: s1, ¬s1←sdd(f |X, vr , zX) 5: s2, ¬s2←sdd(f |¬X, vr , z¬X) 6: return UniqueD{(X, s1), (¬X, s2)}, 7: UniqueD{(X, ¬s1), (¬X, ¬s2)} 8: else 9: g←∃Xf, where X are the variables of vr 10: h←∃Yf, where Y are the variables of vl 11: p, ¬p←sdd(g, vl , z) 12: s, ¬s←sdd(h, vr , z) 13: return UniqueD{(p, s), (¬p, ⊥)}, 14: UniqueD{(p, ¬s), (¬p, ⊤)} 15: end if

and the observations made after Theorem 2 about negation. The use of UniqueD guarantees that the returned SDDs are compressed and trimmed. Note that compression here is easy since primes are always terminal SDDs. One can show by induction that every recursive call sdd(f⋆, v⋆, z) is such that Z are the ALC variables of node v⋆ and f⋆ = ∃W(f|z), where W are all other variables outside node v. Hence, the number of distinct recursive calls for node v⋆ is no more than the number of distinct subfunctions f|z, which is the width of node v⋆. Moreover, for each distinct recursive call, the algorithm constructs at most two decompositions, each of size at most two. Since the number of vtree nodes is O(n), the size of constructed SDDs is O(nw). □

If the function f is in CNF, and with appropriate caching, Algorithm 2 can be adjusted so it runs in O(nw) time as well. That will take away from its clarity, however, so we skip this adjustment here. The importance of nice vtrees is the following result.

Theorem 13 A CNF with n variables and treewidth w has a nice vtree with width ≤ 2w+1 . Hence, the CNF has a compressed and trimmed SDD of size O(n2w ).

Nice vtrees can be constructed easily from appropriate dtrees of the given CNF [Darwiche, 2001], but we leave out the details for space limitations.

A CNF with n variables and pathwidth pw is known to have an OBDD of size O(n2pw ). Pathwidth pw and treewidthw are related by pw = O(w logn) (e.g., [Bodlaender, 1998]). Hence, a CNF with n variables and treewidth w has an OBDD of size polynomial in n and exponential in w [Ferrara et al., 2005]. Theorem 13 is tighter, however, since the SDD size is linear in n and exponential in w. BDD-trees are also canonical and come with a treewidth guarantee. Their size is also linear in n but at the expense of being doubly exponential in treewidth [McMillan, 1994]. Hence, SDDs come with a tighter treewidth bound than BDD-trees.

8 Preliminary Experimental Results

We present in this section some preliminary empirical results, in which we compare the size of SDDs and OBDDs for CNFs of some circuits in the ISCAS89 suite.

OBDDs are characterized by the use of variable orders, and effective methods for generating good variable orders have been critical to the success and wide adoption of OBDDs in practice. This includes orders that are generated statically (by analyzing the input CNF) or dynamically (by constantly revising them during the compilation process); see, e.g., [Meinel and Theobald, 1998]. In contrast, SDDs are characterized by the use of vtrees, which relax the need for total variable orders in OBDDs. This allows one to potentially identify more compact compilations, while maintaining canonicity and a polytime Apply operation (the key factors behind the success and adoption of OBDDs in practice).

In the preliminary experimental results that we present next, we hope to illustrate two points: (1) even simple heuristics for statically constructing vtrees can allow SDDs that are more compact than OBDDs, and (2) SDDs have the potential to subsume the use of OBDDs in practice. The latter point however depends critically on the development of more sophisticated heuristics for statically or dynamically identifying good vtrees.

The main static method we used for generating vtrees is a dual of the method used for generating dtrees in [Darwiche, 2001], with the roles of clauses and variables exchanged. 3 This method requires a variable elimination heuristic, which was the minfill heuristic in our experiments. We also ensured that the left child of a vtree node is the one with the smallest number of descendants. The resulting vtree is referred to as "Minfill vtree" in Table 1. The main static method we used for generating variable orders is the MINCE heuristic [Aloul et al., 2001]. This is referred to as "MINCE order." To provide more insights, we considered two additional types of vtrees and variable orders. In particular, we considered the variable order obtained by a left-right traversal of the Minfill vtree, referred to as "Minfill order" (see end of Section 2). We also considered the vtrees obtained by recursively dissecting the MINCE order in a balanced or random way, referred to as "MINCE balanced vtree" and "MINCE random vtree. 4 " We used the same implementation for both SDDs and OBDDs, obtaining OBDDs by using right-linear vtrees of the corresponding variable orders. The size of a compilation (whether SDD or OBDD) is computed by summing the sizes of decomposition nodes.

Table 1 reveal some patterns. First, Minfill vtrees give the best results overall, leading to smaller compilations almost consistently. Second, linearizing such vtrees, to obtain OBDDs as in Column 5, always leads to larger compilations in these experiments. Third, OBDDs based on MINCE orders are typically larger than SDDs based on Minfill vtrees. Finally, dissecting these orders into vtrees (whether balanced or random) produces better compilations in the majority of cases.

3 One could also use nice vtrees, but these appear to be less competitive based on a preliminary empirical evaluation.

4 In the case of randomly dissecting a variable order, we used five trials and reported the best size obtained.

As mentioned earlier, these results are preliminary as they do not exhaust enough the class of vtrees and variable orders used, nor do they exhaust enough the suite of CNFs used. One interesting aspect of these limited experiments, however, is the close proximity they reveal between the structures characterizing SDDs (vtrees) and the structures characterizing OBDDs (variable orders). In particular, the experiments suggest simple methods for turning one structure into the other. They also suggest that methods for generating good variable orders may form a basis for generating good vtrees.

Within the same vein, the experiments suggest that the practice of using SDDs can subsume the practice of using OBDDs as long as one includes right-linear vtrees in the space of considered vtrees. This is particularly important since the literature contains many generalizations of OBDDs that promise smaller representations, whether theoretically or empirically, yet require a substantial shift in practice to realize such potentials. A notable example here is the FBDD, which relaxes the variable ordering property of an OBDD, by requiring what is known as an "FBDD type" [Gergov and Meinel, 1994]. Using such types, FBDDs are known to be canonical and to support a polytime Apply operation. Yet, one rarely finds practical methods for constructing FBDD types and, hence, one rarely finds practical applications of FBDDs. Another broad class of OBDD generalizations is based on using decompositions that generalize or provide variants on the Shannon decomposition; see [Meinel and Theobald, 1998] for some examples. Again, none of these generalizations proved to be as influential as OBDDs in practice.

The close proximity of vtrees to variable orders is perhaps the most striking feature of SDDs, in comparison to other generalizations of OBDDs, as it stands to minimize the additional investment needed to identify good vtrees (given what we know about the generation of good variable orders). Clearly, the extent to which SDDs will eventually improve on OBDDs in practice will depend on making such an investment. This is why the generation of good vtrees, whether statically or dynamically, is a key priority of our future work on the subject.

Acknowledgement I wish to thank Arthur Choi, Knot Pipatsrisawat and Yexiang Xue for valuable discussions and for comments on earlier drafts of the paper.