An Analysis of Approximate Knowledge Compilation

1 Introduction

Knowledge compilation is the process by which an initial theory E with respect to which inference is intractable is transformed into one or more "approximate" or equiva­ lent theories with respect to which inference can be per­ formed efficiently. The notion of Horn approximations , more specifically of Horn lowest upper bound (L UB) and Horn greatest upper bound(s) (GLB), was introduced by Selman and Kautz in [SK91]. The idea is to map ("com­ pile" ) a clausal propositional theory E into two Horn theories E lb and E1ub such that Eglb is a weakest Horn theory thit entails E, and E1ub is the strongest Horn theory entailed by E. These "approximate theories" can be used to efficiently answer queries about the conse­ quences of E, as reviewed below. The key observation is that queries with respect to Eglb or E1ub can. be answered in polynomial time, since both theories are Horn, rather than using an exponential algorithm to decide whether E I= C. Though the cost of obtaining Elub and Eglb can and usually will be very high (which justifies thinking of it as a preprocessing or compilation step), this cost can be amortized over a sufficiently large set of queries about E, which can be answered more efficiently after compilation.

*Much of this work was performed while the author was a post-doc at Stanford University's Computer Science Depart­

ment. Alternative email address: delval@cs.stanford.edu.

This framework was generalized by Kautz and Sel­ man to approximations written in target languages other than Horn (see [KS91; SK95], and section 2 below). A key aspect of the framework is given by two procedures that generate the LUB and GLB in the given target lan­ guages, respectively the Generate-LUB an.d Generate­ GLB algorithms. Selman and Kautz provide no proof of correctness for Generate-LUB either in its more re­ stricted form (which generates Horn LUBs) or in the more general form in which it generates other kinds of L UBs. In this paper, we establish general conditions for Generate-LUB to be correct ; these conditions are strictly weaker than those cited by Kautz and Selman, as the target language needs to be closed under subsumption, but not under resolution. We thus improve and correct Selman and Kautz's analysis of their general framework for knowledge compilation, greatly expanding the set of target languages for which the generic Generate-LUB al­ gorithm yields correct results. This set now includes, in particular, any subset of k-CNF closed under subsu~p­ tion, for example the k-Horn language [DP92] ; an Im­ portant feature of such languages is that the LUB has guaranteed polynomial size. In addition, a simple mod­ ification of the algorithm allows us to prove it correct with respect to arbitrary propositional clausal target lan­ guages.

The structure of this paper is as follows. In the next section, we review the main concepts of LUB and GLB knowledge compilation. Section 3 offers two gen­ eral characterizations of the LUB for arbitrary target languages; in particular, completeness with respect to queries in the target language fully characterize~ the LUB. Section 4 analyses the Generate-LUB algonthm, establishing general conditions for its correctness, and generalizing it to deal with arbitrary clausal target lan­ guages. In section 5 we consider some complexity issues, followed by an analysis of the quality of Horn approximations in section 6. Related work, together with some implications of our results on the goals of compilation, is discussed in the final section.

2 L UB approximations: Review

In this section, we review the framework for knowledge compilation, as described in [SK91; KS91]. The basic idea is to approximate a theory in a given source lan­ guage by bounding from above and from below the set of models of the theory, where the bounds can be expressed in a computationally less difficult target language.

Kautz and Selman define a general framework for knowledge compilation in terms of arbitrary source and target languages and consequence relations. In this pa­ per, we will focus only on clausal propositional and first order languages, with the classical consequence relation.

Let C be a propositional or first order clausal language. For any given "target language" CT ~ C we can define CT-upper and lower bounds of any theory E expressed in C as follows.

Definition 1 For any E ~ C, the theories Ecb, Eub ~ CT are respectively an CT-lower bound and an CT-upper bound of E iff Ecb I= E I= Eub.

Letting M od(r) denote the set of models of r, we have:

Thus, Ecb approximates E "from below", whereas Eub approximates E "from above". The "best" approxima­ tions are defined as follows:

