A Perspective on Knowledge Compilation

1 Introduction

Knowledge compilation has emerged recently as a key direction of research for dealing with the computational intractability of general propositional reasoning [Darwiche, 1999a; Cadoli and Donini, 1997; Boufkhad et al., 1997; Khardon and Roth, 1997; Selman and Kautz, 1996; Schrag, 1996; Marquis, 1995; del Val, 1994; Dechter and Rish, 1994; Reiter and de Kleer, 1987]. According to this direction, a propositional theory is compiled off-line into a target language, which is then used on-line to answer a large number of queries in polytime. The key motivation behind knowledge compilation is to push as much of the computational overhead into the off-line phase, which is amortized over all on-line queries. But knowledge compilation can serve other important purposes as well. For example, target compilation languages and their associated algorithms can be very simple, allowing one to develop on-line reasoning systems for simple software and hardware platforms. Moreover, the simplicity of algorithms that operate on compiled languages help in streamlining the effort of algorithmic design into a single task: that of generating the smallest compiled representations possible, as that turns out to be the main computational bottleneck in compilation approaches.

There are three key aspects of any knowledge compilation approach: the succinctness of the target language into which the propositional theory is compiled; the class of queries that can be answered in polytime based on the compiled representation; and the class of transformations that can be applied to the representation in polytime. The AI literature has thus

Pierre Marquis

CRIL/Universit´e d'Artois F-62307, Lens Cedex, France marquis@cril.univ-artois.fr

far focused mostly on target compilation languages which are variations on DNF and CNF formulas, such as Horn theories and prime implicates. Moreover, it has focused mostly on clausal entailment queries, with very little discussion of tractable transformations on compiled theories.

The goal of this paper is to provide a broad perspective on knowledge compilation by considering a relatively large number of target compilation languages and analyzing them according to their succinctness and the class of queries/transformations that they admit in polytime.

Instead of focusing on classical, flat target compilation languages based on CNF and DNF, we consider a richer, nested class based on representing propositional sentences using directed acyclic graphs, which we refer to as NNF. We identify a number of target compilation languages that have been presented in the AI, formal verification, and computer science literature and show that they are special cases of NNF. For each such class, we list the extra conditions that need to be imposed on NNF to obtain the specific class, and then identify the set of queries and transformations that the class supports in polytime. We also provide cross-rankings of the different subsets of NNF, according to their succinctness and the polytime operations they support.

The main contribution of this paper is then a map for deciding the target compilation language that is most suitable for a particular application. Specifically, we propose that one starts by identifying the set of queries and transformations needed for their given application, and then choosing the most succinct language that supports these operations in polytime.

This paper is structured as follows. We start by formally defining the NNF language in Section 2, where we list a number of conditions on NNF that give rise to a variety of target compilation languages. We then study the succinctness of these languages in Section 3 and provide a cross-ranking that compares them according to this measure. We consider a number of queries and their applications in Section 4 and compare the different target compilation languages according to their tractability with respect to these queries. Section 5 is then dedicated to a class of transformations, their applications, and their tractability with respect to the different target compilation languages. We finally close in Section 6 by some concluding remarks. Proofs of theorems are omitted for space limitations but can be found in [Darwiche and Marquis, 2001].

2 The NNF Language

We consider more than a dozen languages in this paper, all of which are subsets of the NNF language, which is defined formally as follows [Darwiche, 1999a; 1999b].

Definition 2.1 Let PS be a finite set of prop. variables. A sentence in NNF CB is a rooted, directed acyclic graph (DAG) where each leaf node is labeled with D8D6D9CT, CUCPD0D7CT, CG or BMCG, CG BE CB; and each internal node is labeled with CM or CN and can have arbitrarily many children. The size of a sentence in NNF CB is the number of its DAG edges. Its height is the maximum number of edges from the root to some leaf in the DAG.

Figure 1 depicts a sentence in NNF, which represents the odd parity function (we omit reference to variables CB when no confusion is anticipated). Any propositional sentence can be represented as a sentence in NNF, so the NNF language is complete.

It is important here to distinguish between a representation language and a target compilation language. The former should be natural enough to enable one to encode knowledge directly, while the latter should be tractable enough to permit some polytime queries and/or transformations. We will consider a number of target compilation languages that do not qualify as representation languages from this perspective, as they are not suitable for humans to construct or interpret. We will also consider a number of representation languages that do not qualify as target compilation languages. 1

