Knowledge Compilation Using Theory Prime Implicates

1 Introduction

Query answering from a propositional knowledge base is a central concern in artificial intelligence. Unfortunately, its computational complexity is high, both theoretically (co­ NP-complete), and practically since every existing algorithm runs in time exponential in the size of the knowledge base in the worst case.

To improve query answering and deal with its intractability, several approaches have been proposed so far. A first approach consists in restricting the representation language (e.g. considering only Horn formulas) or the inference mechanisms (e.g. involving resource-bounded reasoning). Another approach consists in approximating the knowledge base [Selman and Kautz, 1991; Kautz and Selman, 1994] or the logical entailment relation [Cadoli and Schaerf, 1991].

A third family gathers equivalence-preserving compilation techniques. Compiling a knowledge base consists in translating (compiling) the base during a preprocessing phase into an equivalent compiled form (a compilation) from which query answering is tractable. In contrast to the two other approaches, equivalence-preserving compilation does not give up expressiveness or equivalence but simply speeds inference by shifting computational costs Relevant to this last approach is, among others (e.g. [del Val, 1994; Mathieu and Delahaye, 1994; Dechter and Rish, 1994]), Reiter and de Kleer's technique which consists in turning the knowledge base 1: into the prime implicates normal form [Reiter and de Kleer, 1987].

