A Top-Down Compiler for Sentential Decision Diagrams

1 Introduction

The area of knowledge compilation has a long tradition in AI (see, e.g., Marquis [1995], Selman and Kautz [1996], Cadoli and Donini [1997]). Since Darwiche and Marquis [2002], this area has settled on three major research directions: (1) identifying new tractable representations that are characterized by their succinctness and polytime support for certain queries and transformations; (2) developing efficient knowledge compilers; and (3) using those representations and compilers in various applications, such as diagnosis [Barrett, 2005; Elliott and Williams, 2006], planning [Barrett, 2004; Palacios et al., 2005; Huang, 2006], and probabilistic inference [Chavira and Darwiche, 2008]. For a recent survey on knowledge compilation, see Darwiche [2014].

This work focuses on developing efficient compilers. In particular, our emphasis is on the compilation of the sentential decision diagram (SDD) [Darwiche, 2011] that was recently discovered as a tractable representation of Boolean functions. SDDs are a strict superset of ordered binary decision diagrams (OBDDs) [Bryant, 1986], which are one of the most popular, tractable representations of Boolean functions. Despite their generality, SDDs still maintain some key properties behind the success of OBDDs in practice. This includes canonicity, which leads to unique representations of Boolean functions. It also includes the support of an efficient Apply operation that combines SDDs using Boolean operators. 1 SDDs also come with tighter size upper bounds than OBDDs [Darwiche, 2011; Oztok and Darwiche, 2014; Razgon, 2014b]. Moreover, SDDs have been used in different applications, such as probabilistic planning [Herrmann and de Barros, 2013], probabilistic logic programs [Vlasselaer et al., 2014; 2015], probabilistic inference [Choi et al., 2013; Renkens et al., 2014], verification of multi-agent systems [Lomuscio and Paquet, 2015], and tractable learning [Kisa et al., 2014; Choi et al., 2015].

Almost all of these applications are based on the bottomup SDD compiler developed by Choi and Darwiche [2013a], which was also used to compile CNFs into SDDs [Choi and Darwiche, 2013b]. This compiler constructs SDDs by compiling small pieces of a knowledge base (KB) (e.g., clauses of a CNF). It then combines these compilations using the Apply operation to build a compilation for the full KB.

An alternative to bottom-up compilation is top-down compilation. This approach starts the compilation process with a full KB. It then recursively compiles the fragments of the KB that are obtained through conditioning. The resulting compilations are then combined to obtain the compilation of the full KB. All existing top-down compilers assume CNFs as input, while bottom-up compilers can work on any input due to the Apply operation. Yet, compared to bottom-up compilation, top-down compilation has been previously shown to yield significant improvements in compilation time and space when compiling CNFs into OBDDs [Huang and Darwiche, 2004]. Thus, it has a potential to further improve the results on CNF to SDD compilations. Motivated by this, we study the compilation of CNFs into SDDs by a top-down approach.

This paper is based on the following contributions. We first identify a subset of SDDs, called Decision-SDDs, which facilitates the top-down compilation of SDDs. We then introduce a top-down algorithm for compiling CNFs into Decision-SDDs, which is harnessed with techniques used in modern SAT solvers, and a new component caching scheme. We finally present empirical results, showing ordersof-magnitude improvement in compilation time, compared to the state-of-the-art, bottom-up SDD compiler.

This paper is organized as follows. Section 2 provides technical background. Section 3 introduces the new representation Decision-SDD. Section 4 provides a formal framework for the compiler, which is then presented in Section 5. Experimental results are given in Section 6 and related work in Section 7. Due to space limitations, proofs of theorems are delegated to the full version of the paper. 2

1 The Apply operation combines two SDDs using any Boolean operator, and has its origins in the OBDD literature [Bryant, 1986].

2 Technical Background

Upper case letters (e.g., X) denote variables and bold upper case letters (e.g., X) denote sets of variables. A literal is a variable or its negation. A Boolean function f(Z) maps each instantiation z of variables Z to true (⊤) or false (⊥).

CNF: A conjunctive normal form (CNF) is a set of clauses, where each clause is a disjunction of literals. Conditioning a CNF ∆ on a literal ℓ, denoted ∆|ℓ, amounts to removing literal ¬ℓ from all clauses and then dropping all clauses that contain literal ℓ. Given two CNFs ∆ and Γ, we will write ∆ |= Γ to mean that ∆ entails Γ.