For a language to qualify as a target compilation language, we require that it permits a polytime clausal entailment test. Therefore, NNF does not qualify as a target compilation language (unless P=NP) [Papadimitriou, 1994], but many of its subsets do. We define a number of these subsets below, each of which is obtained by imposing further conditions on NNF.

We will distinguish between two key subsets of NNF: flat and nested subsets. We first consider flat subsets, which result from imposing combinations of the following properties:

• AF Flatness: The height of each sentence is at most 2. The sentence in Figure 4 is flat, but the one in Figure 1 is not.
• AF Simple-disjunction: The children of each or-node are leaves that share no variables (the node is a clause).
• AF Simple-conjunction: The children of each and-node are leaves that share no variables (the node is a term). The sentence in Figure 4 satisfies this property.

Definition 2.2 The language f-NNF is the subset of NNF satisfying flatness. The language CNF is the subset of fNNF satisfying simple-disjunction. The language DNF is the subset of f-NNF satisfying simple-conjunction.

CNF does not permit a polytime clausal entailment test and, hence, does not qualify as a target compilation language (unless P=NP). But its DNF dual does.

1 Admittedly, the notion of a representation language is not a formal one, yet the distinction is important. For example, we believe that when proposing target compilation languages in AI, there is usually an implicit requirement that the proposed language is also a representation language. As we shall see later, however, the most powerful target compilation languages are not suitable for humans to specify or interpret directly.

The following subset of CNF, prime implicates, has been quite influential in computer science:

Definition 2.3 The language PI is the subset of CNF in which each clause entailed by the sentence is subsumed by a clause that appears in the sentence; and no clause in the sentence is subsumed by another.

A dual of PI, prime implicants IP, can also be defined. 2

Definition 2.4 The language IP is the subset of DNF in which each term entailing the sentence subsumes some term that appears in the sentence; and no term in the sentence is subsumed by another term.

We now consider nested subsets of the NNF language, which do not impose any restriction on the height of a sentence. Instead, these subsets result from imposing one or more of the following conditions: decomposability, determinism, smoothness, decision, and ordering. We start by defining the first three properties. From here on, if BV is a node in an NNF, then CECPD6D7B4BVB5 denotes the set of all variables that label the descendants of node BV.

• AF Decomposability [Darwiche, 1999a; 1999b]. An NNF satisfies this property if for each conjunction BV in the NNF, the conjuncts of BV do not share variables. That is, if BV BD BN BM BM BM BNBV D2 are the children of and-node BV, then CECPD6D7B4BV CX B5 CK CECPD6D7B4BV CY B5 BP BN for CX BIBP CY. Consider the andnode marked in Figure 1(a). This node has two children, the first contains variables BTBNBU while the second contains variables BVBNBW. This and-node is then decomposable since the two children do not share variables. Each other and-node in Figure 1(a) is also decomposable and, hence, the NNF in this figure is decomposable.
• AF Determinism [Darwiche, 2000]: An NNF satisfies this property if for each disjunction BV in the NNF, each two disjuncts of BV are logically contradictory. That is, if BV BD BN BM BM BM BNBV D2 are the children of or-node BV, then BV CX CM BV CY CYBP CUCPD0D7CT for CX BIBP CY. Consider the or-node marked in Figure 1(b), which has two children corresponding to sub-sentences BMBT CM BU and BMBU CM BT. These two sub-sentences are logically contradictory. The ornode is then deterministic and so are the other or-nodes in Figure 1(b). Hence, the NNF in this figure is deterministic.
• AF Smoothness [Darwiche, 2000]: An NNF satisfies this property if for each disjunction BV in the NNF, each disjunct of BV mentions the same variables. That is, if BV BD BN BM BM BM BNBV D2 are the children of or-node BV, then CECPD6D7B4BV CX B5 BP CECPD6D7B4BV CY B5 for CX BIBP CY. Consider the marked or-node in Figure 1(c). This node has two children, each of which mentions variables BTBN BU. This or-node is then smooth and so are the other or-nodes in Figure 1(c). Hence, the NNF in this figure is smooth. 3

The properties of decomposability, determinism and smoothness lead to a number of interesting subsets of NNF.

2 Horn theories (and renamable Horn theories) represent another target compilation subset of CNF, but we do not consider it here since we restrict our attention to complete languages only.