Definition 2 E91b ~ CT is an CT-greatest lower bound (GLB) of E ~ C iff Eglb I= E and for no E' ~ CT it is the case that Eglb I= E' I= E but E' ~ Eglb .

A GLB of E is thus a weakest theory of the target language CT that entails E. Similarly, a LUB of E is a strongest theory of CT that is entailed by E:

Definition 3 Ecub ~ CT is an CT-lowest upper bound (LUB) of E ~ C iff E I= Ecub and for no E' ~ CT it is the case that E I= E' I= Ecub but Ecub ~ E'.

We can use the CT-LUB Ecub and the CT-GLB Eglb of E for answering queries whether E I= C, for any clause C, as follows. If Ecub I= C then E I= C, and if Eglb ~ C then E ~ C (otherwise, answer "don't know", or use a complete theorem prover to answer). Furthermore, it is a consequence of theorem 1 below that for C E CT, if Ecub ~ C then E ~C. Thus, if the query language is a subset of CT then only the CT-LUB is needed to answer queries. Ofcourse, the use of the CT-LUB and CT-GLB instead of the original theory for answering queries only makes sense if one can reason more efficiently (either analytically or empirically) about th!'l former than about the latter.

We will only be concerned with LUBs in this pa­ per. Note that only the LUB can be used to derive logical consequences of E, as opposed to rejecting non­ consequences. We speak of the CT-LVB, since it always exists (the empty theory is an £T-upper bound of any theory), and it must be unique up to logical equivalence: the conjunction (union) of any two upper bounds E'

and E" is by definition also an upper bound, which is at least as strong as both E' and E". Hence the CT­ LUB is equivalent to the conjunction of all £T-upper bounds. Further general characterizations of the CT­ LUB are given below.

3 Characterizing the LUB

In this section we provide two alternative characteriza­ tions of the CT-LUB. We first prove a result that will be useful throughout the paper, namely: completeness for CT queries about E is both sufficient and necessary for a theory of CT to be the CT-LUB of E.

Theorem 1 Let Ecub ~ CT, E C C. The following statements are equivalent:

• Ecub is the CT-L UB of E.
• For every C E CT: E I= C iff Ecub I= C

Proof (=>)Suppose Ecub is the CT-LUB of E, and let C E CT. If Ecub I= C then E I= Ecub I= C. Suppose on the other hand that E I= C yet Ecub ~ C. Then E' = (Ecub U { C}) is such that E' ~ CT and E I= E' I= Ecub, yet Ecub ~ E'. This contradicts the fact that Ecub is the CT-LUB of E.

( ~) Suppose Ecub is not the CT-L UB of E. If E ~ Ecub then there exists C E Ecub ~ CT such that E ~ C, where trivially Ecub I= C. Suppose therefore that E I= Ecub· Then Ecub is an £T-upper bound of E. If it's not the CT­ L UB then there exists E' ~ CT such that E I= E' I= Ecub yet Ecub ~ E'. Hence there exists C E E' ~ CT such that Ecub ~ C and E I= E' I= C. 0

It is interesting to note that this characterization of the CT-LVB, which holds for arbitrary clausal target languages, opens up a somewhat different perspective on the goals of compilation. Namely, the choice of a tar­ get language can now be guided not (only) by efficiency in answering queries about the original theory, but by the desire to obtain completeness with respect to certain query languages, for some perhaps task specific purposes, while ignoring parts of the theory irrelevant to the task. We will briefly come back to this point at the end of the paper.

A second characterization of the CT-LUB can be given in terms of implicates of the source theory. For target languages closed under subsumption, the CT-LUB of E is logically equivalent to the set of prime implicates of E that are in CT .

Definition 4 A clausal language CT is closed under subsumption iff for every C E CT, if a clause C' sub­ sumes C then C' E CT .