SDD: A Boolean function f(X,Y), with disjoint sets of variables X and Y, can always be decomposed into

such that pi ̸= ⊥ for all i; pi ∧ pj = ⊥ for i ̸= j; and ∨i pi = ⊤. A decomposition satisfying the above properties is known as an (X,Y)-partition [Darwiche, 2011]. Moreover, each pi is called a prime, each si is called a sub, and the (X,Y)-partition is said to be compressed when its subs are distinct, i.e., si ̸= sj for i ̸= j.

SDDs result from the recursive decomposition of a Boolean function using (X,Y)-partitions. To determine the X/Y variables of each partition, we use a vtree, which is a full binary tree whose leaves are labeled with variables; see Figure 1(b). Consider now the vtree in Figure1(b), and also the Boolean function f = (A∧B)∨(B∧C)∨(C∧D). Node v = 1 is the vtree root. Its left subtree contains variables X = {A, B} and its right subtree contains Y = {C, D}. Decomposing function f at node v = 1 amounts to generating an (X, Y)-partition:

This partition is represented by the root node of Figure 1(a). This node, which is a circle, represents a decision node with three branches, where each branch is called an element. Each element is depicted by a paired box p s . The left box corresponds to a prime p and the right box corresponds to its sub s. A prime p or sub s are either a constant, literal, or pointer to a decision node. In this case, the three primes are decomposed recursively, but using the vtree rooted at v = 2. Similarly, the subs are decomposed recursively, using the vtree rooted at v = 3. This decomposition process moves down one level in the vtree with each recursion, terminating at leaf vtree nodes.

2 Available at http://reasoning.cs.ucla.edu.

SDDs constructed as above are said to respect the used vtree. These SDDs may contain trivial decision nodes which correspond to (X,Y)-partitions of the form {(⊤, α)} or {(α,⊤), (¬α,⊥)}. When these decision nodes are removed (by directing their parents to α), the resulting SDD is called trimmed. Moreover, an SDD is called compressed when each of its partitions is compressed. Compressed and trimmed SDDs are canonical for a given vtree [Darwiche, 2011]. Here, we restrict our attention to compressed and trimmed SDDs. Figure 1(a) depicts a compressed and trimmed SDD for the above example. Finally, an SDD node representing an (X,Y)-partition is normalized for the vtree node v with variables X in its left subtree vl and variables Y in its right subtree vr . In Figure 1(a), SDD nodes are labeled with vtree nodes they are normalized for.

3 Decision-SDDs

We will next define the language of Decision-SDDs, which is a strict subset of SDDs and a strict superset of OBDDs. Our new top-down compiler will construct Decision-SDDs.

To define Decision-SDDs, we first need to distinguish between internal vtree nodes as follows. An internal vtree node is a Shannon node if its left child is a leaf, otherwise it is a decomposition node. The variable labeling the left child of a Shannon node is called the Shannon variable of the node. Vtree nodes 1 and 3 in Figure 2(b) are Shannon nodes, with X and Y as their Shannon variables. Vtree node 5 is a decomposition node. An SDD node that is normalized for a Shannon (decomposition) vtree node is called a Shannon (decomposition) decision node. A Shannon decision node has the form {(X, α), (¬X, β)}, where X is a Shannon variable.

Definition 1 (Decision-SDD) A Decision-SDD is an SDD in which each decomposition decision node has the form {(p, s1), (¬p, s2)} where s1 = ⊤, s1 = ⊥, or s1 = ¬s2.

Figure 2 shows a Decision-SDD and a corresponding vtree for the CNF {Y ∨¬Z, ¬X∨Z, X∨¬Y, X∨Q}. The language of Decision-SDDs is complete: every Boolean function can be represented by a Decision-SDD using an appropriate vtree.

For further insights into Decision-SDDs, note that a decomposition decision node must have the form {(f, g), (¬f,⊥)}, {(f,⊤), (¬f, g)}, or {(f, ¬g), (¬f, g)}. Moreover, these forms represent the Boolean functions f ∧g, f ∨ g, and f⊕g, respectively, where f and g are over disjoint sets of variables.

If an SDD is based on a general vtree, it may or may not be a Decision-SDD. However, the following class of vtrees, identified by Oztok and Darwiche [2014], guarantees a Decision-SDD.