3 Any sentence in NNF can be smoothed in polytime, while preserving decomposability and determinism. Preserving flatness, however, may blow-up the size of given NNF.

Definition 2.5 The language DNNF is the subset of NNF satisfying decomposability; d-NNF is the subset satisfying determinism; s-NNF is the subset satisfying smoothness; dDNNF is the subset satisfying decomposability and determinism; and sd-DNNF is the subset satisfying decomposability, determinism and smoothness.

Note that DNF is a strict subset of DNNF [Darwiche, 1999a; 1999b]. The following decision property comes from the literature on binary decision diagrams [Bryant, 1986].

Definition 2.6 (Decision) A decision node  in an NNF sentence is one which is labeled with D8D6D9CT, CUCPD0D7CT , or is an or-node having the form B4CG CM ABB5 CN B4BMCG CM ACB5, where CG is a variable, AB and AC are decision nodes. In the latter case, CSCECPD6B4B5 denotes the variable CG.

Definition 2.7 The language BDD is the subset of NNF, where the root of each sentence is a decision node.

The NNF sentence in Figure 2 belongs to the BDD subset.

The BDD language corresponds to binary decision diagrams (BDDs), as known in the formal verification literature [Bryant, 1986]. Binary decision diagrams are depicted using a more compact notation though: the labels D8D6D9CT and CUCPD0D7CT are denoted by BD and BC, respectively; and each decision node

X ¬X α β and and is denoted by α β X . The BDD sentence on the left of Figure 2 corresponds to the binary decision diagram on the right of Figure 2. Obviously enough, every NNF sentence that satisfies the decision property is also deterministic. Therefore, BDD is a subset of d-NNF.

As we show later, BDD does not qualify as a target compilation language (unless P=NP), but the following subset does.

Definition 2.8 FBDD is the intersection of DNNF and BDD.

That is, each sentence in FBDD is decomposable and satisfies the decision property. The FBDD language corresponds to free binary decision diagrams, as known in formal verification [Gergov and Meinel, 1994]. An FBDD is usually defined as a BDD that satisfies the read-once property: on each path from the root to a leaf, a variable can appear at most once. Read-once is equivalent to the decomposability of BDDs. 4

A more influential subset of the BDD language is obtained by imposing the ordering property:

Definition 2.9 (Ordering) Let BO be a total ordering on the variables PS. The language OBDD BO is the subset of FBDD satisfying the following property: if  and  are or-nodes, and if  is an ancestor of node , then CSCECPD6B4B5 BO CSCECPD6B4B5.

The OBDD BO language corresponds to the well-known ordered binary decision diagrams [Bryant, 1986].

The languages we have discussed so far are depicted in Figure 3, where arrows denote set inclusion. The figure contains one additional language that we have not discussed yet:

4 FBDDs are also known as read-once branching programs.

Definition 2.10 MODS is the intersection of sd-DNNF and DNF.

Figure 4 depicts a sentence in MODS. As we show later, MODS is the most tractable NNF subset we shall consider (together with OBDD BO ). This is not surprising since from the syntax of a sentence in MODS, one can immediately recover the sentence models.

3 On the Succinctness of Compiled Theories

We have discussed more than a dozen subsets of the NNF language. Some of these subsets are well known and have been studied extensively in the computer science literature. Others, such as DNNF [Darwiche, 1999b; 1999a] and d-DNNF [Darwiche, 2000], are relatively new. The question now is: What subset should one adopt for a particular application? As we argue in this paper, that depends on three key properties of the language: its succinctness, the class of tractable queries it supports, and the class of tractable transformations it admits.

Our goal in this and the following sections is to construct a map on which we place different subsets of the NNF language according to the above criteria. This map will then serve as a guide to system designers in choosing the target compilation language most suitable to their application. It also provides an example paradigm for studying and evaluating further target compilation languages. We start with a study of succinctness 5 in this section [Gogic et al., 1995].

Definition 3.1 (Succinctness) Let  BD and  BE be two subsets of NNF.  BD is at least as succinct as  BE , denoted  BD AK  BE , iff for every sentence AB BE  BE , there exists an equivalent sentence AC BE  BD where the size of AC is polynomial in the size of AB. 6

The relation AK is clearly reflexive and transitive, hence, a pre-ordering. One can also define the relation BO, where  BD BO  BE iff  BD AK  BE and  BE BIAK  BD .

Proposition 3.1 The results in Table 1 hold.

