Compiling Knowledge into Decomposable Negation Normal Form

1 Introduction

Compiling propositional theories has emerged as a new technique for enhancing the computational efficiency of automated reasoning systems. The basic idea here is to split the computational effort of such systems into two phases, off-line and on-line. In the off-line phase, a propositional theory is compiled into a tractable form which is then used in an on-line phase to answer multiple queries. The main value of such compilation is that most of the computational overhead is shifted into the off-line phase, which is amortized over all on-line queries.

One of the key approaches for compiling propositional theories has been proposed in [7]. Here, a propositional theory is compiled in an off-line phase into a Horn the­ ory, which is used in an on-line phase to answer multiple queries. As it is not always possible to compile a propo­ sitional theory into a Horn theory, the propositional the­ ory is generally compiled into two Horn theories, which approximate the original theory from below and above in terms of logical strength.

In this paper, we propose to compile propositional the­ ories into a new form, which we call decomposable nega­ tion normal form (DNNF). This form is a generalization of disjunctive normal form (DNF) and a specialization of negation normal form (NNF) [1]. DNNF is tractable as the satisfiability of theories expressed in DNNF can be decided in linear time. In fact, a number of other inter­ esting reasoning tasks, such as forgetting [6), can also be performed in linear time on theories expressed in DNNF.

We show a number of results about our compilation approach. First, contrary to compilations into Horn the­ ories, we show that every propositional theory can be compiled into DNNF and present an algorithm to this effect. Second, we show that if a clausal form has a bounded treewidth, then it has a linear DNNF com­ pilation which can be computed in linear time. Here, treewidth is a graph-theoretic parameter which measures the connectivity of a given clausal form. Even when the clausal form does not have a bounded treewidth, we show that its DNNF compilation is exponential only in its treewidth and linear in all other aspects. Finally, we present two techniques for approximating the DNNF compilation of a propositional theory in case such com­ pilation is too large to be practical. One of the tech­ niques generates a sound but incomplete compilation, while the other generates a complete but unsound com­ pilation. Together, these approximations bound the ex­ act compilation from below and above in terms of their ability to answer queries.

This paper is structured as follows. Section 2 in­ troduces DNNF and its various properties. Section 3 discusses the compilation of propositional theories into DNNF. Section 4 discusses the two techniques for ap­ proximating a DNNF compilation and Section 5 focuses on the operation of forgetting. Finally, Section 6 closes with some concluding remarks . Proofs of theorems can be found in the long version of the paper [4].

2 Decomposable NNF

A propositional sentence is in negation normal form (NNF) if it is constructed from literals using only the conjoin and disjoin operators [1]. Figure 1 shows a sen­ tence in NNF depicted as a rooted, directed acyclic graph where the children of each node are shown below it in the graph. Each leaf node represents a literal and each non-leaf node represents a conjunction or a disjunction. We will also allow true and ·false to appear as leaves in a DNNF to denote a conjunction with no conjuncts. Similarly, we will allow false and ·true as leaves to rep­ resent a disjunction with no disjuncts. The size of an NNF is measured by the number of edges in its graph­ ical representation. Note that every disjunctive normal form (DNF) is an NNF, and that every conjunctive nor­ mal form (CNF) is an NNF. There are NNFs, however, that are neither DNFs nor CNFs.

Our concern here is mainly with a subclass of NNFs:

Definition 1 A decomposable negation normal form (DNNF) is a negation normal form satisfying the decom­ posability property: for any conjunction /\ ;a; appearing in the form, no atoms are shared by the conjuncts a;.

The NNF in Figure 1 is decomposable. It has ten con­ junctions and the conjuncts .of each share no atoms. Decomposability is the property which makes DNNF tractable. We will explore this property at length later, but we first note that every DNF is also a DNNF. 1 Therefore, all properties that we shall prove of DNNFs also hold for DNFs. A question that may arise then is why not compile propositional theories into DNFs? As it turns out, there are propositional theories that have linear DNNF representations, yet exponential DNF rep­ resentations. For example, consider a propositional the­ ory .6. over n atoms, which is satisfied exactly by models in which an odd number of atoms is set to true (.6. repre­ sents the odd-parity function) . The DNF representation of this theory is known to be exponential inn. However, the theory has a DNNF representation which is linear in n. Figure 1 depicts such representation for n = 4.

Propositional theories in DNNF are tractable:

1 We assume that in the DNF a 1 V ... V ctn, no atoms are shared by the literals in Lti.