Definition 2 (Decision Vtree) A clause is compatible with an internal vtree node v iff the clause mentions some variables inside vl and some variables inside vr . A vtree for CNF ∆ is said to be a decision vtree for ∆ iff every clause in ∆ is compatible with only Shannon vtree nodes. 3

Figure 2(b) depicts a decision vtree for the CNF {Y ∨ ¬Z, ¬X ∨Z, X ∨¬Y, X ∨Q}.

Proposition 1 Let v be a decision vtree for CNF ∆. An SDD for ∆ that respects vtree v must be a Decision-SDD.

As such, the input to our compiler will be a CNF and a corresponding decision vtree, and the result will be a DecisionSDD for the CNF. Note that one can always construct a decision vtree for any CNF [Oztok and Darwiche, 2014].

When every internal vtree node is a Shannon vtree node (i.e., the vtree is right-linear), the Decision-SDD corresponds to an OBDD. A quasipolynomial separation between SDDs and OBDDs was given by Razgon [2014b]. As it turns out, the SDDs used to show this separation are actually DecisionSDDs. We now complement this result by showing that Decision-SDDs can be simulated by OBDDs with at most a quasipolynomial increase in size (it is currently unknown if this holds for general SDDs).

Theorem 1 Every Decision-SDD with n variables and size N has an equivalent OBDD with size ≤ N 1+log n .

The above result is based on [Razgon, 2014a], which simulates decomposable AND-OBDDs with OBDDs. 4

Xue et al. [2012] have identified a class of Boolean functions fi, with corresponding variable orders πi, such that the OBDDs based on orders πi have exponential size, yet the SDDs based on vtrees that dissect orders πi have linear size. 5 Interestingly, the SDDs used in this result turn out to be Decision-SDDs as well. Hence, a variable order that blows up an OBDD can sometimes be dissected to obtain a vtree that leads to a compact Decision-SDD. This reveals the practical significance of Decision-SDDs despite the quasipolynomial simulation of Theorem 1. We finally note that there is no known separation result between Decision-SDDs and SDDs.

3 Without loss of generality, ∆ has no empty or unit clauses.

4 A decomposable AND-OBDD can be turned into a DecisionSDD in polytime, but it is not clear whether the converse is true.

5 A vtree dissects a variable order if the order is generated by a left-right traversal of the vtree.

Algorithm 1: SAT(∆)

Input: ∆ : a CNF Output: ⊤ if ∆ is satisfiable; ⊥ otherwise 1 Γ ← {} // learned clauses 2 D← 〈〉 // decision sequence 3 while true do 4 if unit resolution detects a contradiction in ∆ ∧ Γ ∧ D then 5 if D = 〈〉 then return⊥ 6 α ← asserting clause for (∆, Γ, D) 7 m ← the assertion level of α 8 D ← the first m decisions of D 9 Γ ← Γ ∪ {α} // learning clause α 10 else 11 if ℓ is a literal where neither ℓ nor ¬ℓ are implied by unit resolution from ∆ ∧ Γ ∧ D then D ← D; ℓ 12 else return⊤

We will next provide a top-down algorithm for compiling CNFs into Decision-SDDs, which is based on state-of-theart techniques from SAT solving. Our intention is to provide a formal description of the algorithm, which is precise and detailed enough to be reproducible by the community. We will start by providing a formal description of our framework in Section 4, and then present our algorithm in Section 5.

4 A Formal Framework for the Compiler

Modern SAT solvers utilize two powerful and complementary techniques: unit resolution and clause learning. Unit resolution is an efficient, but incomplete, inference rule which identifies some of the literals implied by a CNF. Clause learning is a process which identifies clauses that are implied by a CNF, then adds them to the CNF so as to empower unit resolution (i.e., allows it to derive more literals). These clauses, also called asserting clauses, are learned when unit resolution detects a contradiction in the given CNF. We will neither justify asserting clauses, nor delve into the details of computing them, since these clauses have been well justified and extensively studied in the SAT literature (see, e.g., Moskewicz et al. [2001]). We will, however, employ asserting clauses in our SDD compiler (we employ first-UIP asserting clauses as implemented by RSat [Pipatsrisawat and Darwiche, 2007]).