Figure 5 summarizes the results of Proposition 3.1 in terms of a directed acyclic graph.

A classical result in knowledge compilation states that it is not possible to compile any propositional formula AB into a polysize data structure AC such that: AB and AC entail the same set of clauses, and clausal entailment on AC can be decided in time polynomial in its size, unless NP AI P/poly [Selman and Kautz, 1996; Cadoli and Donini, 1997]. This last assumption implies the collapse of the polynomial hierarchy at the second level [Karp and Lipton, 1980], which is considered very unlikely. We use this classical result from knowledge compilation in some of our proofs of Proposition 3.1, which explains why some of its parts are conditioned on the polynomial hierarchy not collapsing.

5 A more general notion of space efficiency (model preservation for polysize reductions) exists [Cadoli et al., 1996], but we do not need its full generality here.

6 We stress here that we do not require that there exists a function that computes AC given AB in polytime; we only require that a polysize AC exists. Yet, our proofs in [Darwiche and Marquis, 2001] contain specific algorithms for computing AC from AB in certain cases.

We have excluded the subsets BDD, s-NNF, d-NNF and f-NNF from Table 1 since they do not qualify as target compilation languages (see Section 4). We kept NNF and CNF though given their importance. Consider Figure 5 which depicts Table 1 graphically. With the exception of NNF and CNF, all other languages depicted in Figure 5 qualify as target compilation languages. Moreover, with the exception of language PI, DNNF is the most succinct among all target compilation languages-we know that PI is not more succinct than DNNF, but we do not know whether DNNF is more succinct than PI.

In between DNNF and MODS, there is a succinctness ordering of target compilation languages:

DNNF is obtained by imposing decomposability on NNF; dDNNF by adding determinism; FBDD by adding decision; and OBDD BO by adding ordering. Adding each of these properties reduces language succinctness.

One important fact to stress here is that adding smoothness to d-DNNF does not affect its succinctness: the sd-DNNF and d-DNNF languages are equally succinct. It is also interesting to compare sd-DNNF (which is more succinct than the influential FBDD and OBDD BO languages) with MODS, which is a most tractable language. Both sd-DNNF and MODS are smooth, deterministic and decomposable. MODS, however, is flat and obtains its decomposability from the stronger condition of simple-conjunction. Therefore, sd-DNNF can be viewed as the result of relaxing from MODS the flatness and simple-conjunction conditions, while maintaining decomposability, determinism and smoothness. Relaxing these conditions moves the language three levels up the succinctness hierarchy, although it compromises only the polytime tests for entailment and equivalence as we show in Section 4.

4 Querying a Compiled Theory

In evaluating the suitability of a target compilation language to a particular application, the succinctness of the language must be balanced against the set of queries and transformations that it supports in polytime. We consider in this section a number of queries, each of which returns valuable information about a propositional theory, and then identify target compilation languages which provide polytime algorithms for answering such queries. 7

The queries we consider are tests for consistency, validity, implicates (clausal entailment), implicants, equivalence, and sentential entailment. We also consider counting and enumerating theory models. 8

From here on, L denotes a subset of language NNF.

Definition 4.1 (CO, VA) L satisfies CO (VA) iff there exists a polytime algorithm that maps every formula A6 from L to BD if A6 is consistent (valid), and to BC otherwise.

One of the main applications of compiling a theory is to enhance the efficiency of answering clausal entailment queries:

Definition 4.2 (CE) L satisfies CE iff there exists a polytime algorithm that maps every formula A6 from L and every clause AD from NNF to BD if A6 CYBP AD holds, and to BC otherwise.

A key application for clausal entailment is in testing equivalence. Specifically, suppose we have a design expressed as a set of clauses A1 CS BP CE CX AB CX and a specification expressed also as a set of clauses A1 D7 BP CE CY AC CY , and we want to test whether the design and specification are equivalent. By compiling each of A1 CS and A1 D7 to targets A0 CS and A0 D7 that support a polytime clausal entailment test, we can test the equivalence of A1 CS and A1 D7 in polytime. That is, A1 CS and A1 D7 are equivalent iff A0 CS CYBP AC CY for all CY and A0 D7 CYBP AB CX for all CX.

7 We restrict our attention in this paper to the existence of polytime algorithms for answering queries, but we do not present the algorithms themselves. The interested reader is referred to [Darwiche, 1999b; 2000; 1999a; Bryant, 1986] for some of these algorithms and to the proofs of theorems in [Darwiche and Marquis, 2001] for others.

