DPLL with a Trace: From SAT to Knowledge Compilation

1 Introduction

Knowledge compilation has been a key direction of research in automated reasoning [Selman and Kautz, 1991; Marquis, 1995; Selman and Kautz, 1996; Cadoli and Donini, 1997; Darwiche and Marquis, 2002]. When propositional theories are compiled into a suitable target language, some generally intractable queries may be answered in time polynomial in the size of the compilation. Compiling combinational circuits into OBDDs, for example, allows functional equivalence to be tested in polynomial time (or constant time if the same variable order is used) [Bryant, 1986]. More recent applications of compilation can be found in the fields of diagnosis and planning, involving the use of the DNNF language [Darwiche, 2001a; Barrett, 2004; Palacios et al., 2005].

Propositional Satisfiability (SAT), on the other hand, has been an area of no less importance, or activity. Aside from its theoretical significance as the prototypical NPcomplete problem, SAT finds practical applications in many areas of artificial intelligence and computer science at large. While SAT algorithms have substantially improved over the decades, many of them continue to build on what is known as the DPLL search [Davis et al., 1962] (for examples, see complete SAT solvers in the 2004 SAT Competition: http://satlive.org/SATCompetition/2004/).

This paper sets out to demonstrate a deep connection between SAT solving and knowledge compilation. In the first direction, we show how advances in search-based SAT algorithms will carry over, via an exhaustive version of DPLL, to compiling propositional theories into one of several tractable languages. We start by pointing out that the trace of an exhaustive DPLL search, recorded compactly as a DAG, can be viewed as a compiled representation of the input theory. With different constraints imposed or lifted on the search process, we then show that the compilation will be in the language of d-DNNF, FBDD, and OBDD, respectively. These languages are known to decrease in succinctness: A propositional theory may have a polynomial-size representation in d-DNNF, but not in FBDD; or in FBDD, but not in OBDD [Darwiche and Marquis, 2002].

In the second direction, we formulate two principles by which the intrinsic complexity and computational power of a DPLL-based exhaustive search is related to the language membership of its traces. Applying these principles, we point out that several recent model counters are doing enough work to actually compile theories into d-DNNF. We also discuss a potential limitation on the efficiency of these model counters, as well as knowledge compilers using similar algorithms, based on the fact that these algorithms only generate traces in a specific subset of d-DNNF. Finally, we note that the efficiency of all DPLL-based exhaustive search algorithms are inherently limited by their inability to produce traces beyond d-DNNF. This realization is significant because some important computational tasks, such as existential quantification of variables and computation of minimum-cardinality models, could be efficiently accomplished with a weaker representation known as DNNF, a strict superset of d-DNNF.

Under our uniform DPLL-based framework for knowledge compilation, the power of successful modern SAT techniques is harnessed, including sophisticated conflict analysis, clause learning, faster detection of unit clauses, and new branching heuristics. We also discuss caching methods specific to the needs of compilation and tailored to the desired target compilation language, as well as structure-based complexity guarantees. We finally relate our experimental results on implementations of the three respective compilers to the theoretical succinctness relations of the corresponding languages.

The remainder of the paper is organized as follows. Section 2 reviews a number of propositional languages concerned in this work and their theoretical roles and relations in knowledge compilation. In Section 3, we describe a uniform framework for knowledge compilation, with regard to these languages, based on recording the trace of an exhaustive DPLL search, and discuss its implications on our understanding of the complexity and computational power of various search algorithms. We report experimental results in Section 4 and conclude in Section 5.

2 Target Compilation Languages

A logical form qualifies as a target compilation language if it supports some set of nontrivial queries, usually including clausal entailment, in polynomial time. We will review in this section several target compilation languages relevant to the present paper, and refer the reader to [Darwiche and Marquis, 2002] for a more comprehensive discussion.

The languages we shall describe are all subsets of the more general Negation Normal Form (NNF). A sentence in NNF is a propositional formula where conjunction (and, ∧), disjunction (or, ∨) and negation (not, ¬) are the only connectives and negation only appears next to a variable; sharing of subformulas is permitted by means of a rooted DAG; see Figure 1a.

We start with the DNNF language, which is the set of all NNF sentences that satisfy decomposability: conjuncts of any conjunction share no variable. Our next language, dDNNF, satisfies both decomposability and determinism: disjuncts of any disjunction are pairwise logically inconsistent. The formula of Figure 1a, for example, is in d-DNNF.

The FBDD language is the subset of d-DNNF where the root of every sentence is a decision node, which is defined recursively as either a constant (0 or 1) or a disjunction in the form of Figure 1b where X is a propositional variable and α and β are decision nodes. Note that an equivalent but more compact drawing of a decision node-shown in Figure 1c-is widely used in the formal verification literature, where FBDDs are equivalently known as Binary Decision Diagrams (BDDs) that satisfy the test-once property: each variable appears at most once on any root-to-sink path [Gergov and Meinel, 1994]. See Figure 2c for an FBDD example using this more compact drawing.

The OBDD language is the subset of FBDD where all sentences satisfy the ordering property: variables appear in the same order on all root-to-sink paths [Bryant, 1986]. See Figure 2d for an OBDD example. For a particular variable order <, we also write OBDD< to denote the corresponding OBDD subset where all sentences use order <.

Having an option among target compilation languages is desirable, despite their succinctness relations which may be known. The reason is that the succinctness of a language often runs counter to its tractability-that is, the set of queries supported in polynomial time-and the best choice may depend on the task at hand. Given this trade-off between the two criteria, the rule of thumb, according to [Darwiche and Marquis, 2002], is to choose the most succinct language that supports the desired set of queries in polynomial time (in some cases the support of transformations, such as Boolean operations, is also a consideration).

Table 1 lists a set of polynomial-time queries of interest supported by each of these languages; the twoletter abbreviations stand for the following eight queries, respectively: COnsistency, VAlidity, Clausal Entailment, IMplicant, EQuivalence, Sentential Entailment, model CounTing, Model Enumeration [Darwiche and Marquis, 2002].

Interestingly, this table offers one explanation for the popularity of OBDDs in formal verification where efficient equivalence testing, among other things, is often critical. Although more succinct, d-DNNF and FBDD are not known to admit a polynomial-time equivalence test (a polynomial-time probabilistic equivalence test is possible [Darwiche and Huang, 2002; Blum et al., 1980]). Note also that although there is no difference between d-DNNF and FBDD to the extent of this table, the question mark on the equivalence test (EQ) could eventually be resolved differently for the two languages.

In the following section we will use the notion of recording the trace of a DPLL search to establish an important link between SAT and knowledge compilation, providing a uniform framework for compiling knowledge into some of these languages. From this point of view we will then discuss our new understanding of the complexity and computational power of algorithms based on exhaustive DPLL.

3 DPLL with a Trace

We start with the basic DPLL search as in [Davis et al., 1962]. To facilitate our subsequent discussion of variants of this algorithm, we will omit unit resolution from the pseudocode. (All our discussions, however, are valid in the presence of unit resolution; see also the following two footnotes.)

Algorithm 1 is a summary of DPLL for SAT. It works by recursively doing a case analysis on the assignment to a selected variable (Lines 5&6): The theory is satisfiable if and only if either case results in a satisfiable subtheory. ∆|x=0 (∆|x=1) denotes the CNF obtained by replacing all occurrences of x with 0 (1) in ∆ and simplifying the formula accordingly. In effect, this algorithm performs a search in the space of variable assignments until it finds one that satisfies the given CNF formula or realizes that no satisfying assignment exists. 1

Now consider extending Algorithm 1 so that it will enumerate all satisfying assignments-by always exploring both branches of Line 6-rather than terminate on finding the first one. Figure 2b depicts the search tree of this exhaustive version of DPLL on the CNF of Figure 2a, under some particular variable ordering. We are using a dotted (solid) line to denote setting the variable to 0 (1), and will refer to the corresponding branch of the search as the low (high) branch. Note that each leaf of this tree gives a partial variable assignment that satisfies the theory regardless of the values of any unassigned variables, and the whole tree characterizes precisely the set of all satisfying assignments.

1 To incorporate unit resolution into this simplified picture where all assignments are by decision, one can assume that when a chosen decision variable (Line 5 of Algorithm 1) has been implied by unit resolution, the algorithm will simply proceed down the right branch according to the implied value of the variable, noting that the other branch leads to unsatisfiability. One may also assume that in choosing a decision variable, those already implied by unit resolution will be favored, although this would represent a restriction on the search traces, which we describe shortly, that can be possibly generated.

Algorithm 1 DPLL(∆): returns satisfiability of CNF ∆

• 1: if there is an empty clause in ∆ then
• 2: return 0
• 3: if there is no variable in ∆ then
• 4: return 1
• 5: select variable x of ∆
• 6: return DPLL(∆|x=0) or DPLL(∆|x=1)

As the title of this paper suggests, we like to think of this complete search tree, also known as a termination tree or decision tree, as the trace left by the exhaustive DPLL search. Such a trace corresponds to the portion of the search space actually explored by a particular execution of the algorithm. Furthermore, the trace can be viewed as a compiled representation of the original CNF formula, because it uniquely identifies the propositional theory-by specifying its models.

From the viewpoint of knowledge compilation, however, a search trace recorded in its present formmay not be immediately useful, because it will typically have a size proportional to the amount of work done to produce it. Answering even a linear-time query on such a compilation, for example, would be as if one were running the whole search over again.

This problem can be remedied by reducing the trace from a tree to a DAG, with repeated applications of the following two rules: (i) Isomorphic nodes (i.e., nodes that have the same label, same low child, and same high child) are merged; (ii) Any node with identical children is deleted and pointers to it are redirected to either one of its children [Bryant, 1986].

If we apply these reduction rules to the tree of Figure 2b, and rename "sat/unsat" to "1/0", we will get the DAG of Figure 2c (in this particular example the first rule only applies to the terminal nodes and the second rule does not apply). Observe that this DAG is none other than a propositional theory in the language of FBDD. And this is no accident!

3.1 Compiling CNF into FBDD

We are in fact in possession of a CNF-to-FBDD compiler, described more formally in Algorithm 2. The main difference from the original DPLL is on Line 6: we always explore both branches, and the newly introduced function, get-node, provides a means of recording the trace of the search in the form of a DAG. Specifically, get-node will return a decision node labeled with the first argument, having the second argument as the low child, and having the third argument as the high child. Note that Lines 2&4 have been modified to return the terminal decision nodes, instead of the Boolean constants.

We point out that the amount of space required by Algorithm 2 to store the FBDD is only proportional to the size of the final result. In other words, it will never create redundant nodes to be reduced later. This is because the two reduction rules are built-in by means of a unique nodes table, well-known in the BDD community [Somenzi, Release 240]. Specifically, all nodes created by get-node are stored in a hash table and get-node will not create a new node if (i) the node to be created already exists in the table (that existing node is returned); or (ii) the second and third arguments are the same (either argument is returned).

Algorithm 2 dpllf (∆): compiles CNF ∆ into FBDD (dpll is lowercased to distinguish it fromAlgorithm 3, its full version)

• 1: if there is an empty clause in ∆ then
• 2: return 0-sink
• 3: if there is no variable in ∆ then
• 4: return 1-sink
• 5: select variable x of ∆
• 6: return get-node(x, dpllf (∆|x=0), dpllf (∆|x=1))

Caching. Despite the use of unique nodes which controls the space complexity, Algorithm 2 still has a time complexity proportional to the size of the tree version of the search trace: Portions of the DAG can end up being explored multiple times. To alleviate this problem, one resorts to formula caching [Majercik and Littman, 1998].

Algorithm 3 describes the same CNF-to-FBDD compiler, but now with caching: The result of a recursive call DPLLf (∆) will be stored in a cache (Line 10) before being returned, indexed by a key (computed on Line 5) identifying ∆; any subsequent call on some ∆′ will immediately return the existing compilation for ∆ from the cache (Line 7) if ∆′ is found to be equivalent to ∆ (by a key comparison on Line 6).

In practice, one normally focuses on efficiently recognizing formulas that are syntactically identical (i.e., have the same set of clauses). Various methods have been proposed for this purpose in recent years, starting with [Majercik and Littman, 1998] who used caching for probabilistic planning problems, followed by [Darwiche, 2002] who proposed a concrete formula caching method in the context of knowledge compilation, then [Bacchus et al., 2003; Sang et al., 2004] in the context of model counting, and then [Huang and Darwiche, 2004; Darwiche, 2004] who proposed further refinements on [Darwiche, 2002].

3.2 FromFBDD to OBDD

We now turn to OBDD as our target compilation language. Note that in Algorithm 3, DPLL is free to choose any variable on which to branch (Line 8). This corresponds to the use of a dynamic variable ordering heuristic in a typical SAT solver, in keeping with the spirit of FBDD compilation.

Not surprisingly, a CNF-to-OBDD compiler can be obtained by switching from dynamic to static variable ordering: The new compiler will take a particular variable order π as a second argument, and make sure that this order is enforced when constructing the DAG. See Line 8 of Algorithm 4.

Caching. Naturally, any general formula caching method, such as the ones we described earlier, will be applicable to Algorithm 4. For this more constrained compiler, however, a special method is available where shorter cache keys can be used to reduce the cost of their manipulation. The reader is referred to [Huang and Darwiche, 2004] for details of this method, which allows one to bound the number of distinct cache keys, therefore providing both a space and a time complexity bound. In particular, due to this specific caching scheme, the space and time complexity of compiling OBDDs

Algorithm 3 DPLLf (∆): compiles CNF ∆ into FBDD

• 1: if there is an empty clause in ∆ then
• 2: return 0-sink
• 3: if there is no variable in ∆ then
• 4: return 1-sink
• 5: key = compute-key(∆)
• 6: if (result = cache-lookup(key)) ̸= null then
• 7: return result
• 8: select variable x of ∆
• 9: result = get-node(x, DPLLf (∆|x=0), DPLLf (∆|x=1))
• 10: cache-insert(key, result)
• 11: return result

was shown to be exponential only in the cutwidth of the given CNF. A variant caching scheme allows one to show a parallel complexity in terms of the pathwidth (cutwidth and pathwidth are not comparable).

Classical OBDD Construction. We emphasize here that Algorithm 4 represents a distinct way of OBDD construction, in contrast to the standard method widely adopted in formal verification where one recursively builds OBDDs for components of the system (or propositional theory) to be compiled and combines them using the Apply operator [Bryant, 1986]. A well-known problem with this latter method is that the intermediate OBDDs that arise in the process can grow so large as to make further manipulation impossible, even when the final result would have a tractable size. Considering that the final OBDD is really all that one is after, Algorithm 4 affords a solution to this problem by building exactly it, no more and no less (although it may do more work than is linear in the OBDD size, both because inconsistent subproblems do not contribute to the OBDD size, and because the caching is not complete). An empirical comparison of this compilation algorithm and the traditional OBDD construction method can be found in [Huang and Darwiche, 2004].

3.3 FromFBDD to d-DNNF

Although any FBDD is also a d-DNNF sentence by definition, it remains a reasonable option to compile propositional theories into d-DNNF only, given its greater succinctness. Considering that d-DNNF is a relaxation of FBDD, we can obtain a d-DNNF compiler by relaxing a corresponding constraint on Algorithm 3. Specifically, immediately before Line 8, we need not insist any more that a case analysis be performed on some variable x of the formula; instead, the following technique of decomposition can be utilized. See Algorithm 5. 2

As soon as variable instantiation finishes without contradiction, we will examine the remaining CNF formula, and partition it into subsets that do not share a variable (Line 5). These subsets can then be recursively compiled into d-DNNF (Lines 7-9) and conjoined as an and-node (Line 10). Note that decomposition takes precedence over case analysis: Only when no decomposition is possible do we branch on a selected variable as in regular DPLL (Lines 14&15).

2 When unit resolution and clause learning are both integrated into this algorithm, an issue arises regarding implications via learned clauses that span otherwise disjoint components. See [Sang et al., 2004] for more discussion on this issue.

Algorithm 4 DPLLo(∆, π): compiles CNF ∆ into OBDDπ

• 1: if there is an empty clause in ∆ then
• 2: return 0-sink
• 3: if there is no variable in ∆ then
• 4: return 1-sink
• 5: key = compute-key(∆)
• 6: if (result = cache-lookup(key)) ̸= null then
• 7: return result
• 8: x = first variable of order π that appears in ∆
• 9: result = get-node(x, DPLLo(∆|x=0, π), DPLLo(∆|x=1, π))
• 10: cache-insert(key, result)
• 11: return result

Note that our relaxation of Algorithm 3 has resulted in a new type of node, returned by get-and-node on Line 10. The old get-node function (Line 15) still returns decision nodes (in a relaxed sense, as their children now are not necessarily decision nodes) in the form of Figure 1c. The unique nodes technique can also be extended in a straightforward way so that isomorphic and-nodes will not be created.

We point out here that Algorithm 5 only produces sentences in a subset of d-DNNF, because it only produces a special type of disjunction nodes-decision nodes (again in the relaxed sense). Recall that d-DNNF allows any disjunction as long as the disjuncts are pairwise logically inconsistent. We will come back to this in the next subsection.

Static vs. Dynamic Decomposition. Algorithm 5 suggests a dynamic notion of decomposition, where disjoint components will be recognized after each variable split. This dynamic decomposition was initially proposed and utilized by [Bayardo and Pehoushek, 2000] for model counting and adopted by a more recent model counter [Sang et al., 2004]. [Darwiche, 2002; 2004] proposed another (static) method for performing the decomposition by preprocessing the CNF to generate a decomposition tree (dtree), which is a binary tree whose leaves correspond to the CNF clauses. Each node in the dtree defines a set of variables, whose instantiation is guaranteed to decompose the CNF into disjoint components. The rationale is that the cost of dynamically computing a partition (Line 5) many times during the search is now replaced with the lesser cost of computing a static and recursive partition once and for all. This method of decomposition allows one to provide structure-based computational guarantees as discussed later, and can be orders of magnitude more efficient on some benchmarks, including the ISCAS85 circuits. 3

3 One may obtain results to this effect by running the model counter [Sang et al., 2004], version 1.1, available at http://www.cs.washington.edu/homes/kautz/Cachet/, on benchmarks used in [Darwiche, 2004]. It should be noted that the two programs differ in other aspects, but the decomposition method appears to be the major difference. Note also that using DPLL for compilation incurs higher overhead than for model counting due to the bookkeeping involved in storing the DPLL trace.

Algorithm 5 DPLLd(∆): compiles CNF ∆ into d-DNNF

• 1: if there is an empty clause in ∆ then
• 2: return 0-sink
• 3: if there is no variable in ∆ then
• 4: return 1-sink
• 5: components = disjoint partitions of ∆
• 6: if |components| > 1 then
• 7: conjuncts = {}
• 8: for all ∆c ∈ components do
• 9: conjuncts = conjuncts ∪ {DPLLd(∆c)}
• 10: return get-and-node(conjuncts)
• 11: key = compute-key(∆)
• 12: if (result = cache-lookup(key)) ̸= null then
• 13: return result
• 14: select variable x of ∆
• 15: result = get-node(x, DPLLd(∆|x=0), DPLLd(∆|x=1))
• 16: cache-insert(key, result)
• 17: return result

Caching. Several caching methods have been proposed for d-DNNF compilation, the latest and most effective of which appeared in [Darwiche, 2004]. However, we refer the reader to [Darwiche, 2001b] for a caching scheme that is specific to the dtree-based decomposition method. This scheme is not competitive with the one in [Darwiche, 2004] in that it may miss some equivalences that would be caught by the latter, yet it allows one to show that the space and time complexity of dDNNF compilation is exponential only in the treewidth of the CNF formula (as compared to the pathwidth and cutwidth in OBDD compilation). Interestingly, no similar structure-based measure of complexity appears to be known for FBDDs.

Relation to AND/OR Search. Recent work has explored the long established notion of AND/OR search to process queries on belief and constraint networks [Dechter and Mateescu, 2004b; 2004a]. An AND/OR search is characterized by a search graph with alternating layers of and-nodes and decision-nodes, the former representing decomposition and the latter branching. The DAGs produced by Algorithm 5 are indeed AND/OR graphs and, conversely, the AND/OR search algorithms described in [Dechter and Mateescu, 2004b; 2004a] can be used to compile networks into the multi-valued equivalent of d-DNNF. This implies that these AND/OR search algorithms are capable of many more tasks than what they were proposed for-model counting (or other equivalent tasks such as computing the probability of a random variable assignment satisfying the constraint query). We discuss this further in the following subsection.

3.4 Understanding the Power and Limitations of DPLL

The main proposal in this paper has been the view of exhaustive-DPLL traces as sentences in some propositional language. This view provides a unified framework for knowledge compilation as we have shown earlier, but we now show another major benefit of this framework: By using known results about the succinctness and tractability of languages, one can understand better the intrinsic complexity and computational power of various exhaustive DPLL procedures.

Consider a particular variation of DPLL, say DPLLx, and suppose that its traces belong to language Lx. We then have:

1. DPLLx will not run in polynomial time on formulas for which no polynomial-size representation exists in Lx.
2. If DPLLx runs in polynomial time on a class of formulas, then DPLLx (with some trivial modification) can answer in polynomial time any query on these formulas that is known to be tractable for language Lx.

Take for example the model counters recently proposed in [Bayardo and Pehoushek, 2000; Sang et al., 2004], which employ the techniques of decomposition and (the latter also) caching. A simple analysis of these model counters shows that their traces are in the d-DNNF language (for specific illustrations, see the DDP algorithm of [Bayardo and Pehoushek, 2000] and Table 1 of [Sang et al., 2004]). Therefore, neither of these model counters will have a polynomial time complexity on formulas for which no polynomial-size representations exist in d-DNNF.

In fact, one can take this analysis one step further as follows. These model counters, and the compiler of [Darwiche, 2004], actually produce traces in a strict subset of d-DNNF, call it d-DNNF′ , which employs a syntactic notion of determinism; that is, every disjunction in their trace has the form (x ∧ α) ∨ (¬x ∧ β), where x is a splitting variable. The dDNNF language, however, does not insist on syntactic determinism: It allows disjunctions η ∨ψ where η ∧ψ is logically inconsistent, yet η and ψ do not contradict each other on any particular variable x. If d-DNNF′ turns out to be not as succinct as d-DNNF, then one may find another generation of model counters and d-DNNF compilers that can be exponentially more efficient than the current ones.

As an example of the second principle above, consider the query of testing whether the minimization of a theory ∆ implies a particular clause α, min(∆) |= α, where min(∆) is defined as a theory whose models are exactly the minimumcardinality models of ∆. This query is at the heart of diagnostic and nonmonotonic reasoning and is known to be tractable if ∆ is in d-DNNF. Therefore, this query can be answered in polynomial time for any class of formulas on which the model counters in [Bayardo and Pehoushek, 2000; Sang et al., 2004] have a polynomial time complexity. Similarly, a probabilistic equivalence test can be performed in polynomial time for formulas on which these models counters run in polynomial time.

Beyond DPLL. DPLL traces are inherently bound to be NNF sentences that are both deterministic and decomposable. Decomposability alone, however, is sufficient for the tractability of such important tasks as clausal entailment testing, existential quantification of variables, and cardinalitybased minimization [Darwiche and Marquis, 2002]. DPLL cannot generate traces in DNNF that are not in d-DNNF, since variable splitting (the heart of DPLL) amounts to enforcing determinism. It is this property of determinism that provides the power needed to do model counting (#SAT), which is essential for applications such as probabilistic reasoning. But if one does not need this power, then one should go beyond DPLL-based procedures; otherwise one would be solving a harder computational problem than is necessary.

4 Experimental Results

By way of experimentation, we compiled a set of CNF formulas into OBDD, FBDD and d-DNNF, both to show the practicality of the DPLL-based compilation approach and to relate the results to the theoretical succinct relations of the three languages. The benchmarks we used include random 3-CNF and graph coloring problems from [Hoos and St¨ utzle, 2000], and a set of ISCAS89 circuits. 4 The compilation was done with the OBDD compiler of [Huang and Darwiche, 2004], using the MINCE variable order [Aloul et al., 2001], an FBDD compiler we implemented according to Subsection 3.1 using the VSIDS variable ordering heuristic [Moskewicz et al., 2001], and the d-DNNF compiler of [Darwiche, 2004].

4 The CNF formulas used for these sequential circuits model the functionality of their combinational parts; they also define the transition relations of the circuits. Compilations of these theories will thus be useful, for example, for reachability analysis of the circuits.

The results of these experiments are shown in Table 2, where the running times are given in seconds based on a 2.4GHz CPU. The size of the compilation reflects the number of edges in the NNF DAG. A dash indicates that the compilation did not succeed given the available memory (4GB) and a 900-second time limit. It can be seen that for most of these propositional theories, the compilation was the smallest in d-DNNF, then FBDD, then OBDD; a similar relation can be observed among the running times. Also, the number of instances successfully compiled was the largest for d-DNNF, then FBDD, then OBDD. This tracks well with the theoretical succinctness relations of the three languages. (However, note that FBDD and d-DNNF are not canonical representations and therefore compilations smaller than reported here are perfectly possible; smaller OBDD compilations are, of course, also possible under different variable orderings.)

We close this section by noting that the implementations of these knowledge compilers bear witness to the advantage of the DPLL-based framework we have described. The first compiler is based on an existing SAT solver [Moskewicz et al., 2001], and the other two on our own implementation of DPLL, all three benefiting from techniques that have found success in SAT, including conflict analysis, clause learning, and data structures for efficient detection of unit clauses.

5 Conclusion

We established an important relationship between SAT and knowledge compilation, based on studying the trace of an exhaustive DPLL search. This relationship provides a uniform framework for compiling propositional theories into various languages of interest, and throws light on the intrinsic complexity and computational power of various DPLL-based algorithms. As interesting examples, we unveiled the "hidden power" of several recent model counters and discussed one of their potential limitations. We also pointed out the inability of exhaustive DPLL to produce traces in strict DNNF, which limits its power from a knowledge compilation point of view.

Acknowledgments

We thank the reviewers for commenting on an earlier version of this paper. This work has been partially supported by NSF grant IIS-9988543 and MURI grant N00014-00-1-0617.