As a first step towards introducing our compiler, we present in Algorithm 1 a modern SAT solver that is based on unit resolution and clause learning. This algorithm repeatedly performs the following process. A literal ℓ is chosen and added to the decision sequence D (we say that ℓ has been decided at level |D|). After deciding the literal ℓ, unit resolution is performed on ∆∧ Γ ∧D. If no contradiction is found, another literal is decided. Otherwise, an asserting clause α is identified. A number of decisions are then erased until we reach the decision level corresponding to the assertion level of clause α, at which point α is added to Γ. 6 The solver terminates under one of two conditions: either a contradiction is found under an empty decision sequence D (Line 5), or all literals are successfully decided (Line 12). In the first case, the input CNF must be unsatisfiable. In the second case, the CNF is satisfiable with D as a satisfying assignment.

6 The assertion level is computed when the clause is learned. It corresponds to the lowest decision level at which unit resolution is guaranteed to derive a new literal using the learned clause.

Algorithm 1 is iterative. Our SDD compiler, however, will be recursive. To further prepare for this recursive algorithm, we will take two extra steps. The first step is to abstract the primitives used in SAT solvers (Figure 3), viewing them as operations on what we shall call a SAT state.

Definition 3 A SAT state is a tuple S = (∆, Γ,D, I) where ∆ and Γ are sets of clauses, D is a sequence of literals, and I is a set of literals. The number of literals in D is called the decision level of S. Moreover, S is said to be satisfiable iff ∆∧D is satisfiable. 7

Here, ∆ is the input CNF, Γ is the set of learned clauses, D is the decision sequence, and I are the literals implied by unit resolution from ∆ ∧ Γ ∧ D. Hence, ∆ |= Γ and D ⊆ I .

The second step towards presenting our compilation algorithm is a recursive algorithm for counting the models of a CNF, which utilizes the above abstractions (i.e., the SAT state and its associated primitives in Figure 3). To simplify the presentation, we will assume a variable order π of the CNF. If X is the first variable in order π, then one recursively counts the models of ∆∧X, recursively counts the models of ∆∧¬X, and then add these results to obtain the model count of ∆. This is given in Algorithm 2, which is called initially with the SAT state (∆, {}, 〈〉, {}) to count the models of ∆. What makes this algorithm additionally useful for our presentation purposes is that it is exhaustive in nature. That is, when considering variable X, it must process both its phases, X and ¬X. This is similar to our SDD compilation algorithm - but in contrast to SAT solvers which only consider one phase of the variable. Moreover, Algorithm 2 employs the primitives of Figure 3 in the same way that our SDD compiler will employ them later.

The following is a key observation about Algorithm 2 (and the SDD compilation algorithm). When a recursive call returns a learned clause, instead of a model count, this only means that while counting the models of the CNF ∆ ∧ D

7 Without loss of generality, ∆ has no empty or unit clauses.

Algorithm 2: #SAT(π, S)

targeted by the call, unit resolution has discovered an opportunity to learn a clause (and learned one). Hence, we must backtrack to the assertion level, add the clause, and then try again (Lines 10 and 19). In particular, returning a learned clause does not necessarily mean that the CNF targeted by the recursive call is unsatisfiable. The only exception is the root call, for which the return of a learned clause implies an unsatisfiable CNF (and, hence, a zero model count) since the learned clause must be empty in this case. 8

5 A Top-Down SDDCompiler

We are now ready to present our SDD compilation algorithm, whose overall structure is similar to Algorithm 2, but with a few exceptions. First, the SDD compilation algorithm is driven by a vtree instead of a variable order. Second, it uses the vtree structure to identify disconnected CNF components and compiles these components independently. Third, it employs a component caching scheme to avoid compiling the same component multiple times.

This is given in Algorithm 3, which is called initially with the SAT state S = (∆, {}, 〈〉, {}) and a decision vtree v for ∆, to compile an SDD for CNF ∆. 9 When the algorithm is applied to a Shannon vtree node, its behavior is similar to Algorithm 2 (Lines 15-44). That is, it basically uses the Shannon variable X and considers its two phases, X and ¬X. However, when applied to a decomposition vtree node v (Lines 5-14), one is guaranteed that the CNF associated with v is decomposed into two components, one associated with

8 When the decision sequence D is empty, and unit resolution detects a contradiction in ∆∧Γ, the only learned clause is the empty clause, which implies that ∆ is unsatisfiable (since ∆ |= Γ).