8 One can also consider computing the probability of a propositional sentence, assuming that all variables are probabilistically independent. For the subsets we consider, however, this can be done in polytime whenever models can be counted in polytime.

A number of the target compilation languages we shall consider, however, support a direct polytime equivalent test:

Definition 4.3 (EQ, SE) L satisfies EQ (SE) iff there exists a polytime algorithm that maps every pair of formulas A6, A8 from L to BD if A6 AH A8 (A6 CYBP A8) holds, and to BC otherwise.

Note that sentential entailment (SE) is stronger than clausal entailment and equivalence. Therefore, if a language L satisfies SE, it also satisfies CE and EQ.

For completeness, we consider the following dual to CE:

Definition 4.4 (IM) L satisfies IM iff there exists a polytime algorithm that maps every formula A6 from L and every term AD from NNF to BD if AD CYBP A6 holds, and to BC otherwise.

Finally, we consider counting and enumerating models:

Definition 4.5 (CT) L satisfies CT iff there exists a polytime algorithm that maps every formula A6 from L to a nonnegative integer that represents the number of models of A6 (in binary notation).

Definition 4.6 (ME) L satisfies ME iff there exists a polynomial D4B4BMBN BMB5 and an algorithm that outputs all models of an arbitrary formula A6 from L in time D4B4D2BND1B5, where D2 is the size of A6 and D1 is the number of its models (over variables occurring in A6).

Proposition 4.1 The results in Table 2 hold.

The results of Proposition 4.1 are summarized in Figure 3. One can draw a number of conclusions based on the results in this figure. First, NNF, s-NNF, d-NNF, f-NNF, and BDD fall in one equivalence class that does not support any polytime queries and CNF satisfies only VA and IM; hence, none of them qualifies as a target compilation language in this case. But the remaining languages all support polytime tests for consistency and clausal entailment. Therefore, simply imposing either of smoothness (s-NNF), determinism (d-NNF), flatness (f-NNF), or decision (BDD) on the NNF language does not lead to tractability with respect to any of the queries we consider-neither of these properties seem to be significant in isolation. Decomposability (DNNF), however, is an exception and leads immediately to polytime tests for both consistency and clausal entailment, and to a polytime algorithm for model enumeration.

Recall the succinctness ordering DNNF BO d-DNNF BO FBDD BO OBDD BO BO MODS from Figure 5. By adding decomposability (DNNF), we obtain polytime tests for consistency and clausal entailment, in addition to a polytime model enumeration algorithm. By adding determinism to decomposability (d-DNNF), we obtain polytime tests for validity, implicant and model counting, which are quite significant. It is not clear, however, whether the combination of decomposability and determinism leads to a polytime test for equivalence. Moreover, adding the decision property on top of decomposability and determinism (FBDD) does not appear to increase tractability with respect to the given queries 9 , although it does lead to reducing language succinctness as shown in Figure 5. On the other hand, adding the ordering property on top of decomposability, determinism and decision (OBDD BO ), leads to polytime tests for sentential entailment and equivalence.

As for the succinctness ordering NNF BO DNNF BO DNF BO IP BO MODS from Figure 5, note that DNNF is obtained by imposing decomposability on NNF, while DNF is obtained by imposing flatness and simple-conjunction (which is stronger than decomposability). What is interesting is that DNF is less succinct than DNNF, yet does not support any more polytime queries; see Figure 3. However, the addition of smoothness on top of flatness and simple-conjunction (MODS) leads to five additional polytime queries, including equivalence and entailment tests. 10

We close this section by noting that determinism appears to be necessary (but not sufficient) for polytime model counting: only deterministic languages, d-DNNF, sd-DNNF, FBDD, OBDD BO and MODS, support polytime counting. Moreover, polytime counting implies a polytime test of validity, but the opposite is not true.

9 Deciding the equivalence of two sentences in FBDD, d-DNNF, or in sd-DNNF, can be easily shown to be in coNP. However, we do not have a proof of coNP-hardness, nor do we have deterministic polytime algorithms for deciding these problems. Actually, the latter case is quite unlikely as the equivalence problem for FBDD has been intensively studied, with no such algorithm in sight. Note, however, that the equivalence of two sentences in FBDD can be decided probabilistically in polytime [Blum et al., 1980].

