Semantical and Computational Aspects of Horn Approximations

1 Introduction

In a recent study [Selman and Kautz, 1991; Kautz and Selman, 1992] Selman and Kautz proposed a method, called Horn approzimation, for speeding up inference in propositional Knowledge Bases. Propositional infer­ ence is the problem of checking whether :E f= a holds, where :E and a are propositional formulae. The start­ ing point of their technique stems from the fact that inference for general propositional formulae is co-NP­ complete -hence polynomially unfeasible- while it is doable in polynomial time when :E is a Horn formula. The fascinating question they address is the following: is it possible to compile a propositional formula :E into a Horn one :E' so that a significant amount of the in­ ferences that are performed under :E can be performed under :E' in polynomial time?

·work supported by the ESPRIT Basic Research Action N.3012-COMPULOG and by the Progetto Finalizzato Sis­ temi lnformatid e Calcolo Parallelo of the CNR (Italian Re­ search Council).

Selman and Kautz notice that there exist two different ways of doing such a compilation. In the first case the compiled formula satisfies the relation :E' f= :E, or equiv­ alently M(:E') ~ M(:E) -where M( ~) denotes the set of models of the formula ~. For this reason :E' is called a Horn lower bound -or LB- of :E. As an example­ taken from [Selman and Kautz, 1991]-let ~be the for­ mula (man --+ person) 1\ (woman --+ per son) 1\ (man V woman). The formula ~lb =man 1\ woman 1\ person is a Horn LB of~.

The second form of compilation is dual. The compiled version of :E is a Horn formula :E' that satisfies the re­ lation :E f= :E', or equivalently M(:E) ~ M(:E'). :E' is called a Horn upper bound -or UB- of :E. Returning to the previous example, the formula ~ub = (man --+ person) 1\ (woman--+ person) is a Horn UB of~.

The importance of having compiled forms of a Knowl­ edge Base is in that sometimes we can use them for pro­ viding a quick answer to an inference problem. As an example, if we are faced with the problem of checking :E f= a, we may benefit from the fact that for any Horn LB :Etb of :E, :Etb ~ a implies :E ~ a. :Etb is therefore a complete approzimation of :E. Dually, a Horn UB :Eub is a sound approzimation of :E, since :Eub f= a implies :E Fa.

Selman and Kautz notice that some complete ap­ proximations are better than others. In the previous example, both ~lbl = man 1\ woman 1\ person and ~tb2 = man 1\ person are Horn LBs of~. ~lb2 seems to be a better approximation than ~lbl, since M( ~lbl) C M(~tb2) C M(~), hence the former is in some precise sense "closer" to ~ than the latter. This consideration leads to the notion of Horn greatest lower bound -or GLB- of a formula :E, which is a Horn formula :Eglb such that M(:Egtb) ~ M(:E) and for no Horn formula :E' it holds that M(:Egtb) C M(:E') ~ M(:E). In the previous example ~lb2 is a Horn GLB of~.

The same argument can be done for Horn upper bounds: in our example both ~ubl = (man --+ person) 1\ (woman --+person) and ~ub2 =person are Horn UBs of~. but M(~) C M(~ub2) C M(~ubt), hence ~ub2 is a better approximation of~. A Horn least upper bound -or L UB- of a formula :E is a Horn formula :Etub such that M(:E) ~ M(:Eiub) and for no Horn formula :E' it holds that M(:E) ~ M(:E') C M(:Etub)· ~ub2 is a Horn LUB of~.

Selman and Kautz's proposal is to approximate inference wrt a propositional formula :E by using its Horn GLBs and L UBs. In this way inference could be unsound or incomplete, but it is anyway possible to spend more time and use a general inference procedure to determine the answer directly from the original formula. The general inference procedure could still use the approximations to prune its search space (see [Selman and Kautz, 1991, page 905]). It is also important to notice that Horn GLBs and LUBs can be computed off-line, hence this form of approximate reasoning is actually a compilation.

Table 1 summarizes the major properties of Horn GLBs and LUBs stated in [Selman and Kautz, 1991; Kautz and Selman, 1992]. The four columns refer re­ spectively to:

• logical relation wrt :E (i. e. what kind of inference can be performed using this approximation?);
• size of the formula wrt the size II: I of :E;
• number of possible approximations of this kind;
• computational complexity of the search problem of finding the approximation.