9 Algorithm 3 assumes that certain negations are freely available (e.g., ¬p on Line 14). One can easily modify the algorithm so it returns both an SDD and its negation, making all such negations freely available. We skip this refinement here for clarity of exposition, but it can be found in the longer version of the paper.

Algorithm 3: c2s(v, S)

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

Input: v : a vtree node, S : a SAT state (∆, Γ, D, I) Output: A Decision-SDD or a clause 1 if v is a leaf node then 2 X ← variable of v 3 if X or ¬X belongs to I then return the literal of X that belongs to I 4 else return ⊤ 5 else if v is a decomposition vtree node then 6 p ← c2s(vl , S) 7 if p is a learned clause then 8 clean cache(vl ) 9 return p 10 s ← c2s(vr , S) 11 if s is a learned clause then 12 clean cache(v) 13 return s 14 return unique({(p, s), (¬p, ⊥)}) 15 else 16 key ← Key(v, S) 17 if cache(key) ̸= nil then return cache(key) 18 X ← Shannon variable of v 19 if either X or ¬X belongs to I then 20 p ← the literal of X that belongs to I 21 s ← c2s(vr , S) 22 if s is a learned clause then return s 23 return unique({(p, s), (¬p, ⊥)}) 24 s1 ← decide literal(X, S) 25 if s1 is success then s1 ← c2s(vr , S) 26 undo decide literal(X, S) 27 if s1 is a learned clause then 28 if at assertion level(s1, S) then 29 s1 ← assert clause(s1, S) 30 if s1 is success then return c2s(v, S) 31 else return s1 32 else return s1 33 s2 ← decide literal(¬X, S) 34 if s2 is success then s2 ← c2s(vr , S) 35 undo decide literal(¬X, S) 36 if s2 is a learned clause then 37 if at assertion level(s2, S) then 38 s2 ← assert clause(s2, S) 39 if s2 is success then return c2s(v, S) 40 else return s2 41 else return s2 42 α ← unique({(X, s1), (¬X, s2)}) 43 cache(key) ← α 44 return α

the left child vl and another with the right child vr (since v is a decision vtree for ∆). In this case, the algorithm compiles each component independently and combines the results.

We will next show the soundness of the algorithm, which requires some additional definitions. Let ∆ be the input CNF. Each vtree node v is then associated with:

• CNF(v): The clauses of ∆ mentioning only variables inside the vtree rooted at v (clauses of v).
• ContextC(v): The clauses of ∆ mentioning some variables inside v and some outside v (context clauses of v).
• ContextV (v): The Shannon variables of all vtree nodes that are ancestors of v (context variables of v).

We start with the following invariant of Algorithm 3.

Theorem 2 Every call c2s(v, S) with S = (∆, Γ, D, I) satisfies ∆ |= Γ and V ars(D) ⊆ ContextV (v) ⊆ V ars(I).

Hence, when calling vtree node v, all its context variables must be either decided or implied. We can now define the CNF component associated with a vtree node v at state S.

Definition 4 The component of vtree node v and state S = (., ., ., I) is CNF(v, S) = CNF(v) ∧ ContextC(v)|γ, where γ are the literals of ContextV (v) appearing in I.

Hence, the component CNF(v, S) will only mention variables in vtree v. Moreover, the root component (CNF(v, S) with v being the root vtree node) is equal to ∆.

Following is the soundness result assuming no component caching (i.e., while omitting Lines 8, 12, 16, 17 and 43).

Theorem 3 A call c2s(v, S) with a satisfiable state S will return either an SDD for component CNF (v, S) or a learned clause. Moreover, if v is the root vtree node, then a learned clause will not be returned.

Theorem 4 A call c2s(v, S) with an unsatisfiable state S will return a learned clause, or one of its ancestral calls c2s(v′ , S′ ) will return a learned clause, where v′ is a decomposition vtree node.

We now have our soundness result (without caching).

Corollary 1 If v is the root vtree node, then call c2s(v, (∆, {}, 〈〉, {})) returns an SDD for ∆ if ∆ is satisfiable, and returns an empty clause if ∆ is unsatisfiable.