Definition 5 A clausal language CT is closed under res­ olution iff for every B, C E CT , if A is a resolvent of B and C then A E CT.

Theorem 2 Let TI(E) be the set of prime implicates of E ~ C. If CT is closed under subsumption then the CT­ L UB of E is logically equivalent to TI(E) n CT .

Proof This is a corollary of theorem 3 below.

0

To see that theorem 2 does not hold in general for languages not closed under subsumption, let CT be the language of definite clauses (clauses with exactly one positive literal). The .CT-LUB of :E = { --.p, --.q V r} is equivalent to { --.p V q, ·q V r}, which is clearly not equiv­ alent to II(:E) n .CT . 1

It is easy however to generalize theorem 2 to target languages not closed under subsumption. For this, we need the notion of prime .CT-implicates.

Definition 6 A clause C is an .CT-implicate of :E iff C E .CT and :E F= C. C is a prime .CT-implicate of :E iff C is an .CT-implicate of :E not strictly subsumed by any other .CT-implicate of L The set of prime .CT-implicates of :E is denoted II.cT (:E).

Theorem 3 The .CT-LUB of:E is equivalent to II.cT(E).

Proof By theorem 1, it suffices to show that for any C E .CT, :E F C iff II.cT(:E) F C. Let C E .CT. If II.cT (:E) F C then :E F= II.cT (:E) F C. For the other direction, if :E F= C then C is an .CT-implicate of :E, hence there exists C' E II.cT (:E) such that C' subsumes C. Thus II.cT(:E) F= C' F= C. D

Note that if .CT is closed under subsumption then II.cT (:E) = (II(:E) n .CT ), from which theorem 2 follows as a corollary. More generally, II.cT (:E) and therefore the .CT-LUB of :E can be characterized in terms of II(:E) through a certain form of weakening of the prime impli­ cates, a notion which can be seen as a dual of Selman and Kautz's notion of strengthenings.

Definition 7 A non-tautologous clause C is an .CT­ weakening of a clause C' iff C E .CT, C' subsumes C, and no C" E .CT subsumed by C' strictly subsumes C. The set of .CT-weakenings of a clause C is denoted W.cT(C).

For example, if .CT is the language of definite clauses over a vocabulary {Pl, ... , Pn} then the set of .CT­ weakenings of 'Pl is W.cT ( ·pi) = { --.pl V Pi I 1 < i ~ n}. On the other hand, if C E .CT then W.cT (C) = { C}. Finally, .CT-weakenings may not always exist. If .CT is closed under subsumption then there are no .CT­ weakenings of any clause C fl. .CT. There is for example no Horn-weakening of a non-Horn clause in the proposi­ tional case; and while Horn clauses have definite clause weakenings, non Horn clauses do not.

Despite these complexities, the next theorem shows that the .CT-LUB can be obtained by collecting the .CT­ weakenings of the prime implicates of :E (p(f) denotes the result of removing subsumed clauses from r.)

Theorem 4 II.cT(:E) = J.t(UcEII(~) WcT(C)).

Proof (~)Suppose C E II.cT(:E). Then :E F= C, hence there exists C" E II(:E) that subsumes C. If C" E .CT then C subsumes C" as well (otherwise C fl. II.cT(:E), which would be a contradiction); hence C E II(:E), and since C E .CT, Cis an .CT-weakening of itself. Suppose on the other hand that C" fl. .CT. Because C E II.cT (:E) ~ .CT, if Cis not an .CT-weakening of C" then there exists C' E .CT subsumed by C" which strictly subsumes C. Since :E F= C" F= C', this contradicts C E II.cT (:E).

1 [SK91] prove theorems 1 and 2 for the Horn case. After writing this paper, we found a much more indirect proof of theorem 1 in [KR94].

(2) Suppose Cis an .CT-weakening of C' E II(:E), and C is not subsumed by any clause in the right hand side. Then :E F C' F C and C E .CT. Hence C is an .CT­ implicate of :E, and clearly no other .CT-implicate of E can strictly subsume C. 0