Horn approximations have two computational problems: 1) computing them is an NP-hard task and 2) due to its exponential size, it may be impossible to store the Horn LUB. About the first aspect Selman and Kautz notice that since approximations could be computed off-line, the computational cost of finding them will be amortized over the total set of subsequent queries to the Knowledge Base. With respect to the second aspect, they propose in [Kautz and Selman, 1992] a technique for "compressing" the Horn L UB into a (quasi-)equivalent formula. Due to reasons related to circuit complexity theory, it is not possible to apply the technique in general (see [Kautz and Selman, 1992] for further details).

Other computational properties of Horn approxima­ tions are studied in [Greiner and Schuurmans, 1992; Roth, 1993].

In this paper we address two important questions that have not been addressed so far:

1. is it possible to describe Horn approximations with a semantics that does not rely on the syntactic notion of Horn clause?
2. what is the exact complexity of finding Horn ap­ proximations?

An answer to the first question shows the exact meaning of the approximate answers. An answer to the second question tells in which cases it is reasonable -from the computational point of view- to use Horn approxima­ tions.

We obtain two different kinds of results:

semantical

• Horn GLBs of :E are closely related to models of the circumscription of :E;
• reasoning wrt Horn GLBs is the same as rea­ soning by counterexamples using only minimal models;
• while 1keptical reasoning wrt the Horn GLBs of a formula :E is the same as ordinary reasoning wrt :E, brave reasoning wrt the Horn GLBs of :E is the same as reasoning wrt CIRC(:E);
• compiling more knowledge does not always give better Horn GLBs;
• reasoning wrt the Horn L UB can be mapped into classical reasoning;
• the Horn LUB of :E is related to CW A(:E).

computational

• finding a Horn G LB is "mildly" harder than solving the original inference problem;
• reasoning wrt the Horn L UB is exactly as hard as solving the original inference problem;
• finding a Horn UB is a search problem that cannot be parallelized.

We believe that our results provide useful criteria that may help finding a knowledge compilation policy. In particular, we show that an interesting tradeoff seems to emerge between the computation done during the compi­ lation time and the computation done during the query answering time.

The structure of the paper is as follows: in . Section 2 and 3 we study Horn GLBs and LUBs, respectively; we discuss our results in Section 4.

2 Horn GLBs

In this section :E denotes a propositional formula and :E91b denotes one of its Horn GLBs. We assume that both of them are in CNF. We start with some considerations on the syntactic form of Horn GLBs.

In [Selman and Kautz, 1991] a Horn-1trengthening of a clause "Y is a Horn clause "YH such that "YH ~ "'( and there is no Horn clause "'fk such that "YH C "YH ~ "Y· As noticed in [Selman and Kautz, 1991, Lemma 2], every clause in :Egtb is a Horn-strengthening (i. e. a "witness") of a clause in :E. On the other hand we can easily prove that for each clause in :E there is at least one Horn­ strengthening ("witness") in :Eglb·

In thP. following two subsections we prove that Horn GLBs of a formula :E are closely related to the minimal models of :E. Minimal models of a propositional formula have the property that the set of atoms that they map into 1 is minimal. More formally (see [Lifschitz, 1985]), given two models M, N of a formula, we write M ~ N iff

{zj M(z) = 1} ~ {zl N(z) = 1} and we write M < N iff the containment is strict. The models of a formula ~ that are minimal in this preorder are called the minimal mod­ els of ~. Minimal models are important in the theory of non-monotonic reasoning, since the)' are the seman­ tical counterpart of circumscription [McCarthy, 1980; Lifschitz, 1985]: The models of CIRC(I:) are exactly the minimal models of I:.

We recall that Horn formulae have a unique minimal model (the minimum model).

2.1 FroDl GLBs to llliniDlal Dlodels

Let I: be a propositional formula and I:glb a Horn GLB of I:. We prove that the minimum model M of I: 8 ,, is minimal for I:, thus proving that if a Horn GLB of I: is known, then it is possible to obtain in linear time a minimal model of I: (see [Dowling and Gallier, 1984]).

First of all we notice that M is also a model of I:. Now, let's assume that M is not minimal, and let N be a model of I: such that N < M. We prove that we can build a Horn formula U such that M(I:gtb) C M(U) ~ M(I:), thus contradicting the assumption that I:glb is a Horn GLB of I:.

The Horn formula U is built as follows:

begin