10 Formally, we also need determinism to obtain MODS (see Definition 2.10). But given flatness, simple-conjunction and smoothness, we can obtain determinism by simply removing duplicated terms.

5 Transforming a Compiled Theory

A query is an operation that returns information about a theory without changing it. A transformation, on the other hand, is an operation that returns a modified theory, which is then operated on using queries. Many applications require a combination of transformations and queries.

Definition 5.1 ( CMBVBN CNBV) L satisfies CMBV (CNBV) iff there exists a polytime algorithm that maps every finite set of formulas A6 BD BN BM BM BM BNA6 D2 from L to a formula of L that represents A6 BD CM A1 A1 A1 CM A6 D2 (A6 BD CN A1 A1 A1 CN A6 D2 ).

Definition 5.2 (BMBV) L satisfies BMC iff there exists a polytime algorithm that maps every formula A6 from L to a formula of L that represents BMA6.

If a language satisfies one of the above properties, we will say that it is closed under the corresponding operator. Closure under logical connectives is important for two key reasons. First, it has implications on how compilers are constructed for a given target language. For example, if a clause can be easily compiled into some language , then closure under conjunction implies that compiling a CNF sentence into L is easy. Second, it has implications on the class of polytime queries supported by the target language: If a language  satisfies CO and is closed under negation and conjunction, then it must satisfy SE (to test whether A1 CYBP A0, all we have to do, by the Refutation Theorem, is test whether A1 CM BMA0 is inconsistent). Similarly, if a language satisfies VA and is closed under negation and disjunction, it must satisfy SE by the Deduction Theorem.

It is important to stress here that some languages are closed under a logical operator, only if the number of operands is bounded by a constant. We will refer to this as boundedclosure.

Definition 5.3 (CMBUBVBN CNBUBV) L satisfies CMBUBV (CNBUBV) iff there exists a polytime algorithm that maps every pair of formulas A6 and A8 from L to a formula of L that represents A6CMA8 (A6 CN A8).

We now turn to another important transformation:

Definition 5.4 (Conditioning) [Darwiche, 1999a] Let A6 be a propositional formula, and let AD be a consistent term. The conditioning of A6 on AD, noted A6 CY AD, is the formula obtained by replacing each variable CG of A6 by true (resp. false) if CG (resp. BMCG) is a positive (resp. negative) literal of AD.

Definition 5.5 (CD) L satisfies CD iff there exists a polytime algorithm that maps every formula A6 from L and every consistent term AD to a formula from L that represents A6 CY AD.

Conditioning has a number of applications, and corresponds to restriction in the literature on Boolean functions. The main application of conditioning is due to a theorem, which says that A6CMAD is consistent iff A6 CY AD is consistent [Darwiche, 1999b; 1999a]. Therefore, if a language satisfies CO and CD, then it must also satisfy CE. Conditioning also plays a key role in building compilers that enforce decomposability. If two sentences A1 BD and A1 BE are both decomposable (belong to DNNF), their conjunction A1 BD CMA1 BE is not necessarily decomposable since the sentences may share variables. Conditioning can be used to ensure decomposability in this case since A1 BD CMA1 BE is equivalent to CF AD B4A1 BD CY ADB5 CM B4A1 BE CY ADB5 CM AD, where AD is a term covering all variables shared by A1 BD and A1 BE . Note that CF AD B4A1 BD CY ADB5 CM B4A1 BE CY ADB5 CM AD must be decomposable since A1 BD CY AD and A1 BE CY AD do not mention variables in AD. The previous proposition is indeed a generalization to multiple variables of the well-known Shannon expansion in the literature on Boolean functions. It is also the basis for compiling CNF into DNNF [Darwiche, 1999a; 1999b].

Another critical transformation we shall consider is that of forgetting [Lin and Reiter, 1994]:

Definition 5.6 (Forgetting) Let A6 be a propositional formula, and let CG be a subset of variables from PS. The forgetting of CG from A6, denoted BLCGBMA6, is a formula that does not mention any variable from X and for every formula AB that does not mention any variable from X, we have A6 CYBP AB precisely when BLCGBMA6 CYBP AB.

Therefore, to forget variables from X is to remove any reference to X from A6, while maintaining all information that A6 captures about the complement of X. Note that BLCGBMA6 is unique up to logical equivalence.