Interestingly, this last technique relies on a more general and computationally valuable principle of locality. Let us say that a knowledge base 1: is local for query answering when, for every formula 1t, 1t is a logical consequence of 1: iff there exists a formula 1t' in 1: s.t. 1t is a logical consequence of 1t'. Now, let us assume that 1: contains n formulas 1t' of size m and that 1t is of size p. The time cost c(1:, 1t) for answering query 1t from 1: is (in practice) exponential in n*m +pin the worst case. When 1: is local, the cost comes down to n*c(1t', 7t), which can easily be exponentially smaller than c(1:, 1t). Additionally, query answering from formulas 1t' can be computationally easier than query answering from the whole knowledge base. This is exactly what happens with prime implicates knowledge bases: they are local for clausal query answering (i.e. considering queries limited to clauses) and, while c(1: , 7t) is exponential in the size of 1: u {7t} , c(1t', 1t) is polynomial in the size of {7t', 1t} (checking whether a clause 1t' entails a clause 1t can be done in time O(sup(l7t'l, l1tl)2)).

In this paper, we propose a new approach to equivalence­ preserving knowledge compilation which extends Reiter and de Kleer's technique. Our approach is based on both:

(1) the idea of expressiveness restrictions and/or compilations that make inferences tractable. Thus, we propose a compilation function which takes advantage of tractable theories <I> among those implied by 1:. This leads us to generalize the standard logical entailment relation 1= to the relation I=<I> where <I> is built-in.

(2) the idea of locality for clausal query answering. To be more precise, our compilation function aims at making 1: local for clausal query answering by computing the theory prime implicates of 1: w.r.t. <I>; theory prime implicates are to I= <I> as prime implicates are to 1= .

The rest of this paper is organized as follows . Some formal preliminaries are given in section 2. In section 3, the concept of theory prime implicate is introduced. Some metatheoretic properties and a procedure for generating theory prime implicates are successively pointed out. In section 4, we present our compilation function which basically consists in computing the theory prime implicates of 1: w.r.t. a tractable theory <I> implied by 1:. As a central result, we prove that query answering from a compilation can be done in time polynomial in the size of the compilation. In addition, we point out several potential candidates for the notion of "good" tractable theories, i.e. those leading to a reasonable growth of the corresponding compilation. While a compilation which is exponentially larger in size than the original base may easily be produced, the size of the theory prime implicates compilation of a knowledge base is smaller than the size of its prime implicates compilation in the general case and it can even be exponentially smaller. In section 5, we show that our compilation technique can be advantageously compared with other approaches to knowledge compilation in some situations; we present some preliminary experimental results providing evidence for the substantial space savings achievable with this approach. Section 6 concludes the paper with some perspectives. More details about this work can be found in [Marquis, 1995].

2 Formal preliminaries

Let PS be a finite set of propositional symbols (atoms). Let PROPps denote the propositional language built in the usual way upon PS and the connectives. The elements 'If of PROPps are called formulas. Any finite set of formulas will be identified with the conjunctive formula whose conjuncts are the elements of the set.

An interpretation I (on PROPps) is a mapping from PS to {T, F} . The semantics of a formula 'If in an interpretation I, noted ['If] (I), is an element of {T, F} defined in the usual way. We say that an interpretation I is a model of a formula 'If iff [ 'If] (I) = T. We will note 'If I= q, when [ q,] (I) = T for every model I of 'If, and say that q, is a logical consequence of 'If. When 'If I= q, and q, I= 'If, 'If and q, are said equivalent; this is noted 'If = q,. PROPps I= denotes the quotient set of PROPps induced by the equivalence relation=.

The size l'lf I of a formula 'If is the number of propositional symbols occurring in it. nb_cl{'l') will denote the number of clauses occurring in the set of formulas 'I'. We say that a formula 'If is in k-CNF if it is in clausal normal form (CNF), and the size of every clause in 'If is bounded by the constant k. When 'If is in k-CNF, then l'lfl =t9(nb_cl{'lf)).

A prime implicate of a finite set 'I' of formulas is a clause 1t such that:

• 'I' I= 1t holds, and
• for every clause 1t', if 'I' I= 1t' and 1t' I= 1t hold, then 1t' = 1t holds.

Pl('l') will denote the set of prime implicates of 'I'. Clearly enough, the:; prime implicates of 'I' are the minimal elements w.r.t. I= in the set of all the clauses implied by 'I' (the so-called implicates 1('1') of '1'). Formally, we will note it Pl('l') = min(l('l'), I=). ·

Let <I> be a finite set of formulas. Let I= <1> denote the relation over PROPps X PROPps defined by cr I=<I> 'tiff <I> u {cr} 1= 't. Clearly enough, I=<I> is a partial pre-ordering over PROPps and I=<I> extends 1=. When cr I= <1> 't holds, we say that 't is a ci>-logical consequence of cr. Let =<1> denote the equivalence relation over PROPps induced by I=<I> and defined by cr =<1> 't iff cr 1= <1> 't and 't 1= <1> cr. When cr =<1> 't holds, cr and 't are said ci>-equivalent. Let PROPps I =<1> denote the quotient set of PROPps induced by the equivalence relation =<I>· By construction, I=<I> is a partial ordering over PROPps I =<~>·

3 Theory prime implicates

3.1 Generalizing prime implicates

Turning the concept of prime implicate into the notion of theory prime implicate consists in extending logical entailment by considering some piece of knowledge as built-in.

Definition 1 Let 'I' and <I> be finite sets of formulas. A clause 1t is a theory prime implicate of 'I' w.r.t. <I> iff:

• 'I' I=<I> 1t holds, and

· for every clause 1t', if 'I' I= <1> 1t' and 1t' I= <I> 1t hold, then 1t' =<1> 1t holds.

We note TPI('I', <I>) the set of theory prime implicates of 'I' w.r.t. <I>. TPI('I', <I>) is composed of the minimal elements w.r.t. I= <1> in the set of all the clauses that are <I>-logical consequences of 'I' (the theory implicates of'¥ w.r.t. <1>). Such clauses are considered up to <!>-logical equivalence: only one representative per equivalence class is kept in TPI('I', <1>).

Example 1 Let 'I' =def {p v q v s, p v t , q v t, q v s v u} and <I> =def { --,p v q, --,q v r, --,t v u} . Clauses p v t and q v s are the theory prime implicates of 'I' w.r.t. <I> (up to <!>-equivalence).

Clearly enough, the concept of theory prime implicate extends the standard notion of prime implicate. Formally, Pl('l') = TPI('I', { } ).

3.2 Some metatheoretic properties of theory prime implicates

In the following, we point out some metatheoretic properties of theory prime implicates. Thus, we show that TPI('I', ci>) is finite and independent of the syntactic nature of formulas occurring in 'I' or <1>. We also stress the central role taken by . theory prime implicates among theory implicates. On this ground, we make the interplay between prime implicates and theory prime implicates precise.

Proposition 1 Let 'I', 'I'', <I>, <I>' be finite sets of formulas. TPI('I', <I>) is a finite set (up to <!>-equivalence). Moreover, if <I> = <I>' and 'I' =<1> 'I'' hold, then TPI('I'', <I>')= TPI('I'', <I>') (up to <!>-equivalence).

The next proposition is central for our purpose since it shows that TPI('I', <I>) captures in some sense all the clauses that are <I>-logical consequences of 'I'.

Proposition 2 Let 'I' and <I> be finite sets of formulas and 1t be a clause. 'I' I= <1> 1t holds iff there exists a theory prime implicate 1t' of 'I' w.r.t. <I> s.t. 1t' I= <I> 1t holds.

Example 1 (continued) r v t v u is a <!>-logical consequence of 'I' since there exists p v t in TPI('I', ci>) s.t. p v t I= <I> r v t v u holds.

As a consequence, turning a set \f of formulas into the set of its theory prime implicates w.r.t. <I> is an information­ preserving operation given <1>.

Corollary 1 Let \f and <I> be finite sets of formulas. \f =<t> TPI(\f, <I>) holds.

An additional consequence of Proposition 2 is that strengthening <I> can never increase the number of clauses of TPI(\f, <I>), as long as <I> is a logical consequence of \f.

Corollary 2 Let \f, <I> and <I>' be finite sets of formulas s.t. \f I= <I>' and <I>' I= <I> hold. For every n' e TPI(\f, <1>'), there exists 1t e TPI(\f , <I>) s.t. 1t' = <1>' 1t holds. Consequently, nb_cl(TPI(\f, <I>'))~ nb_cl(TPI(\f, <1>)).

Finally, we have shown before that prime implicates can be defined from theory prime implicates. The next proposition shows that the converse holds as well.

Proposition 3 Let \f and <I> be finite sets of formulas. TPI(\f, <I>) = min(PI(\f u <1>), l=<t>).

3.3 Computing theory prime implicates

Let us now address the problem of computing theory prime implicates. The algorithm TPI below is adaptated from Quine's iterated consensus technique [Quine, 1952; Quine, 1955]; it basically consists in computing the implicates of \f u <I> using any resolution-based prime implicates algorithm (e.g. [Kean and Tsiknis, 1990; de Kleer, 1992]), while keeping clauses minimal w.r.t. <I> only (using any procedure for deciding <I>-logical entailment).

Function TPI ('P, <I>)

% Input : two sets of formulas 'P and <I> in CNF. % Output : the theory prime implicates of 'P w.r.t. <1>. ~

1. Set TPI to 'P U <I>.

2. a/ Compute a new implicate C of 'P U <I> using any resolution-based prime implicates algorithm.

b/ If no new implicate is generated then return(TPI).

c/ If C is a <!>-logical consequence of some clause in TPI then repeat this step ignoring C.

1. a/ Delete from TPI any clause which is a <!>-logical consequence of C.

b/ Add C to TPI.

1. Go back to step 2.

Clearly enough, the correctness of TPI w.r.t. theory prime implicates computation is a direct consequence of Propositions 1 and 3. Interestingly, TPI is independent of the resolution-based prime implicates procedure used in it; indeed, whatever the resolution-based prime implicates procedure under consideration is, the set of clauses computed by TPI will be the same (up to <!>-equivalence). This allows us to use refinements of Quine's iterated consensus technique (in particular, this prevents one from generating redundant implicates thanks to Tison's technique [Tison, 1967] without sacrifying correctness). We can also improve TPI by preventing the implicates of <I> from being generated (step 2a/).

We developed two additional algorithms for computing theory prime implicates. The first one relies on a property relating the theory prime implicates of a disjunction of formulas to the theory prime implicates of its disjuncts (several prime implicates algorithms, including [Slagle et al., 1970; Jackson and Pais, 1990], rely on this property restricted to the prime implicates situation). The second one is based on theory resolution [Stickel, 1985]. Due to space limitations, we do not present these algorithms hereafter.

4 Knowledge compilation using theory prime implicates

4.1 Theory prime implicates compilations

Our approach to knowledge compilation basically consists (1) in pointing out tractable theories <I> that are implied by r. and (2) in making r. local using <I> while preserving logical equivalence. Formally, (2) is achieved thanks to the computation of the theory prime implicates of r. w.r.t. <1>.

Definition 2 Let r., <I> be finite sets of formulas such that r. I= <I> holds and <I> is tractable (i.e. clausal queries 1t can be answered in time polynomial in the size of <I> u { 1t }). The theory prime implicates compilation of r. w.r.t. <I> is defined by COMP<t>(L) =der <TPI(L, <1>), <1>>.

From a logical point of view, COMP<t>(L) is equivalent to TPI(L, <I>) u <I>; however, we do not keep together TPI(L, <I>) and <I> since they do not play the same role w.r.t. query answering.

Our objective is to prove that COMP<t> is actually an equivalence-preserving compilation function. On the one hand, showing that COMP<t> is equivalence-preserving is easy (the next corollary results directly from Propositions 1 and 2).

Corollary 3 COMP<t>(L) = r. holds.

On the other hand, we have to prove that query answering from COMP<t>(L) can be done in time polynomial in the size of COMP<t>(L). For this purpose, let us consider the function query-answering below:

Function query-answering (COMPq,(I:), 1t)

% Input: the theory prime implicates compilation COMPq,(I:) of I: w. r. t. <I> and a clause 1t.

• % Output: true iff I: I= 1t holds.
• For every 1t' in TPI(I:, <I>)

If 1t' I= <1> 1t holds then return (true)

1. Return(false).

The correctness of query-answering w.r.t. query answering is a straightforward consequence of Propositions 1 and 2. Now, a way to check whether n' I= <1> 1t holds consists in determining whether <I> I= (-,li v n) holds for every literal li of n'. When <I> is tractable, this test can be done in time O(ln'l * 1<1> u { 1t} I <X), where a is a constant. Subsequently, query answering from a compilation can be performed in time polynomial in its size. More precisely:

Proposition 4 Let I: be a finite set of formulas. Let <I> be a finite set of formulas s.t. I: I= <I>. If, for every clause 1t, checking whether <I> I= 1t holds can be done in time O(I<I> u {n}I<X) (where <X is a constant), then query-answering runs in time O(ITPI(I:, <I>)I*I<I> u {1t}I<X) in the worst case.

Thus, the crucial complexity factor of query answering from our comg,ilations is the size of TPI(I:, <I>) (provided that I<I>I = O(II:IP) where ~ is a constant).

4.2 Main characteristics of theory prime implicates compilations

Our approach to knowledge compilation possesses several interesting features. A strong point is that it is model­ theoretic. In particular, the number of clauses of COMP<J>(L) does not depend on any particular ordering of symbols but on the models of <I> only. This is not true for many approaches to knowledge compilation, particularly FPio [del Val, 1994] and Ed [Dechter and Rish, 1994]. We can also prove that FPio and FPI2 compilations depend as well on a particular ordering of symbols; particularly, the way in which implicates are generated in FPio and FPI2 may dramatically bear on the size of the resulting compilation (i .e. by an exponential factor).

Another strong point of our approach is that it is generic in essence. It may give rise to many compilations, taking advantage of many tractable classes of theories in propositional logic. For instance, the class of theories which are unit-refutation complete (including the Horn and the reverse Horn theories) and the class of theories consisting of binary clauses (Krom formulas) are polynomial for SAT (see [Jones and Laaser, 1977], [Cook, 1971]). It is easy to prove that they are also stable by expansion with unit clauses (i.e. if <I> belongs to such a class C then <I> u {11 · ... , In} (where li are unit clauses) belongs to C). Consequently, all these classes are tractable. Additionally, the classes of theories which result from any equivalence-preserving compilation technique (including FPio, FPI 1. FPI2, Ed compilations and all the techniques that remain to be discovered) are tractable (by definition). All these classes of theories can be used to generate theory prime implicates compilations. Incidentally, this shows that our approach can be considered complementary as well as supplementary to the existing (and future!) knowledge compilation techniques.

From a computational point of view, some additional advantages of our approach -that are not shared by many existing techniques- lie in the fact that theory prime implicates compilations are local. In particular, it is possible to enhance query-answering by checking in parallel whether 1t' 1= <I> 1t holds for every 1t' of TPI(I:, <I>). Furthermore, when the procedure used for checking whether n' 1= <I> 1t holds consists in determining whether li I= <I> 1t holds for every literal li of 1t', query-answering can be further improved by caching; caching simply consists in keeping track of the answer "yes" I "no" to the test li=<J> 1t for every literal I encountered so far. In this situation, the time complexity of query- answering becomes CXIPSI*I<I>u { 1t }la+ITPI(I:,<I>)I*log2(IPSI)) in the worst case. Interestingly, caching can be viewed as an additional compilation of TPI(I:, <I>) [Moses and Tennenholtz, 1993]. Indeed, n' 1= <I> 1t holds iff -,1t I= <I> -,1t' holds; the point is that the set of all the literals of PROPps is an efficient basis for the set of all the conjunctions of literals -,7t' of PROPps (see [Moses and Tennenholtz, 1993] for details).

Another valuable consequence offered by locality is the possibility to organize the theory prime implicates of I: w.r.t. <I> . Thus, attaching to each minimal implicate the frequency with which it is used to answer a query, we can order such implicates in a decreasing way. Since the ordering may vary dynamically, the organization of the compilation evolves with the queries and this may result in a an improvement of query answering with time. Interestingly, this is fully compatible with the common point of view stating that every piece of knowledge which is often used must be easy to remember. Clearly enough, such a behaviour is not guaranteed by the existing approaches to compilation (with [Reiter and de Kleer, 1987] as a notable exception) since they do not suggest any way to organize the knowledge.

Interestingly, our compilation technique can also be shown incremental and anytime. In fact, the results pointed out in [del Val, 1994] can be easily adaptated to our framework (the structure of TPI is close to the structure of FPio). Thus, provided that TPI uses an incremental prime implicate procedure inside, each time the knowledge base is revised (i.e. a new clause ~s added), recompiling the base from scratch is not mandatory. Note however that a small change in the knowledge base may result in a significant (and computationally expensive) change in the compilation (thus, from a computational point of view, incremental prime implicate algorithms do not behave better than non­ incremental ones in the worst case [Kean and Tsiknis, 1990]). A further advantage of our compilation technique is that it is anytime; it means that the knowledge base can be queried before compiling ends up. To be more precise, TPI can be interrupted at any time and produce some useful intermediate results nevertheless: while time passes, the number of queries that can be answered successfully increases and when the compiling process ends, every query can be answered. As [del Val, 1994] underlines it, the interest of this "convergent approximation" view of compilation is that it has the potential to greatly decrease the inconvenience of using off-line computation.

Despite many advantages, our approach to knowledge compilation does not overcome the main impediment of existing compilation techniques: there is no guarantee that the size of our compilation is not exponentially greater than the size of the original knowledge base. For instance, let us consider the empty theory <I> =def { } · The empty theory is tractable but theory prime implicates compilations with empty theory reduce to prime implicates compilations (cf. § 3). Hence, their size can easily be exponential in II:I [Chandra and Markowsky, 1978; Kean and Tsiknis, 1990]. In this situation, query answering, while tractable w.r.t. COMP<t>(I:), is still exponential in the size of I:.

However, our approach does not behave computationally worse than its predecessors in this respect since, for all the compilation techniques pointed out so far, an exponential growth of the knowledge base may result from compiling. Moreover, due to the complexity considerations pointed out in [Kautz and Selman, 1992], it is unlikely that a given compilation technique definitely outperforms by an exponential factor all its challengers for every possible knowledge base; indeed, a compilation technique s.t. compiling L results in a polynomial growth for every L is hardly to be expected.

Additionally, the size of COMPq, (L) can be advantageously compared with the size of PI(L) when the size of<!» is small w.r.t. the size of PI(L) (this condition is often satisfied when theories <!» are taken among subsets of the knowledge base L). Indeed, a direct consequence of Corollary 2 is that nb_cl(TPI(L, <!»)) ~ nb_cl(PI(L)).

Finally, we will show in section 5 that our compilations can also beat their challengers by an exponential factor in some situations. Since PI(L) is an instance of TPI(L, <!»), this shows incidentally that every tractable theory is not a good theory for the compilation purpose and that the choice of a "good" tractable theory may strongly bear on the efficiency of query answering from our compilations.

4.3 Pointing out "good", tractable theories

Since all the theory prime implicates compilations of L do not behave identically w.r.t. query answering from a computational point of view, a way to compare such compilations and a notion of optimal compilation of a knowledge base L must be defined. Intuitively, an optimal compilation is one that makes query answering the most efficient. However, we cannot define a unique criterion, significant and computable in practice, for characterizing the notion of optimal compilation in full generality.

In order to assess COMPq,(L) w.r.t. query answering in the worst case, a possible criterion c is the time complexity of<!» w.r.t. query answering per the size of TPI(L, <!»). Unfortunately, given a knowledge baseL, we did not find a procedure to point out, in time polynomial in ILl, a tractable theory <!» leading to an optimal COMPq,(L) w.r.t. c (we suspect that there is no such polytime procedure).

Instead, we propose a time-bounded heuristic search strategy through the space of tractable theories. Thus, our strategy basically consists in pointing out a potentially good tractable theory <!» from L, compile L w.r.t. <!», then retain C 0 M P q, (L) if it is better than every compilation encountered so far, reject it otherwise. The search terminates when a satisfying compilation has been found or when the time devoted to search is wasted. Clearly enough, our strategy is fully compatible with del Val's view of compilation as a process of increasing the efficiency and the quality of query answering over the life cycle of the knowledge base [del Val, 1994].

Applying this strategy requires to deal with the size of the space of tractable theories. It may exist a large number of tractable theories which are logical consequences of a given knowledge baseL ( and we surely do not know all of them!). Consequently, we need some criteria to prune the search space and focus on promising candidates <!» only. To this end, we mainly consider the time complexity of<!» w.r.t. query answering and an estimation of the computational resources to be spent to point out<!»; in particular, tractable theories that cannot be put forward in time polynomial in ILl are considered as a last resort. The logical strength of <!» is taken into account as an additional criterion (when it does not conflict with the two previous criteria). Indeed, in the light of Corollary 2, we know that it is sufficient to consider logically strongest theories only in order to minimize the number of clauses in the corresponding compilations. Since checking logical entailment is intractable in the general case, we focus in practice on computationally easier relationships between theories, particularly on set-inclusion.

Thus, given a knowledge base L , we will successively take into account as potentially good theories:

11 The set <!» of all the Hom clauses of L ,

21 The set <!» of all the binary clauses of L,

31 Subsets <!»of L such that the tied chain graph GT(<I») is acyclic (if so, <!» is unit-refutation complete [del Val, 1994]). 41 Sets Ed(<l») where<!» is a subset of L such that the induced width of<!» is lower or equal to 2 or the induced diversity of <!» is lower or equal to 1 (if so, <!» can be compiled under the form of a directional extension without an exponential growth [Dechter and Rish, 1994]).

51 Sets CF(<I») where CF is an equivalence-preserving compilation function (or CF is Horn_LUB [Selman and Kautz, 1991]) and<!» is a subset ofL, provided that ICF(<I»)I does not exceed 1<1»1 from more than around one order of magnitude.

When several choices are possible (steps 31 41 51), we prefer maximal sets<!» (w.r.t. set-inclusion) if we have a way to point them out in polynomial time in ILI1. Otherwise, we try to approximate them. If it is not possible, we pick up randomly any possible choice.

To restrict the search space further, an additional heuristic can be used; it consists in setting aside every theory <!» s.t. nb_cl(<l») I nb_cl(L) is lower than a given threshold. This may prevent us from taking into account unpromising theories (e.g. if there is no Horn clause in L, we jump directly to the set of all the binary clauses of L and we do not generate TPI(L, {}) = PI(L)).

Clearly enough, our strategy is very inefficient in the general case since an experimental post-hoc evaluation is necessary to check the choices that have been made. However, existing compilation techniques do not behave better here: in the general case, there is no way to estimate the size of a compilation before computing it2.

5 A comparison with some other approaches to knowledge compilation

Before comparing our approach with some existing techniques, we must define the way in which the comparison will be done. As a matter of fact, a crucial complexity factor of PI, FPio, FPI1. FPI2 and Ed compilations w.r.t. query answering is the size of the compilation (the number of clauses is equally significant when k-CNF knowledge bases are considered, cf. § 2).

I This is not possible in the general case. For instance, determining maximal subsets of l: that do not contain a tied­ chain by focusing on maximal acyclic subgraphs of GT(l:) cannot be done in time polynomial in ll:l in the general case since this last problem is NP-complete.

2 This is not exact for the approach of [Dechter and Rish, 1994] since the size of a directional extension is related to its induced width and to its induced diversity. These factors can be determined without computing the compilation but this does not help so much since determining a best ordering -i.e. one leading to a smallest induced width or a smallest induced diversity- is not tractable in the general case.

Since this is true for COMP<t> as well, we will compare our approach with PI, FPio, FPI1, FPI2 and Ed focusing on the number of clauses in the compilations.

Because l: does not fully characterize FPio(l:), FPI 1 (l:), FPI2(L) and Ed(L) in the general case, we must choose some FPio, FPI 1, FPI2 and Ect compilations among the possible ones; to be fair, we will compare our compilations with the best possible choices (i.e. FPio, FPI1, FPI2 and Ed compilations containing a minimal number of clauses).

5.1 Some examples for which our technique proves helpful

Our approach clearly outperforms any equivalence-preserving compilation function CF (including PI, FPio, FPI 1, FPI2 and Ed) whenever L = <I> u { c}, ICF(l:)l is exponentially greater than ll:l and ICF(<l>)l is polynomial in 1<1>1. Indeed, in such a situation, choosing CF(<l>) as a theory leads to the compilation COMP<J>(L) = <{ c }, CF(<l>)> and ICOMP<t>(l:)l is polynomial in ll:l while ICF(l:)l is exponentially greater than ll:l. In particular, when L is not known as tractable but <I> is, our approach proves valuable.

Example 2 (adaptated from [Kean and Tsiknis, 1990]) L =<ler{ -,pl v -,qll v r, -,pl V -,qlm V r, -,pk v -,qkl v r, -,pk v -,qkm v r, Pl v P2 v ... v Pk v r}.

With <I> =defL \ {Pl v P2 v ... v Pk v r }, we obtain:

nb_cl(COMP<t>(l:)) = 1 + m*k.

nb_cl(FPI1(L)) = 1 + m*k.

nb_cl(Ed(L)) =1 + m*k.

nb_cl(PI(l:)) = (m+1)k + m*k.

nb_cl(FPio(l:)) = (m+l)k + m*k.

nb_cl(FPI2(L)) = (m+l)k + m*k.

In this example, COMP<t> beats PI, FPio and FPI2 by an exponential factor. If we substitute each Pi with its negation and vice-versa, then the resulting <I> is unit-refutation complete (there are no tied literals in it). The results above still hold.

5.2 Preliminary experimental results

As a first step towards a comparison, we performed some preliminary experiments. We implemented our compilation technique and tested it on k-CNF knowledge bases l: drawn from diagnosis and qualitative physics. These knowledge bases are taken from [Forbus and de Kleer, 1993], allowing us to compare our results with PI and FPI1 compilations. For each problem under consideration, the theory <I> we have first considered is the subset of all the Horn clauses of L (it can easily be found in time linear in the size of l:).

Table I gives the number of clauses of the initial knowledge base, the number of clauses of the corresponding prime implicates knowledge base, the numbers of clauses of the FPI 1 compilation of l:, and finally the number of clauses of the theory prime implicates compilation of L w.r.t. <I>. FPI 1 (l:) corresponds to the compilations associated with the orderings of symbols which gave an optimal FPI 1 (l:) in each case [del Val, 1994].

Table 1 clearly shows that our approach can result in huge savings in the growth of the knowledge base by comparison with the prime implicates compilation. The savings we obtain w.r.t. FPI1 are often less significant. We do not know the numbers of clauses of the optimal FPio compilations associated with these knowledge bases. However, the knowledge base returned by FPio never is smaller than the knowledge base returned by FPI 1 when the same prime implicate algorithm is used inside both procedures. Hence, the savipgs obtained w.r.t. any optimal FPio are at least as significant as those obtained w.r.t. the corresponding optimal FPI 1 and they can be exponentially larger.

In contrast to our compilation, the performances of FPio and FPI 1 depend on the choice of a good ordering over the propositional symbols and, as [del Val, 1994] points out, we only have a very limited understanding of how to obtain such good orderings (hence, to find optimal FPio and FPI 1 compilations). Conversely, the performance of our approach depends on the existence and the choice of a good theory, i.e. a tractable theory such that the absolute growth of the corresponding compilation is reasonable (e.g. no more than around an order of magnitude). As shown in Table 1, this was the case for the theories used in our experiments.

Interestingly, using other theories can lead to still better savings in the growth of the knowledge base. We performed a few additional experiments to this end, focusing on the adder problem (see [Kean and Tsiknis, 1992] for its specification). In the first place, we have considered the set composed of the 16 last clauses of the specification (the "negation laws"). Since this set is composed of binary clauses only, it can be used as a tractable theory. The corresponding set TPI(l:, <I>) contains 698 clauses. This is a slight improvement w.r.t. the number of clauses obtained by using all the Horn clauses of the specification as a theory. We have also focused on the set composed of the 34 last clauses in the specification (all the clauses of the specification except the description of the behaviour of the two exclusive-or gates). In this set, every merge resolvent is subsumed by a clause of the original set. Accordingly, this set is identical to its FPio compilation, hence it is unit­ refutation complete [del Val, 1994]. Using it as a theory, we obtained a set TPI(l:, <l>) composed of 112 clauses only. Once more, this example shows that our own compilation technique can take advantage of the derivation of a tractable theory thanks to any other approach to compilation.

6 Conclusion

In this paper, we have been concerned with equivalence­ preserving logical compilation of propositional knowledge bases. The main contribution of this paper is a new approach to compilation, based on the concept of theory prime implicates, a generalization of the standard notion of prime implicates. Our approach can be viewed as an additional element in the panoply of techniques designed to deal with intractability of propositional query answering. Interestingly, our approach can also be viewed as complementary to its predecessors. Analytically and experimentally, we have shown that theory prime implicates compilation can achieve substantial space savings w.r.t. some other compilation techniques.

This work must be extended in several directions. A first direction concerns the empirical validation of the approach. More experiments are clearly needed to assess its practical applicability. A second direction is related to the choice of a good theory. We have only a very limited understanding of how to point out such good theories. Accordingly, the naive strategy we have proposed must be improved. More generally, the key problem of predicting whether a given compilation technique is well-suited to a given knowledge base should be addressed in the future.

Acknowledgements

The author would like to thank Alvaro del Val for several fruitful discussions and the anonymous reviewers for their helpful comments.