unmark all the clauses of I:; U :=true; for each clause "'( = a1 V · · · V am V -,bt V · · · V ...,b,. of I: do fori:= 1 tom do if N(a,) = 1 then begin (* add a Horn-strengthening of 'Y *) u := u 1\ (ao v ...,b1 v · · · v ...,b,.); mark 'Y end; for each unmarked clause 'Y of I: do begin end. let "'( 1 be (one of) the witness(es) of"'( in I:gtbi u := u /\"'( 1 j end;

Since U is a collection of Horn-strengthenings of I:, M(U) ~ M(I:) holds. It is easy to prove that N is a model of U: 1) N clearly satisfies all the clauses in U that come from marked clauses of I:; 2) N must sat­ isfy at least one negative literal of each clause "'( 1 in U that comes from an unmarked clause 'Y of I:, otherwise 'Y would have been marked.

Now we prove that M(I: 8 ,,) C M(U) holds. Since N E M(U) and N ft M(I: 8 ,,), it is sufficient to prove that M(I: 8 ,,) ~ M(U). Let's take a generic model P of I: 9 ,,; we prove that it is also a model of U. Since P is a model of I: 9 ,,, M < P must hold, hence N < P holds too. As a consequence P satisfies all the clauses in U that come form marked clauses of I:. As far as the other clauses of U are concerned, they are clauses of Eglb as well, therefore P satisfies all of them.

The following theorem summarizes the above result.

TheoreDl 1 Let I: be a propositional formula and I: 9 ,, a Horn GLB of:E. The minimum model of:E 9 ,, is minimal for I:.