Definition 5.7 (FO, SFO) L satisfies FO iff there exists a polytime algorithm that maps every formula A6 from L and every subset CG of variables from PS to a formula from L equivalent to BLCGBMA6. If the property holds for singleton X, we say that L satisfies CBBY.

Forgetting is an important transformation as it allows us to focus/project a theory on a set of variables. For example, if we know that some variables CG will never appear in entailment queries, we can forget these variables from the compiled theory while maintaining its ability to answer such queries correctly. Another application of forgetting is in counting/enumerating the instantiations of some variables Y, which are consistent with a theory A1. This query can be answered by counting/enumerating the models of BLCGBMA1, where X is the complement of Y. Forgetting also has applications to planning, diagnosis and belief revision. For instance, in the SATPLAN framework, compiling away fluents or actions amounts to forgetting variables. In model-based diagnosis, compiling away every variable except the abnormality ones does not remove any piece of information required to compute the conflicts and the diagnoses of a system [Darwiche, 1999b]. Forgetting has also been used to design update operators with valuable properties [Herzig and Rifi, 1999].

Proposition 5.1 The results in Table 3 hold.

One can draw a number of observations regarding Table 3. First, all languages we consider satisfy CD and, hence, lend themselves to efficient application of the conditioning transformation. As for forgetting multiple variables, only DNNF, DNF, PI and MODS permit that in polytime. It is important to stress here that neither FBDD nor OBDD BO permit polytime forgetting of multiple variables. This is noticeable since some of the recent applications of OBDD BO to planning depends crucially on the operation of forgetting and it may be more suitable to use a language that satisfies FO in this case. Note, however, that OBDD BO allows the forgetting of a single variable in polytime, but FBDD does not allow even that. dDNNF is similar to FBDD as it satisfies neither FO nor SFO.

It is also interesting to observe that none of the target compilation languages is closed under conjunction. A number of them, however, are closed under bounded-conjunction, including OBDD BO , DNF, IP and MODS.

As for disjunction, the only target compilation languages that are closed under disjunction are DNNF and DNF. The OBDD BO and PI languages, however, are closed under bounded disjunction. Again, the d-DNNF and FBDD languages are closed under neither.

The only target compilation languages that are closed under negation are FBDD and OBDD BO , while it is not known whether d-DNNF or sd-DNNF are closed under this operation. Note that d-DNNF and FBDD support the same set of polytime queries (equivalence checking is unknown for both) so they are indistinguishable from that viewpoint. Moreover, the only difference between the two languages in Table 3 is the closure of FBDD under negation, which does not seem to be that significant in light of no closure under either conjunction or disjunction. Note, however, that d-DNNF is more succinct than FBDD as given in Figure 5.

Finally, OBDD BO is the only target compilation language that is closed under negation, bounded conjunction, and bounded disjunction. This closure actually plays an important role in compiling propositional theories into OBDD BO and is the basis of state-of-the-art compilers for this purpose [Bryant, 1986].

6 Conclusion

The main contribution of this paper is a methodology for analyzing propositional compilation approaches according to two key dimensions: the succinctness of the target compilation language, and the class of queries and transformations it supports in polytime. The second main contribution of the paper is a comprehensive analysis, according to the proposed methodology, of more than a dozen languages for which we have produced a knowledge compilation map, which crossranks these languages according to their succinctness, and the polytime queries and transformations they support. This map allows system designers to make informed decisions on which target compilation language to use: after the class of queries/transformations have been decided based on the application of interest, the designer chooses the most succinct target compilation language that supports such operations in polytime. Another key contribution of this paper is the uniform treatment we have applied to diverse target compilation languages, showing how they all are subsets of the NNF language. Specifically, we have identified a number of simple, yet meaningful, properties, including decomposability, determinism, decision and flatness, and showed how combinations of these properties give rise to different target compilation languages. The studied subsets include some well known languages such as PI, which has been influential in AI; OBDD BO , which has been influential in formal verification; and CNF and DNF, which have been quite influential in computer science. The subsets also include some relatively new languages such as DNNF and d-DNNF, which appear to represent interesting, new balances between language succinctness and query/transformation tractability.

Acknowledgements

We wish to thank Ingo Wegener for his help with some of the issues discussed in the paper. This work has been done while the second author was a visiting researcher with the Computer Science Department at UCLA. The first author has been partly supported by NSF grant IIS-9988543 and MURI grant N00014-00-1-0617. The second author has been partly supported by IUT de Lens and the R´egion Nord/Pas-de-Calais.