We remark that all the results of this section hold for both propositional and first order clausal languages. In the rest of the paper we restrict our attention to propo­ sitional languages.

4 Computing the L UB

In this section, we provide procedures to compute the .CT-LUB for arbitrary propositional clausal target lan­ guages. We begin by considering the case in which .CT is closed under subsumption, and later extend the results to the general case.

The following procedure computes an .CT-L UB for any target language .CT that is closed under subsumption, as we will show; the procedure differs from the one given in [SK91] only in the incorporation of a tautology dele­ tion strategy. The algorithm is a brute force resolution algorithm modified to avoid resolving together pairs of clauses both of which belong to the target language .CT, in the expectation that this will lead to smaller compiled theories (smaller, that is, than what theorems2-4 would give us).

Procedure Generate-.CT-LUB(:E) begin :ET := { C E :E I C E .CT and C is not tautologous} EN := { C E :E I C fl. .CT and C is not tautologous} loop choose clauses cl E :ET u :EN' c2 E :EN with a non-tautologous resolvent C which is not subsumed by any clause in :ET U :EN if no such choice is possible then exit loop endif ~CE~ . then delete from :ET and :EN any clause subsumed by C :ET := :ET U {C} else delete from EN any clause subsumed by C EN:= EN u {C} endif endloop return :ET end

In order to establish the correctness of the algorithm for target languages closed under subsumption we need two lemmas, whose proofs are omitted for lack of space. 2 In what follows, we write r 1- C, for a clause C and a set of clauses r' iff there exists a resolution deduction from r of a clause C' that subsumes C; also, :ET and :EN refer to the final values of these variables in the Generate-.CT­ LUB algorithm .

Lemma 5 If ET 1- B, C E :EN, and A is a non­ tautologous resolvent of B and C, then either ET 1- A or there exists A' E :EN s. t. A' subsumes A.

· 2 They are available from the author in a longer version of this paper.

This lemma in effect tells us that it is possible to trans­ form certain resolution trees, so that all resolutions be­ tween two clauses of the target language occur in the bottom part of the transformed tree. Using these trans­ formations, the next lemma in turn establishes that ET and EN completely characterize the set of clausal conse­ quences of the source theory E.

Lemma 6 If E r A then either ET r A or there exists A' E EN s.t. A' subsumes A.

Suppose now that CT is closed under subsumption. Then no A' E EN can subsume A when A E CT, so lemma 6 has the following immediate corollary:

Lemma 7 Suppose CT is closed under subsumption. If E r A and A E CT then ET r A .

Theorem 8 Generate-CT-L UB{E) computes the CT­ L UB of E for any clausal language CT closed under sub­ sumption.

Proof By theorem 1, it suffices to show that for any C E CT, E ~ C iff ET ~C. The right to left direction follows from the fact that E ~ ET. The other direction follows directly from lemma 7 and the completeness of resolution as an inference procedure. 0

It was previously thought [SK95] that closure under resolution was also required for Generate-CT-LUB to be correct. That this is not the case is fortunate, since im­ portant languages such as k-Horn (Horn clauses with at most k literals) and k-quasi-Horn (clauses with at most k positive literals) are closed under subsumption but not under resolution. Important uses of k-Horn approxima­ tions are discussed in [DP92; KS92b] . More generally, any subset of k-CNF closed under subsumption (which includes k-Horn) can now be the target language for Generate-CT-LUB. Note that the use of any such subset as target language guarantees that the compiled approxi­ mate theory has polynomial size.

Let us now turn our attention to target languages which are not closed under subsumption. One could use theorem 3 to compute the c ·T-LUB for any such CT: compute all prime implicates, and then collect those in CT plus the CT weakenings of those not in CT. For­ tunately, the space optimization used in the Generate­ CT-LUB algorithm can still be used. The next theorem implies that, for any target language CT, we can com­ pute the CT-LUB of an arbitrary clausal theory E by computing ET and EN using the original Generate-CT­ LUB algorithm, returning the union of ET with the set of CT-weakenings of clauses in EN; 3 resolutions within CT can still be avoided for such languages.