We are now ready to discuss the soundness of our caching scheme (Lines 8, 12, 16, 17 and 43). This requires an explanation of the difference in behavior between satisfiable and unsatisfiable states (based on Theorem 1 of Sang et al. [2004]). Consider the component CNFs ∆X and ∆Y over disjoint variables X and Y, and let Γ be another CNF such that ∆X ∧ ∆Y |= Γ (think of Γ as some learned clauses). Suppose that IX is the set of literals over variables X implied by unit resolution from ∆X ∧ Γ. One would expect that ∆X ≡ ∆X ∧ IX (and similarly for ∆Y). In this case, one would prefer to compile ∆X ∧ IX instead of ∆X as the former can make unit resolution more complete, leading to a more efficient compilation. In fact, this is exactly what Algorithm 3 does, as it includes the learned clauses Γ in unit resolution when compiling a component. However, ∆X ≡ ∆X∧IX is not guaranteed to hold unless ∆X∧∆Y is satisfiable. When this is not the case, compiling ∆X∧IX will yield an SDD that implies ∆X but is not necessarily equivalent to it. However, this is not problematic for our algorithm, for the following reason. If ∆X∧∆Y is unsatisfiable, then either ∆X or ∆Y is unsatisfiable and, hence, either ∆X∧IX or ∆Y ∧ IY will be unsatisfiable, and their conjunction will be unsatisfiable. Hence, even though one of the components was compiled incorrectly, the conjunction remains a valid result. Without component caching, the incorrect compilation will be discarded. However, with component caching, one also needs to ensure that incorrect compilations are not cached (as observed by Sang et al. [2004]).

By Theorem 4, if we reach Line 8 or 12, then state S may be unsatisfiable and we can no longer trust the results cached below v. Hence, clean cache(v) on Line 8 and 12 removes all cache entries that are indexed by Key(v′ , .), where v′ is a descendant of v. We now discuss Lines 16, 17 and 43.

Definition 5 A function Key(v, S) is called a component key iff Key(v, S) = Key(v, S′ ) implies that components CNF (v, S) and CNF (v, S′ ) are equivalent.

Hence, as long as Line 16 uses a component key according to this definition, then caching is sound. The following theorem describes the component key we used in our algorithm.

Theorem 5 Consider a vtree node v and a corresponding state S = (., ., ., I). Define Key(v, S) as the following bit vector: (1) each clause δ in ContextC(v) is mapped into one bit that captures whether I |= δ, and (2) each variable X that appears in vtree v and ContextC(v) is mapped into two bits that capture whether X ∈ I, ¬X ∈ I, or neither. Then function Key(v, S) is a component key.

6 Experimental Results

We now present an empirical evaluation of the new topdown compiler. In our experiments, we used two sets of benchmarks. First, we used some CNFs from the iscas85, iscas89, and LGSynth89 suites, which correspond to sequential and combinatorial circuits used in the CAD community. We also used some CNFs available at http://www.cril.univ-artois.fr/PMC/pmc.html, which correspond to different applications such as planning and product configuration. We compiled those CNFs into SDDs and Decision-SDDs. To compile SDDs, we used the SDD package [Choi and Darwiche, 2013a]. All experiments were performed on a 2.6GHz Intel Xeon E5-2670 CPU under 1 hour of time limit and with access to 50GB RAM. We next explain our results shown in Table 1.

The first experiment compares the top-down compiler against the bottom-up SDD compiler. Here, we first generate a decision vtree 10 for the input CNF, and then compile the CNF into an SDD using (1) the bottom-up compiler without dynamic minimization (denoted BU), (2) the bottom-up compiler with dynamic minimization (denoted BU+), and (3) the top-down compiler (denoted TD), using the same vtree. 11 Note that BU+ uses a minimization method, which dynamically searches for better vtrees during the compilation process, leading to general SDDs, whereas both BU and TD do not modify the input decision vtree, hence generating Decision-SDDs with the same sizes. We report the corresponding compilation times and sizes in Columns 2-4 and 6-7, respectively. The top-down Decision-SDD compiler was consistently faster than the bottom-up SDD compiler, regardless of the use of dynamic minimization. In fact, in Column 5 we report the speed-ups obtained by using the top-down compiler against the best result of the bottom-up compiler (i.e., either BU or BU+, whichever was faster). There are 40 cases (out of 61) where we observe at least an order-ofmagnitude improvement in time. Also, there are 15 cases where top-down compilation succeeded and both bottom-up compilations failed. However, the situation is different for the sizes, when the bottom-up SDD compiler employs dynamic minimization. In almost all of those cases, BU+ constructed smaller representations. As reported in Column 8, which shows the relative sizes of SDDs generated by TD and BU+, there are 21 cases where BU+ produced an orderof-magnitude smaller SDDs. This is not a surprising result though, given that BU+ produces general SDDs and our topdown compiler produces Decision-SDDs, and that SDDs are a strict superset of Decision-SDDs.