1. Deciding the satisfiability of a DNNF can be done in linear time.
2. Forgetting about some atoms in a DNNF can be done in linear time [6].
3. Computing the minimum cardinality of models that satisfy a DNNF can be done in linear time, where cardinality is the number of atoms that are set to true (or false) by the model [3].

The last task has applications to model-based diagnosis and is outside the scope of this paper. Our focus here will be on the first two tasks, which we consider next.

By a clause (over distinct atoms p1 , .. . , Pn), we will mean a disjunction l1 V ... V ln, where l; is either p; or ·p;. By an instantiation (of distinct atoms p1 , ... ,Pn), we will mean a conjunction l1 1\ ... 1\ ln . We start with a linear test for deciding the satisfiability of NNFs.

Definition 2 Let SAT? be a predicate over NNFs de­ fined as follows. SAT?(l) is true where l is a literal. SAT?(/\; a;) is true iff each SAT?(a;) is true. SAT?(V; a;) is true iff some SAT?(a;) is true.

It should be clear that the predicate SAT?(a) can be evaluated in time which is linear in the size of NNF a. The previous test is sound and complete for DNNFs:

Theorem 1 DNNF a is satisfiable iff SAT?(a) is true.

Now that we have a satisfiability test, we can also define an entailment test. Specifically, to test whether a entails clause (3, we only need to test whether a 1\ ·fJ is satisfiable. Note, however , that even though both a and ·fJ may be in DNNF, their conjunction a 1\ · fJ is not guaranteed to be in DNNF as a and ·fJ may share atoms. This can be easily dealt with, however, using the notion of conditioning:

Definition 3 Let a be a propositional sentence and let r be an instantiation. The conditioning of a on"(, written a I r, is the sentence which results from replacing each atom p in a with true if the positive literal p appears in r and with false if tha negative literal ·p appears in r.

For example, conditioning the DNNF ( ·AI\ ·B) V (B /\C) on instantiation B 1\D gives ( ·AI\ ·true) V (true /\C) and conditioning it on ·BI\D gives (·AI\·false)V(falsei\C). Conditioning allows us to eliminate reference to atoms while preser.:ving satisfiability:

Theorem 2 For DNNF a and instantiation,, aIr is in DNNF, and a I r is satisfiable iff a 1\ r is satisfiable.

Therefore, to test whether DNNF a entails clause (3, we only need to test whether a I ·fJ is satisfiable, which is guaranteed to be in DNNF. We can now define a lin­ ear entailment test for DNNFs. Actually, we will (more generally) define it for NNFs:

Definition 4 For NNF a and clause (3, define af--(3 to be true when SAT?(a I ·fJ) is false, where ·fJ is the in­ stantiation negating clause (3 .

This linear test is both sound and complete for DNNFs: Theorem 3 For DNNF a and clause (3, af--(3 iff a f= (3.

Consider the DNNF a in Figure 1, the clause (3 = ·A V ·B V --,C V ·D, and suppose we want to test whether a f= (3. Theorem 3 suggests that we condition a on ·f3, to yield a I ·f3, and then test whether SAT?(a I ·f3) is false. Figure 2 depicts the conditioning of a on ·f3 and the result of applying the SAT? test. Since SAT?(a I ·f3) is false, we conclude af-(3 and also a f= (3.

Before we close this section, we present three impor­ tant results on DNNF entailment. First, that the entail­ ment test f- is sound with respect to sentences in NNF:

Theorem 4 For NNF a, af-(3 only if a f= (3.

That is, even though a may not be decomposable, the entailment test f- is still sound, but not necessarily com­ plete. Even completeness of this test, however, can be guaranteed under the following condition.

Definition 5 NNF a is decomposable except on atoms X iff for any conjunction 1\i f3i that appears in a, only atoms in X are shared by the conjuncts f3i.

For example, the NNF (·A V B) 1\ ( ·B V C) is decom­ posable except on B.

Theorem 5 Let a be an NNF which is decomposable except on X. Let (3 be a clause which mentions all atoms in X. Then af-(3 iff a f= (3.

Consider the NNF a = (·A V B) 1\ ( ·B V C) and the queries A-:JB, B-:JA and A-:JC. Since a is decompos­ able except on B, the test f- is sound and complete with respect to the first two queries but is only sound with respect to the third query. Partial decomposability is extremely important in practice since the less decompos­ able a sentence is, the smaller its size will be. Finally:

Theorem 6 For NNF a, which is decomposable except on X, and for clause (3, a f= (3 iff af-/i V (3 for each clause /i over atoms appearing in X but not in (3.

Therefore, if the size of X is bounded by a constant, then a f= (3 can be decided in linear time for any query (3, even though a itself is not decomposable.

3 Compiling Knowledge into DNNF

We established two main results in the previous section. First, we identified the class of DNNF theories. Second, we showed that satisfiability and entailment can be de­ cided in linear time with respect to DNNF theories. Our goal in this section is two fold. First, to prove that every propositional theory can be expressed in DNNF. Second, to provide an algorithm for this purpose.

The following theorem is the key to proving that every propositional theory can be converted into DNNF.

Theorem 7 Let ~1 and ~2 be two propositional sen­ tences in DNNF. Let ~ be the sentence V 13 (~1 I (3) 1\ ( ~2 I (3) 1\ (3, where (3 is an instantiation of all atoms shared by ~1 and ~2 . Then ~ is in DNNF and ~ is equivalent to ~1 1\ ~2.

Here is a recursive algorithm DNNFl(~), based on the above theorem, which converts any clausal form ~ into an equivalent theory in DNNF:

1. If~ contains a single clause a, DNNFl(~)+-a.
2. Otherwise, DNNFl(~)+- V /3 DNNF1(~ 1 (3) 1\ DNNF1(~2 I (3) 1\ (3, where ~1 and ~2 is a parti­ tion of the clauses in ~' and (3 is an instantiation of the atoms shared by ~1 and ~2.

This algorithm converts any theory in clausal form into an equivalent theory in DNNF, but at the expense of increasing the theory size. The increase in size comes mainly from the case analysis performed on the atoms shared by the sub-theories ~1 and ~2 . Consider the theory ~ = (A-:JB) 1\ (B-:JC) and let ~1 = A-:JB and ~2 = B-:JC. Then DNNFl(~) = (DNNF1(~ 1 I B) 1\ DNNF1(~2 I B)(\ B) v (DNNF1(~1 I ·B)(\ DNNF1(~2 I ·B) 1\ ·B), which simplifies to ( C 1\ B) V (·A 1\ ·B).

We have two key observations about the above proce­ dure. First, the size of resulting DNNF is very sensitive to the way we split the theory~ into two sub-theories ~1 and ~2 . Second, the above procedure is not determinis­ tic since it does not specify how to split the theory~ into two sub-theories. To make the procedure deterministic, we will utilize a decomposition tree, which represents a recursive partitioning of the clauses in ~.

Definition 6 A decomposition tree T for clausal form ~ is a full binary tree whose leaves correspond to the clauses in ~. If N is the leaf node corresponding to clause a in~~ then ~(N)d~ {a}.

Figure 3 depicts a decomposition tree for the theory 6. which contains the clauses A:JB, B:JC and C:JD.

For a decomposition tree to be useful computationally, we need to associate some information with each of its nodes. First, for every internal node N: N1 and Nr de­ note the left and right children of N, respectively, and

6.(N)d,;j 6.(Nt)U6.(Nr)· Second, atoms(N) is defined as the set of atoms appearing in clauses 6.(N). For exam­ ple, in Figure 3, 6.(n2 ) contains the clauses A:JB and B:JC and atoms(n2 ) contains the atoms A, B and C.

Given a decomposition tree for theory 6. , Figure 4 depicts an algorithm which compiles 6. into DNNF.

Theorem 8 DNNFl(N, a) returns 6.(N) I a in DNNF.

Therefore , to convert a theory 6. into DNNF, we first construct a decomposition tree T for 6. and call DNNFl(N, true) with N being the root of tree T. The following is an important observation about DNNFl:

Theorem 9 If a and a' agree on atoms(N), then DNNFl(N, a) is equivalent to DNNFl(N, a').

Therefore, . we can improve on DNNFl by associat­ ing a cache with each node N to store the result of DNNFl(N, a) indexed by the projection of instantiation a on atoms(N), denoted project(a, atoms(N)). When another recursive call DNNFl(N, a') is made, we first check the cache of node N to see whether we have an entry for project(a', atoms(N)). If we do, we return it. Otherwise, we continue with the recursion. This im­ provement leads to the refined algorithm in Figure 5.

We now address the complexity of DNNF2.

Definition 7 Let N be a node in a decomposition tree T. The cluster of node N is defined as follows:

• If N is a leaf node, then its cluster is atoms ( N).
• If N is an internal node, then its cluster is the set of atoms that appear either
• above and below node N in the tree; or
• in the left and right subtrees of node N.

The width of a decomposition tree is the size of its max­ imal cluster minus one.

In Figure 3, we have cluster(nl) = { C}, cluster(n2 ) = {B,C}, cluster(n3) = {A,B}, cluster(n4 ) = {B,C} and cluster(n5) = {C, D}. Therefore, the decomposition tree has width 1.

Theorem 10 Let T be the decomposition tree used in Figure 5. The time and space complexity of the algorithm in Figure 5 is O(nw2w), where n is the number of leaf nodes in tree T and w is its width. 2

Therefore, the complexity of compiling a propositional theory into DNNF depends crucially on the quality (width) of decomposition tree used. The question now is how to construct good decomposition trees (ones with small width)? As it turns out, there is a device in the literature on graph-based reasoning, known as ajointree, which can be easily converted into a decomposition tree. A jointree also has a width and good jointrees are those with small width. We can easily convert a jointree into a decomposition tree while maintaining its width. There­ fore, any good method for constructing jointrees is also a good method for constructing decomposition trees. A jointree, however, is constructed for an undirected graph while a decomposition tree is constructed for a proposi­ tional theory. The following definition makes the con­ nection.

Definition 8 [5} Let 6. be a propositional theory in clausal form. The interaction graph for 6. is the undi­ rected graph G constructed as follows. The nodes of G are the atoms of 6. . There is an edge between two atoms in G iff the atoms appear in the same clause of 6..

Theorem 11 Let 6. be a propositional theory in clausal form and let G be its interaction graph. Let J be a join­ tree for G with width w. There is a decomposition tree for 6. which has width < w and which can be constructed from J in time linear ~ the size of J.

The width of the best jointree for a graph G is known as the treewidth of G. If the treewidth of a graph is bounded by a constant w, then one can construct an op­ timal jointree in linear time [2]. A major implication of this result is that if a clausal form 6. has an interaction graph with a bounded treewidth, then (a) computing an optimal decomposition tree (jointree) for that the­ ory, (b) compiling the theory based on the computed decomposition tree, and (c) answering queries based on the resulting compilation, can all be done in linear time. This is our central result on the complexity of compiling theories into DNNF. 3

2 Note that if T is a decomposition tree for a clausal form ll., then n is also the number of clauses in fl..

We stress, however, that the interaction graph of a theory may not have a bounded treewidth, yet the the­ ory may have a polynomial compilation into DNNF. Consider the theory 6. = {P1 1\ . .. 1\ Pn"JQ,Rl 1\ ·Pt"JQ, ... , Rn 1\ ·Pn"JQ}. The interaction graph of this theory has treewidth n, yet it has a DNNF compi­ lation of size O(n 2 ) (shown in Figure 6 for n = 3).

The theory we just considered is not equivalent to any Horn theory. In fact, even its Horn approximation is known to be exponential in n [7]. This shows that there are theories with exponential Horn approximations, yet polynomial DNNF representations.

4 Approximate Compilation

What if we have a theory 6. for which the best decom­ position tree has an unacceptable width? We have two key choices to address this problem. First, we can try to improve on algorithm DNNF2. Second, we can try to gen­ erate an approximate compilation, which is the direction we shall peruse in this section.

Consider the algorithm DNNF2 in Figure 5. It should be clear that the reason for possible intractability in this algorithm is the size of S(N, o/~ atoms(Nt) n atoms(Nr)- atoms( a), which contains some of the atoms shared by sub-theories 6.(N1) and 6.(Nr)· Specifically, the algorithm will consider a number of instantiations f3 which is exponential in the size of S(N, a). Therefore, we can control the size of resulting compilation by re­ ducing the number of instantiations considered. We can do this in two ways:

1. Ignoring atoms: We can ignore some of the atoms in S(N, a) by performing a case analysis on only a subset of S(N, a). That is, we consider all instan-

3 The satisfiability of this class of theories can also be de­ cided in linear time using directional resolution [5].

• tiations f3 of a subset of S(N, a) . This leads to a variation on algorithm DNNF2 which we call DNNFu.
• Ignoring instantiations: We can ignore some of the instantiations (3. That is, we only consider some instantiations f3 of S(N, a). This leads to a variation on algorithm DNNF2 which we call DNNF1.

In either case, we can control the size of resulting com­ pilation and to the degree we wish. In fact, using either technique we can ensure a linear compilation if we decide to ignore enough atoms or instantiations. This leaves two questions. First, what atoms or instantiations should we ignore? Second, what can we guarantee about the re­ sulting compilations?

The choice of atoms or instantiations to ignore is typ­ ically heuristic and will not be addressed in this paper. We only address the second question here.

Theorem 12 DNNFu(N, a) is in NNF and is equivalent to DNNF2(N,a).

That is, ignoring atoms preserves equivalence to the ex­ act compilation, but compromises the decomposability property. The more atoms we ignore, the less decom­ posable the approximation is. But in all cases, the com­ pilation generated by DNNFu is sound, although not nec­ essarily complete, with respect to entailment.

Corollary 1 DNNFu(N, a)f-(3 only if DNNF2(N, a)f-(3 .

Here is the guarantee about the second approximation:

Theorem 13 DNNF1(N, a) is in DNNF and DNNF1(N,a) f= DNNF2(N,a) .

That is, ignoring instantiations preserves the decompos­ ability property but could lead to strengthening the com­ pilation. The more instantiations we ignore, the stronger the approximate compilation is. But in all cases , the compilation generated by DNNF1 is complete, although not necessarily sound, with respect to entailment.

Corollary 2 DNNF1(N,a) 'f(J only ijDNNF2(N,a) 'f(J.

Therefore, if the size of a DNNF compilation r is too large, we can replace it with two approximations f 1 and r u· Given a query (3, we first test whether f 1f-(J and r uf-fJ. We have three possibilities: If f1 'j-(3, then 6. ~ f3. H r uf-!3, then 6. F= fJ. H ftf-!3 and r u ;f-!3, then the approximations are not good enough to answer this query. Note that the case ft 'f(J and r uf-fJ is impossible.

The bounds f 1 and r u are inspired by the lower and upper Horn approximations proposed in [7]. In their approach, however , these bounds are crucial since not every theory has a Horn representation. In our case, however, the approximations are only meant to address intractability; our compilation approach would continue to be meaningful without them.

5 Compiling Out Atoms

Given a theory 6., we may only be interested in queries (3 which do not mention atoms X . In this case, it makes sense to compile 6. into a theory which does not mention atoms X either, yet is equivalent to 6. with respect to queries {3. Such theory is the result of forgetting about atoms X in ~ [6]. As it turns out, once a theory is converted into DNNF, forgetting takes linear time:

Definition 9 For DNNF a and atoms X, define FORGET( a, X) as the result of replacing each literal in a with true iff that literal refers to an atom in X.

The following theorem shows that the above linear op­ eration does correspond to forgetting as defined in [6] :

Theorem 14 Let a be a sentence in DNNF and let f3 be a clause that does not mention atoms X. Then a p f3 iff FORGET( a, X) p {3.

Consider the DNNF in Figure 6, which is equiva­ lent to the theory ~ = { P1 1\ P2 1\ P3 -::>Q, R1 1\ -.P1-::>Q,R2 1\ ·P2-::>Q,R3 1\ -.P3-::>Q}. Forgetting about atoms P1, P2 , P3 in this theory gives the DNNF in Fig­ ure 7, which can be easily simplified to R1 I\R2 I\R3-::>Q.

Forgetting has three major applications. First, re­ ducing the size of a DNNF compilation by forgetting about atoms that would never appear in queries. Second, computing DNNF representations of Boolean functions . Consider the circuit in Figure 8 which implements the odd-parity function, and let ~ be a theory representing this circuit. If we compile ~ U { G} into DNNF, and then forget atoms E, F and G, we obtain a DNNF represen­ tation of this Boolean function. This technique can be used to compile any circuit representation of a Boolean function into its DNNF representation. 4 A final applica­ tion of forgetting is in computing the implications of a given theory on a particular set of atoms X (by forget­ ting about all atoms other than X). This has proven to be very useful in model- based diagnosis [3].

6 Conclusion

We have proposed an approach for compiling proposi­ tional theories into a tractable form, which we refer to as decomposable negation normal form (DNNF) . We have shown that once a theory is compiled into that form, a number of reasoning tasks including entailment, sat­ isfiability and forgetting can be accomplished in linear time. We have shown that every propositional theory can be compiled into DNNF and presented an algorithm to this effect. We then presented a key result according to which the time and space complexity of our compi­ lation technique is linear given that the propositional theory has a clausal form with bounded treewidth. Fi­ nally, we presented two techniques for approximating DNNF compilations. One of the techniques generates sound compilations, the other generates complete com­ pilations. Together, the two approximations bound the original theory from below and above in terms of their ability to answer queries. There are at least three key distinctions between our compilation approach and the one proposed in [7]. First, every theory has a DNNF representation, while not every theory has a Horn rep­ resentation. Second, there are theories with exponential Horn approximations, yet polynomial DNNF represen­ tations. Third, we have characterized a class of theories which is guaranteed to have linear DNNF compilations. We are not aware of a similar guarantee on the Horn approximations of this class of theories.

4 In (4], we compare DNNFs with Binary Decision Dia­ grams (BDDs) as a representation of Boolean functions.