Theorem 9 For any E ~ C, the theory Elub = (ET U UceEN W.cT(C)) is the CT-LUB of E.

Proof By theorem 1, it suffices to show that for any C E CT, E ~ C iff E1ub ~ C. The right to left direc­ tion follows from the fact that E ~ Elub . For the other direction, let C E CT and suppose E ~C. By lemma 6, either ET ~ C (in which case trivially Elub ~ C) , or there exists C' E EN such that C' subsumes C. In the latter case, since C E CT, there exists an CT-weakening C" of C' such that C" subsumes C (possibly C" = C) . Since C" E W.cT(C') and C' E EN, Elub ~ C" ~C. 0

3 Except that .in the "else" clause we should also delete from L;T any clause subsumed by C if we do not want to end up with some subsumed clauses.

Note that theorem 8 is a special case of theo­ rem 9, since if CT is closed under subsumption then UceEN W.cT(C) = 0 (see observations after definition 7) . We thus conclude that there exists a procedure that computes the CT-LUB for arbitrary clausal target lan­ guages.

5 Computational complexity

The perhaps surprising power of the Generate-CT-LUB algorithm is not without serious costs, however. As shown in this section, the space requirements of the pro­ cedure are exponential in the combined size of input and output.

Before proving this result, it is worth mentioning first the following simple generalization of theorem 1 from [SK91], which has an essentially identical proof.

Theorem 10 If CT can express unsatisfiable theories 4 then the CT-L UB of E is satisfiable iff E is satisfiable.

It does not follow from this, in general, that computing the CT-L UB is intractable (consider the degenerate case in which CT = C). It does follow however that for any such CT either there is no polynomial time algorithm for computing the CT-LUB, or inference in CT cannot be performed in polynomial time (provided P f. N P). For if both tasks could be performed in polynomial time we could decide satisfiability in polynomial time.

Let us now turn to the space requirements of Generate­ CT-LUB, the main goal of this section. An unfortunate consequence of lemma 6 is that if CT is closed under resolution then EN contains all prime implicates of E not in CT.

Theorem 11 If CT is closed under resolution then (IT(E) \ CT) ~ EN.

Proof Suppose C E (IT(E) \ CT)· Then E r C, hence by lemma 6 either ET r cor there exists C' E EN such that C' subsumes C.

Case 1: ET r c. Since CT is closed under resolution and ET ~ CT ' ET r C' for some C' E CT that subsumes C. But since C ¢ CT by hypothesis, C' must strictly subsume C. Since E ~ ET ~ C', this contradicts C E IT(E). Hence this case is impossible.

Case 2: there exists C' E EN that subsumes C. Since E ~EN ~ C', and C E IT(E), C must subsume C' as well, hence C E EN. 0

The converse inclusion does not hold. For a counterex­ ample, let CT be the language of Horn clauses, and let E = {pV--,q , qV--,r,pV.....,rVs}. Then EN= {pV.....,rVs} C£

4 The language of definite clauses, for example, cannot ex­ press unsatisfiable theories: the valuation which assigns true to every symbol satisfies any set of definite clauses. On the other hand, any language closed under subsumption includes the empty clause.

II(:E). Nor does the theorem hold in general for lan­ guages which are not closed under resolution: let CT be the language 3-Horn, withE= { ..,pV..,qV..,r, rv-,sv-,t}. Then EN = 0, yet II(E) \ CT = { -,p V -,q V -,s V -,t}.

Consider now any theory with an exponential number of prime implicates (examples can be found in [KT90; CM78]). By adding two new positive literals to every clause, any such theory will have an exponential number of non-Horn prime implicates, since those two literals will occur in any clause entailed by the theory; in fact, all prime implicates will be non-Horn. And since the language of Horn clauses is closed under resolution, all these prime implicates will be computed and stored by Generate-CT-LUB, for CT =Horn, despite the fact that the Horn-LUB of any such theory will be empty. Similar or identical examples can be used to show that the same holds for many other target languages. These include, to begin with, subsets of the Horn language, such as definite clauses, k-Horn clauses (Horn with at most k literals, for any fixed k), and unit clauses (at most one literal per­ clause); but also languages such as reverse Horn (clauses with at most one negative literal) and its subsets, binary clauses (clauses with at most two literals), or a language that allows only a subset of the symbols of the language. The following corollary summarizes this discussion.

Corollary 12 The Generate-CT-L UB algorithm re­ quires exponential space (hence time}, even in cases in which it outputs the empty theory as the CT-L UB.

Cases in which Generate-£T-LUB has exponential size output have already been described in [KS92a]. Corol­ lary 12 is stronger in that the exponential space require­ ments are not justified by the size of the output, in other words, time and space are exponential in the com­ bined size of input and output. Notice furthermore that for all the above mentioned theories with empty LUB, Generate-CT-LUB reduces to a brute force prime impli­ cate algorithm, which is likely to be extremely inefficient.

There are other complexity results from the litera­ ture on Horn approximations that readily generalize to a wide variety of target languages. In particular, the proof [KS92a] that Horn approximations most likely re­ quire worst case exponential space (unless non-uniform P ~ N P) applies with little or no modification to many other target languages, as was already noted in [KR94]. Another result that can be generalized deals with the complexity of inference with respect to the £T-LUB, that is of deciding whether E1ub f= C, given as input E and C. The reason behind this question is that we may want to consider this inference problem without ex­ plicitly computing the CT-LVB. Cadoli [Cad93] shows that this problem has exactly the same complexity as that of deciding whether E f= C, for Horn C. Using the notion of CT-strengthening introduced in [KS91] as a generalization of Horn strengthenings [SK91], one can easily generalize this result to arbitrary target languages closed under resolution.

6 The quality of approximations

There are at least two important aspects in assessing the quality of an approximate theory: its size, and its "closeness" to the original theory. In this section, we discuss the latter from a worst case perspective. For concrete­ ness, we will focus on Horn approximations. We show that the weakening of the original theory represented by the L UB can result in failing to answer an exponential number of queries, and in adding an exponential number of models to those of the original theory. We leave the reader the task of identifying further target languages for which the conclusions of this section apply.

Example 1 The examples used to establish corol­ lary 12 have an exponential number of prime implicates which do not follow from the Horn LUB. There is there­ fore an exponential number of queries entailed by the original theory that the L UB will fail to answer.

Example 2 Given a set of variables x1 , ... , Xn, let E = { x; V xi 11 ::; i < j ::; n} be the set of all binary positive clauses on this vocabulary. This theory is satisfied by exactly the set of interpretations that satisfies at most one negative literal, hence it has n + 1 models. The Horn LUB is empty, however, so it has 2n models. The ratio between the number of models of the L UB and the number of models of E is therefore exponential. A similar asymptotic ratio holds for any fixed k, with E = {k-ary positive clauses}.

In the last example, it is possible to work around the problem by observing that E can be brought to Horn form by an uniform renaming of all symbols, i.e. E is in the class "renamable Horn" and is therefore tractable. The next example does not have this property.

Example 3 Given variables x1 , ... , Xn, the non-parity theory is given by the sentence ..,(x1 EB ... EB xn), where EB denotes the exclusive-or connective. The models of this theory are all interpretations that satisfy an even number of positive literals, for a total of 2n-l models. In prime implicate form, it can be written as

where o- is the set whose elements are those sets con­ sisting of exactly one literal for each variable in the lan­ guage, such that the total number of negative literals is odd. (See the discussion of the parity function in [Weg87].) If n is odd (the case with n even is left to the reader), then the Horn L UB approximation of non­ parity, equivalently the set of Horn prime implicates of non-parity, contains the single clause -,x1 V .. . V-,xn (any other implicate contains at least two more positive liter­ als). This clause rules out exactly one model, hence the LUB has 2n- 1 models, or 2n-l - 1 more models than the original theory. Any model containing at least one negative literal will satisfy the LUB, rather than only those models with an even number of positive literals.

Example 4 There is also at least one fairly natural class of theories that yield inadequate approximations.

Consider the propositional encoding of constraint sat­ isfaction problems (CSP). For each variable Xi of a given CSP, its propositional encoding E contains a clause Ci = (Xi = x{ V ... V Xj = x~;) specifying its initial domain, clauses specifying that distinct values of a vari­ able are incompatible, and where n-ary constraints for n ~ 2 are encoded by negative clauses ("no goods") stat­ ing which combinations of values are incompatible.

For each clause Ci , there must exist a unique clause Cj E ll(E) which subsumes Ci. Now, it is easy to see that Elub, being Horn, can only entail Cj iff Cj is a unit clause, i.e. if the CSP uniquely determines a single pos­ sible value for the given variable. For any variable for which this is not the case, the information that the vari­ able must have at least one value will be lost by the Horn ' LUB, and the LUB will be consistent with a number of variables having no value. If k is the number of variables for which the CSP does not uniquely determine a value,

this gives at least Ej=1 ( ~ ) additional models. Inde­

pendently of quantitative measures, moreover, we would argue that there is a qualitative sense in which these approximations are inadequate - for example, if Xj de­ notes the position of an object, the compiled theory may be consistent with the object mysteriously vanishing (i.e. with Xi having no value), so a robot may have no reason to loqk for it. Note incidentally that combining the LUB with a GLB would be of little help for such problems, as any GLB of E must entail a complete assignment of val­ ues to every variable (because all Horn strengthenings of the various clauses Xi are positive unit clauses.)

In conclusion, it is easy to find examples which defeat Horn approximations, even in theories (such as CSPs) with a very small proportion of non-Horn clauses. While this is an important fact, we emphasize that it in no way precludes a profitable use of Horn approximations for large classes of theories which do not include the ones discussed here.

7 Discussion

In this paper, we have provided an analysis of approx­ imate knowledge compilation on the basis of the ap­ proach introduced by Selman and Kautz in [SK91; KS91; SK95]. Highlights of the analysis, which generalize the results of Selman and Kautz in a number of ways, are:

• the characterization of the .Cr-LUB for arbitrary clausal languages used as target of the compilation, both in terms of completeness with respect to .Cr­ queries and of prime .Cr-implicates;
• an analysis and proof of correctness of the generic procedure Generate-.Cr-LUB, as introduced in [KS91], showing that it can be used without mod­ ification for any target language closed under sub­ sumption;
• for languages not closed under subsumption, we have shown that the main computational attractive of the procedure, namely the avoidance of resolu­ tions among clauses of the target language, can be preserved, providing a new generic algorithm that

computes the .Cr-LUB for arbitrary propositional clausal languages.

As already mentioned, there is an important class of languages, closed under subsumption but not under resolution, for which, contrary to what was previously thought, Generate.Cr-LUB gives correct results. This class of languages includes any subset of k-CNF closed under subsumption; the LUB with any such subset as target language has polynomial size. Of special interest among them is the language k-Horn, which is tractable, and which has been explored in detail as an approxima­ tion tool in [DP92; KS92b].

We have also analyzed some points which are crucial to the evaluation of the concepts and procedures discussed. First, either computation of the .Cr-LUB, or inference in .Cr is likely to be intractable. Second, for many target languages Generate-.Cr-LUB has exponential space and time requirements even in cases where the .Cr-L UB is the empty theory. Finally, we have analyzed the quality of Horn approximations in terms of closeness to the initial theory.

In the category of related work, the great debt of this paper to the work of Selman and Kautz should be ob­ vious to any reader; credit for specific results or proofs due to them has been explicitly indicated where appro­ priate. We should also mention that our results may have consequences for other approaches to knowledge compi­ lation, specifically for the work of del Val in [dV94] . del Val presents procedures to compile propositional theo­ ries into equivalent, not just approximate, theories for which unit resolution is complete. One of these proce­ dures uses the skeleton of the Generate-.Cr-LUB algo­ rithm as instantiated for the Horn target language, and the question arises whether the cited procedure can be generalized to take advantage of the results of this paper.

Finally, let us mention the work oflnoue [Ino92] on lin­ ear resolution procedures for finding the "characteristic clauses" (prime .Cr-implicates) of a "production field" (target language .Cr). Just like us, Inoue considers the problem for arbitrary target languages, providing proce­ dures that compute the characteristic clauses of a theory for any target language closed under subsumption (what he calls an "stable" production field) . Interestingly, he discusses multiple applications of the notion of charac­ teristic clauses, which suggest a somewhat different per­ spective on the goals of compilation. For example, in ab­ duction we are interested in certain kinds of entailments of the database, namely the implicates that involve only literals describing allowable hypothesis ( abducibles) and some literal to be explained in terms of those hypoth­ esis. Similarly, in determining the circumscriptive con­ sequences of a propositional theory we are interested in particular in clauses that involve only positive literals whose symbol is being "minimized" or literals made from the set of "fixed", non-variable symbols. In diagnosis, we are interested in the "minimal conflicts", that is, the prime implicates that contain only AB-literals. In either case, the desired class of implicates can be designated as target language .Cr; the Generate-.Cr-LUB procedure can then be used to ensure completeness for queries ex­ pressed in .Cr . One can also think of less sophisticated but equally useful task specific reasons for choosing the target language. For example, we may want to com­ pile the input-output behavior of a device assembled by means of some other more elementary components de­ scribed prepositionally. One possibility is to compute the prime implicates of the theory resulting from com­ bining the theories corresponding to the device's com­ ponents, throwing out all those which involve "internal" variables which do not refer to the initial input or final output of the assembled device. The other possibility, which may require much less space, is to designate the clauses involving only input and output variables as tar­ get language, and compile using the standard Generate­ .Cr-LUB.

In summary, achieving completeness with respect to a given target or query language is a worthwhile goal for L UB compilation. Even if the query language is not tractable, one can benefit from ignoring irrelevant parts of the initial theory, and there is always the possibility of further compiling the LUB into a tractable form in a second pass, possibly using some other method. There is in fact an interesting alternative when the query lan­ guage .CQ is not tractable but its complement is closed under resolution. In this case, we can choose the comple­ ment as target language .Cr for Generate-.Cr-LUB, and obtain in '£N the prime implicates of '£ which belong to .CQ (as implied by theorem 11), hence the .CQ-LUB. This guarantees completeness and tractability (relative to the size of EN) with respect to .CQ, while avoiding all resolutions among clauses which do not belong to the query language. As an example, one can obtain the k-quasi-Horn LUB, in prime implicate form, by desig­ nating its complement as target language; no pairs of non k-quasi-Horn clauses will ever be resolved together by Generate-.Cr-LUB in this case.

Both Inoue's linear resolution procedure and the pro­ cedures of this paper can be used to obtain completeness with respect to the selected query language (Inoue's re­ sults are limited in this regard to languages closed under subsumption, though the results of the present paper can be easily used to lift this restriction). There are two main differences. First, the restrictions imposed by his version of linear resolution have no analogous in Generate-.Cr­ LUB; the latter is therefore much more likely to gen­ erate redundant resolution derivations. However, and this is the second crucial difference, his procedure does compute all prime .Cr-implicates, producing "compiled" theories which in general will require much more space than those generated by the LUB algorithm; this fact limits the usefulness of the linear resolution procedures for compilation purposes.