Theorem 1 implies that if we have a Horn GLB of I:, then we can obtain in linear time (see [Dowling and Gallier, 1984]} a minimal model of I:. More techni­ cally, the theorem shows a polynomial reduction from the search problem of finding a minimal model of I: to the search problem of findin~ a Horn GLB of I:. The present author analyzed in [Cadoli, 1992] the compu­ tational complexity of the search problem of finding a minimal model of a propositional formula. One of the results of that paper is that finding a minimal model of a formula I: is hard (using many-one reductions) with respect to the class pNP(O(log n)J. 1 It is important to remark that pNP[O(log n)Lhard problems are in a precise sense computationally harder than NP-complete or co­ NP-complete problems 2 · We recall that the problem of deciding whether I: f: a holds is co-NP-complete.

As shown in [Cadoli, 1992], pNP(O(log n)Lhardness of finding a minimal model holds even if a model of I: is known. This fact can be compared with a consideration in [Selman and Kautz, 1991, Theorem 1]: I: 9 ,, is sat­ isfiable iff I: is satisfiable, hence finding a Horn GLB is NP-hard. We can now say that even if we know that I: is satisfiable and have one of its models in hand, finding a Horn GLB is still pNP(O(log n)Lhard. We recall that finding a model (not necessarily minimal) of a propositional formula is per se an NP-hard task.

Corollary 2 Finding a Horn GLB of a propositional formula I: is pNP(O(log n)Lhard. Thill holds even if a model of I: is already known.

We notice that the above corollary gives us just a lower bound. It is reasonable to ask how easy is to find a Horn GLB, i. e. to give an upper bound to the problem. In [Selman and Kautz, 1991] an algorithm for computing a Horn GLB of a formula I: is shown. The algorithm performs an exponential number of polynomial steps. It is possible to show that a Horn GLB can be found in polynomial time by a deterministic Turing machine with access to an NP oracle, i. e. to prove that the problem is in the class pNP. This means that we only need a polynomial number of queries to the GLB in order to "pay off" the overhead of the knowledge compilation.

2.2 FroDl llliniDlal Dlodels to GLBs

We now show that if we have a minimal model M of a formula I:, then we can easily build a very good approx­ imation of a Horn GLB of I:. In particular we show that we can build in linear time a Horn LB of I: whose min­ imum model is M. This result allows us to perform, in the following subsection, some interesting considerations on the semantics of Horn GLBs.

1 pNP[O(io11 n)) is the class of decision problems that can be computed by a polynomial-time deterministic machine which can use for free an oracle (or subroutine) that answers a set ofNP-complete queries (e. g. satisfiability checks) whose car­ dinality is bound by a logarithmic function. We refer the reader to [Johnson, 1990] for a thorough description of all the complexity classes that are cited in this paper.

2 Both NP-complete and co-NP-complete problems can be solved with a 1ingle call to an oracle in NP.

We build a Horn LB W of :E, whose minimum model isM. Moreover, we prove that there is a Horn GLB of:E whose minimum model is also M. W is built as follows:

begin

unmark all the clauses of :E; W :=true; for each clause "{ = a1 V · · · V a,. V ·bt V · · · V ·b,. of :E do for i : = 1 to m do if M(<~i) = 1 then begin W := W 1\ (a, V ·b1 V · · · V ·b,.); mark"/ end; for each unmarked clause "Y = end. a1 V · · · V am V ·bt V · · · V ·b,. of :E do w := w 1\ (·bt v ... v ·b,.);

M is clearly a model of W, since 1) M satisfies all of the clauses in W that come from marked clauses of :E, 2} M must satisfy at least one negative literal of each clause "'( 1 in W that comes from an unmarked clause "Y of :E, otherwise "Y would have been marked. Since W is a collection of Horn-strengthenings of :E, M(W) ~ M(:E) holds. As a consequence M is the minimum model of w.

W is aLB of :E, but it might be not a Horn GLB. As an example if:E = ·aVb, M(a) = M(b) = 0, then W = ·a. Let V be a Horn GLB of :E such that M(W) C M(V). It is easy to prove that M is the minimum model of V: all of the models of V must be greater or equal than its minimum model; since M is a model of V and no model of :E is smaller than M, M is the minimum model of V.

Theorem 3 Let M be a minimal model of :E. There i6 a Horn GLB of :E who6e minimum model i6 M.

2.3 Semantical consequences

Theorems 1 and 3 can be summarized as follows.

Theorem 4 The set of minimal models of a formula :E and the 6et of minimum model! of the Horn GLB6 of :E are the 6ame.

We now address some interesting semantical conse­ quences of the above results.

As noticed in [Selman and Kautz, 1991] a traditional AI approach is reasoning by counterezample6, which con­ sists in refuting a possible consequence of a theory by means of a suitable model that contradicts it (an ex­ ample of this technique is in the early work [Gelernter, 1959]}. This approach is based on the well-known prop­ erty M ~ a ==:} :E ~ a, that holds for any pair of for­ mulae a, :E and any model M of :E. Selman and Kautz indicate that reasoning under a specific Horn GLB is an improved version of such a reasoning schema, since a single Horn GLB captures a 6et of models of the orig­ inal theory. Using Theorem 4 and the well-known fact that the minimum model of a Horn formula completely characterizes the set of its positive consequences, we can say that, as far as positive theorems are concerned, rea­ soning under Horn GLBs is the same as reasoning by counterexamples using only minimal models. This does not hold for negative theorems.

Selman and Kautz address briefly the issue of how rea­ soning with respect to a set of Horn GLBs looks like, proving [Selman and Kautz, 1991, Theorem 3] that a formula is equivalent to the disjunction of all its Horn GLBs. The notions of 6/ceptical and brave reasoning are frequently used in the literature. We say that a formula a skeptically follows from the Horn GLBs of a formula :E (written 6/cep-glb(:E) 1- a) if for each of its Horn GLBs :Eglb it holds :Eglb F= a. We also say that a bravely fol­ lows (written brave-glb(:E) 1- a) if there exists a Horn GLB :Eglb such that :Eglb F= a. .

The result by Selman and Kautz can be rephrased in the following way: 6/cep-glb(:E) 1- a iff :E F= a. Us­ ing Theorems 1 and 3 we can say that - as far as positive theorems are concerned - brave reasoning wrt Horn G LBs is the same as brave reasoning wrt mini­ mal models. More precisely let a be a positive clause, brave-glb(:E) 1- a iff there exists a minimal model M of :E s. t. M F= a, i. e. iff CIRC(:E) ~ ·a (see [Lifschitz 1985]). Using a result shown in [Eiter and Gottlob, 1991j we can say that brave reasoning wrt Horn GLBs is a de­ cision problem which is hard wrt the class :E~ of the polynomial hierarchy.

Let us see how the relation with non-monotonicity just shown affects approximate inference under Horn GLBs. We consider two knowledge bases :E, :E+ such that M(:E+) C M(:E), i. e. :E+ F= :E and :E ~ :E+. It is well known that for a generic formula a, CIRC(:E) F= ·a does not imply CIRC(:E+) F= ·a, even if:E+ ~a holds. Using the relation (CIRC(:E) F= ·a) iff (brave-glb(:E) If a) we prove the following result.

Proposition 5 Let :E, :E+ be two formulae 6uch that :E+ F= :E and :E ~ :E+; let a be a po6itive clau6e. If :E+ ~ a and brave-glb(:E) If a then it might be the ca6e that brave-glb(:E+) 1- a.

We recall that reasoning using a generic Horn GLB is complete and unsound wrt reasoning using the original formula. In other words if brave-glb(:E) If a then we know that :E ~ a, i. e. a is disproved. Proposition 5 says that if we are able to disprove a formula a using any complete compilation of a "small" formula :E, then we are not guaranteed that we are able to disprove a using a generic complete compilation of a "bigger" formula :E+, even if :E+ ~ a. In other words it is not true that com­ piling more knowledge we always have better complete approximations. As an example, let :E = ·a V ·b and :E+ = :E/\(avb). Clearly :E+ ~a and brave-glb(:E) If a. Moreover brave-glb(:E+) 1- a, as :E+ has two different Horn GLBs: (a 1\ ·b) and ( ·a 1\ b).

For the sake of completeness, we notice that brave-glb(:E) 1- a does not imply brave-glb(:E+) 1- a: this can be seen if :E = a V b, :E+ = :E 1\ b and a = a.

3 Horn LUB

In this section :E denotes a propositional formula and :Etub denotes its Horn LUB. As shown in [Kautz and Selman, 1992] in general it is not possible to store efficiently the Horn LUB of I:. In particular the size of I:, .. , can be exponential in the size of I:, and this seems to be inde­ pendent on the representation used for I:, .. , (see [Kautz and Selman, 1992] for further details). As a consequence any method for efficiently representing the Horn LUB is incomplete. In [Selman and Kautz, 1991, page 908] the authors propose to approzimate the Horn LUB with Horn upper bounds of limited length. This idea is used in [Greiner and Schuurmans, 1992], where Horn UBs with a limited number of Horn clauses are studied. In Sub­ section 3.1 we investigate about this idea and analyze its computational properties. Other computational proper­ ties of Horn LUBs are addressed in Subsection 3.2. In Subsection 3.3 we make a brief semantical remark.

3.1 Horn UBs with a limited number of clauses

I:1 .. , is logically equivalent to the conjunction of all the Horn prime implicates of I: [Selman and Kautz, 1991, Theorem 4]. I:, .. , therefore guarantees sound and com­ plete reasoning wrt I: as far as inference of Horn formu­ lae is concerned: for all Horn formulae a, (I:, .. , Fa) iff (I: Fa). One natural choice is to approximate I:, .. , with a formula that guarantees sound and complete reasoning wrt I: as far as inference of 6hort Horn formulae is con­ cerned. As an example of this kind of approximation, we define the formula :r:;, to be the conjunction of the for­ mulae in the set {~I ~ is a positive literal and I: F ~}. Notice that :r:;, is a Horn UB of I:. This formula is a reasonable approximation of I:, since 1) at least all the positive atomic queries are answered correctly and 2) it has a nice short representation.

An interesting question is the following: how difficult is to obtain I:~,? We notice that finding I:~, is the search problem that amounts to decide for each propositional variable ~ occurring in I: whether I: F ~ holds. It is well known that just deciding I: F ~ for a single propositional variable is co-NP-complete, but it is important to under­ stand if the task of deciding I: F ~ for many proposi­ tional variables can be parallelized. In other words we are interested in the following practical problem: is it possible to obtain I:~, with one -or few- queries to a propositional theorem prover, or is it the case that the best strategy is just to ask separately for each proposi­ tional variable ~ of I: whether I: F ~ holds? Clearly if it is possible to parallelize the process of building I:~, -or any other approximation of I:, .. ,- then we have better chances to obtain good approximations of I:, .. ,.

Several authors (see for example [Beigel, 1988; Krentel, 1988]) studied the computational complexity of search problems of the kind we are addressing here. The goal of the research in this field is to understand "how much NP-hardness" does an NP-hard problem con­ tain. The problem QUERY, which is a generalization of the standard satisfiability problem SAT, is defined in [Krentel, 1988]. The input of QUERY are k propositional formulae T1, ... , T,. and its output are k bits b1, ... , b,., where for any i (1 ::; i ::; k ), b, = 1 if 11 is satisfiable, and b, = 0 if 11 is not satisfiable. Beigel shows in [Beigel, 1988] that it is very unlikely that QUERY can be solved with less than k queries to a SAT oracle. In other words it seems that any strategy for solving QUERY cannot be better than solving independently the k corresponding SAT problems. A general property of this kind of NP­ hard problems (see [Beigel, 1988] for further details) is that it is not possible to gain efficiency via paralleliza­ tion.

QUERY can be immediately mapped into the problem of finding the approximation I:~, of a given formula I: . Moreover the proof can be immediately adapted to the problem of finding any set of Horn prime implicates of I:.

This result can be interpreted in the following way: the task of finding short approximations ofi:1 .. , -like for example I:~,- contains "a lot of NP-hardness". There seems to be a direct correspondence between the size of the approximation and the computational effort that we need to obtain it. As a consequence there is little hope to obtain good approximations of I:, .. , by performing few calls to a theorem prover.

3.2 How hard is to decide I:, .. , Fa?

In the previous subsection we addressed the issue of how hard is to compile I:, and in particular how hard is to ob­ tain an approximation of I:, .. ,. In this subsection we are interested in another computational property of I:, .. ,: we want to know how hard is to reason wrt I:, .. ,, regardless of the representation of this formula that we are cur­ rently storing in our memory. In other words we want to understand what is the exact complexity of deciding I:, .. , Fa, assuming that the inputs are I: and a.

We assume that the formula a is in CNF. In partic­ ular, let a be a clause ·b1 V · · · V ·bm V a1 V ···Van, that we denote as f3 ----t a1 V · · ·Van, where f3 is a short­ hand for the conjunction b1 1\ · · · 1\ bm. It is not hard to prove that inference wrt I:1 .. , can be mapped into clas­ sical inference. Let £ be the set of letters that occur in I:, £1, ... , Cn be n disjoint sets of letters of the same arity of£ and I: 1 , ... , :r:n be n duplicates of I: built on £ 1, ... , Cn, respectively. In an analogous way we define /3 1 , ... , pn. I:, .. , F a holds iff

This proves that the problem of deciding I:, .. , F a can be solved by means of a single call to a propositional theorem prover. More formally, I:, .. , F a is a co-NP­ complete problem, i. e. it has exactly the same complex­ ity as the original problem of deciding I: F a.

Summarizing all the results presented so far we can say that:

1. it is not possible to represent I:1 .. , explicitly in the memory;
2. we can make I:, .. , partially explicit; this is doable off-line but it is more difficult than the original task of reasoning wrt I:;
3. if we keep I:, .. , completely implicit then reasoning wrt it is exactly as hard as reasoning (on-line) wrt I:.

An interesting tradeoff therefore exists between the amount of compilation that we want to perform off-line and the amount of reasoning that we want to do on-line.

3.3 A se111antical re111ark

Equation (1) gives a sound and complete characteriza­ tion of inference wrt :Etub in terms of classical propo­ sitional inference. In this subsection we make a brief remark about the relation existing between Horn LUBs and closed-world assumption [Reiter, 1978].

Observation 6 Let M be the minimum model of :Etub· M i6 the inter6ection of all the minimal model6 of :E. Therefore M i6 a model of :E iff the clo6ed-world a66umption CW A(:E) of :E i6 con6i6tent.

We notice that CW A(:E) may be consistent even if :E is non-Horn: The CWA of ·a V b V c is consistent. Re­ lations between Horn LUBs and closed-world reasoning are implicit in the works [Borgida and Etherington, 1989; Selman and Kautz, 1991].

4 Discussion

The computational results that we have seen in Sec­ tions 2 and 3 show that when we deal with knowledge compilation there exists an interesting tradeoff between computation during compile time (off-line) and compu­ tation during query-answering time (on-line).

In Section 2 we have seen that the computational effort of finding a Horn GLB is justified only if a significant number of queries to it will be done. In particular we have seen that the compilation is more expensive than a set of query answering tasks. The size of such a set has a lower bound which is a function logarithmic in the size of the input and an upper bound which is a function polynomial in the size of the input.

In Section 3 we have obtained similar results, showing that high-quality Horn UBs need a significant computa­ tional effort.

Since compilation causes anyway loss of information (either soundness or completeness), the computational effort spent in the compilation must be comp~ed to the quality of the inference obtained. It is an open issue to find an adequate formal framework for comparing the two aspects.

Acknowledg111ents

I am grateful to H. Kautz and B. Selman for fruitful dis­ cussions on their method. I had interesting discussions also with L. C. Aiello, M. Lenzerini, E. Omodeo and M. Schaerf, who also read previous versions of the paper. Thanks to D. Schuurmans for sending me a preliminary version of his paper.