10 We obtained decision vtrees as in Oztok and Darwiche [2014].

11 Choi and Darwiche [2013b] used balanced vtrees constructed from the natural variable order, and manual minimization. We chose to use decision vtrees as they performed better than balanced vtrees.

Since Decision-SDDs are a subset of SDDs, any minimization algorithm designed for SDDs can also be applied to Decision-SDDs. In this case, however, the results may not be necessarily Decision-SDDs, but general SDDs. In our second experiment, we applied the minimization method provided by the bottom-up SDD compiler to our compiled Decision-SDDs (as a post-processing step). We then added the top-down compilation times to the post-processing minimization times and reported those in Column 9, with the resulting SDD sizes in Column 10. As is clear, the post-processing minimization step significantly reduces the sizes of SDDs generated by our top-down compiler. In fact, the sizes are almost equal to the sizes generated by BU+ (Column 7). The top-down compiler gets slower due to the cost of the post-processing minimization step, but its total time still dominates the bottom-up compiler. Indeed, it can still be an order-of-magnitude faster than the bottom-up compiler (18 cases). This shows that one can also use Decision-SDDs as a representation that facilitates the compilation of CNFs into general SDDs.

7 RelatedWork

Our algorithm for compiling CNFs into SDDs is based on a similar algorithm, introduced recently [Oztok and Darwiche, 2014]. The latter algorithm was proposed to improve a size upper bound on SDDs. However, it did not identify DecisionSDDs, nor did it suggest a practical implementation. The current work makes the previously introduced algorithm practical by adding powerful techniques from the SAT literature and defining a practical caching scheme, resulting in an efficient compiler that advances the state-of-the-art.

Combining clause learning and component caching was already used in the context of knowledge compilation [Darwiche, 2004] and model counting [Sang et al., 2004]. Yet, neither of these works described the corresponding algorithms and their properties at the level of detail and precision that we did here. A key difference between the presented topdown compiler and the one introduced in Darwiche [2004], called c2d, is that we compile CNFs into SDDs, while c2d compiles CNFs into d-DNNFs. These two languages differ in their succinctness and tractability (SDDs are a strict subset of d-DNNFs, and are less succinct but more tractable). For example, SDDs can be negated in linear time. Hence, the CNF-to-SDD compiler we introduced can easily be used as a DNF-to-SDD compiler. For that, we first negate the DNF into a CNF by flipping the literals and treating each term as a clause. After compiling the resulting CNF into an SDD, we can negate the resulting SDD efficiently, which would become the SDD for the given DNF. Since no efficient negation algorithm is known for d-DNNFs, one cannot use c2d when the original knowledge base is represented in DNF. We note that we did not evaluate our compiler for compiling DNFs into SDDs, so we do not know how practical it would be. Still, it can be immediately used to compile DNFs, which has not been discussed before in the context of top-down compilation. Another top-down compiler, called eadt, was presented recently [Koriche et al., 2013], which compiles CNFs into a tractable language that makes use of decision trees with xor nodes. A detailed comparison of bottom-up and topdown compilation has been made before in the context of compiling CNFs into OBDDs [Huang and Darwiche, 2004]. Our work can be seen as making a similar comparison for compiling CNFs into SDDs.

8 Conclusion

We identified a subset of SDDs, called Decision-SDDs, and introduced a top-down algorithm for compiling CNFs into Decision-SDDs that is based on techniques from the SAT literature. We provided a formal description of the new algorithm with the hope that it would facilitate the development of efficient compilers by the community. Our empirical evaluation showed that the presented top-down compiler can yield significant improvements in compilation time against the state-of-the-art bottom-up SDD compiler, assuming that the input is a CNF.

Acknowledgments

This work has been partially supported by ONR grant #N00014-12-1-0423 and NSF grant #IIS-1118122.