Complexity Results for Propositional Closed World Reasoning and Circumscription from Tractable Knowledge Bases

1 Introduction

Closed world reasoning (CWR) is a widely used inference technique in Artificial Intelligence, Database Theory and Logic Programming. It relies on the idea that negative information is often not represented in an explicit way; in this situation, every piece of positive information which cannot be deduced from a knowledge base (KB) is as­ sumed false.

In order to define CWR in a formal way, an approach consists in characterizing the formulas which must be assumed false in the KB: CWR is then viewed as deduc­ tion from the closure of the KB, i.e., the KB completed with these assumptions. Several policies for characteriz­ ing such assumptions have been developed so far, giving rise to several forms of CWR. Let us mention the (ba­ sic) closed world assumption (CWA) [Reiter, 1978], the generalized closed world assumption (GCWA) [Minker, 1982], the extended generalized closed world assump­ tion (EGCWA) [Yahya and Henschen, 1985], the careful closed world assumption (CCWA) [Gelfond and Przy­ musinska, 1986], and the extended closed world assump­ tion (ECWA) [Gelfond et al. , 1989]. The most sophisti­ cated closed world assumption is ECWA; in the propo­ sitional case, Gelfond, Przymusinska and Przymusinski

Pierre Marquis

CRIL /U ni versi te d 'Artois rue de l'Universite, S.P. 16 62307 Lens cedex - France

[1989] show it is equivalent to circumscription, as defined in [McCarthy, 1986].

The complexity of propositional CWR has already been investigated by several researchers. Eiter and Got­ tlob [1993] show that CWR is hard in the general case: typically at the second level of the polynomial hierar­ chy. Cadoli and Lenzerini [1994] focus on the complexity of CWR from various fragments of propositional logic for which clause deduction is tractable, especially the Horn CNF class, the reverse Horn CNF class and the Krom one. For such classes of formulas, the complexity of CWR falls one level down in the polynomial hierarchy.

The aim of this paper is to complete the complexity results pointed out in [Cadoli and Lenzerini, 1994] by focusing on some other tractable fragments of proposi­ tional logic. Especially, four classes are considered:

• The Blake class is the set of formulas given in prime implicates normal form,
• the DNF class is the set of formulas given in dis­ junctive normal form (DNF),
• the Horn cover class is the set of disjunctions of Horn CNF formulas ,
• the renamable Horn cover class is the set of disjunctions of renamable Horn CNF formulas . ·

As a main contribution, the complexity of clause in­ ference is identified for each form of CWR and each tractable class listed above. Several new tractable sub­ cases are exhibited for each form of CWR; some new intractable subcases are presented as well.

Interestingly, our tractability results for CWR apply to classes of formulas strictly more expressive than some of the most expressive tractable fragments for CWR pointed out up to now. In particular, some of the classes we focus on include classes considered in [ Cadoli and Lenzerini, 1994] as strict subcases. Additionally, the fragments we consider are target classes for exact knowl­ edge compilation functions . Thus, every propositional formula can be turned ("compiled") into a formula from the Blake class (the target class for the compilation func­ tion given in [Reiter and de Kleer, 1987]) , the DNF class (the target class for the function given in [Schrag, 1996]), the Horn cover class and the renamable Horn cover class (which are specific instances of the class of tractable covers considered in [Boufkhad et al., 1997]). Since CWR from such tractable formulas is shown com­ putationally easier than CWR from unconstrained for­ mulas, our study suggests a two step approach to com­ pute CWR: the KB is first compiled off-line, giving rise to a formula from one of the target classes, then queries are addressed on-line w.r.t. the compiled KB. While such a pre-processing is known as not computationally helpful in the general case, our results indicate that it can prove valuable when CWR from the compiled KB can be achieved in polynomial time, as long as the KB does not often change and the size of its compiled form remains "small enough".

The rest of this paper is organized as follows. Some formal preliminaries are given in Section 2. Basic defi­ nitions and complexity results about CWR are recalled in Section 3. Section 4 presents the complexity of CWR for each of the fragments we focus on. Section 5 con­ cludes the paper. Proofs are given in [Coste-Marquis and Marquis, 1999) available from the authors.

2 Formal Preliminaries

PROPps denotes the propositional language built up from a denumerable set P S of symbols and the connec­ tives in the standard way. The size of a formula I: from PROPps, noted I I: I, is the number of signs (symbols and connectives) used to write it. Every propositional sym­ bol of P S is also called a positive literal and a negated one a ne~ative literal. For every subset V of PS, Lv (resp. Lv, L"V) is the set of literals (resp. positive lit­ erals, negative literals) built up from the propositional symbols of V. V ar(I:) denotes the set of propositional symbols occurring in I:.

Formulas are interpreted in the classical way. Every set of formulas is interpreted conjunctively. A formula is Horn CNF (resp. reverse Horn CNF) iff it is a CNF formula s.t. every clause in it contains at most one pos­ itive (resp. negative) literal. A Krom formula is a CNF formula in which every clause contains at most two liter­ als. A renamable Horn CNF formula I: is a CNF formula which can be turned into a Horn CNF formula by sub­ stituting in a uniform way in I: some literals of Lvar(E) by their negation.

We assume that the reader is familiar with some basic notions of computational complexity, especially the com­ plexity classes P, NP, and coNP, and the classes ~1, I:1 and II1 of the polynomial hierarchy PH (see [Papadim­ itriou, 1994) for details). The class pX[O(Iogn)) contains the decision problems which can be solved in polyno­ mial time with no more than O(log n) calls to an oracle for deciding a problem Q E X for "free" (i.e., within a constant time), n representing the size of the problem instance. Let us recall that a decision problem is said at the kth level of PH iff it belongs to ~1+1, and is either I:~-hard or II~-hard. It is strongly believed that PH does not collapse (at any level), i.e., is a truly infinite hierar­ chy (for every integer k, PH "I I:D.

3 Closed World Reasoning

All the forms of CWR pointed out so far can be charac­ terized through the notions of closure and free for nega­ tion formula. A clause 'Y is then considered as a (non monotonic) consequence of a KB I: interpreted under some closed world assumption policy *CW A (where the generic character* can be replaced by G, EG, CC, E or the empty string) iff it is a logical consequence of the clo­ sure of I: w.r.t. the policy. Both the CCWA and ECWA policies require V ar(I:) to be partitioned into three sets, P, Q, and Z. P contains the symbols preferred false, Z contains the symbols the truth value of which can vary when trying to falsify the symbols from P, and Q con­ tains the symbols the truth value of which cannot vary.

Definition 3.1 (closure of a KB)

Let *CW A be any closed world assumption policy among (basic) CW A, GCW A, EGCW A, CCW A and ECW A. Let I: be a formula from PROPps and (P, Q, Z) a par­ tition ofVar(I:). The closure *CWA(I:,(P,Q,Z)) 1 of I: given (P, Q, Z) w. r. t. *CW A is the formula I: U { ·a ; a is a *CW A-free for negation formula w.r.t.

I: and (P,Q,Z)}.

The *CW A-free for negation formulas w.r.t. I: are the negations of the formulas which are assumed false when they are not deducible from I:. They vary according to the closed world assumption policy under consideration:

Definition 3.2 (*CWA-free for negation formula) Let I: and a be two formulas from PROPps and let (P, Q, Z) be a partition of V ar(I:).

• a is CW A-free for negation iff a is a positive literal s.t. I: ~a holds.
• a is GCW A-free for negation iff a is a positive lit­ eral and for each positive clause 'Y s.t. I: ~ 'Y holds, I: ~a V 'Y holds.
• a is EGCW A-free for negation iff a is a conjunc­ tion of positive literals and for each positive clause 'Y s.t. I: ~ "( holds, I: ~a V 'Y holds.
• a is CCW A-free for negation iff a is a literal from L t and for each clause 'Y containing only literals from Lt U LQ and s.t. I: ~ "( holds, I: ~ a V "( holds.
• a is ECW A-free for negation iff Var(a) n Z = 0 and for each clause 'Y containing only literals from Lt U LQ and s.t. I: ~ 'Y holds, I: ~a V 'Y holds.

Let us note that every symbol not belonging to Var(I:) is CW A, GCW A and EGCW A-free for negation. As to CCW A and ECW A, every symbol from PS\ Var(I:) is assumed to belong to P.

In the rest of this paper, the following decision prob­ lems are considered:

Definition 3.3 (*CWA clause inference)

Let *CW A be any closed world assumption policy among

1 The partition of Var(l:) is not significant for the CW A, GCW A and EGCW A policies.

(basic) CW A, GCW A, EGCW A, CCW A and ECW A. *CW A CLAUSE INFERENCE is the following decision problem:

• Input: A formula~ and a clause 1 from PROPps, a partition (P, Q, Z) of Var(~) and a CWA policy *CWA.
• Query: Does *CW A(~, (P, Q, Z)) f= 1 hold?

*CW A LITERAL INFERENCE is the restriction of the corresponding *CW A CLAUSE INFERENCE problem where 1 is restricted to be a literal.

The complexity of propositional CWR has been in­ vestigated by several researchers, especially Eiter and Gottlob [1993) and Cadoli and Lenzerini [1994). CWR has been shown hard: all the forms of CWR except basic CWA are at the second level of the polynomial hierar­ chy. Thus, CWR is computationally harder than deduc­ tion in the general case (CLAUSE DEDUCTION is "only" coNP-complete), unless PH collapses.

In order to circumvent this complexity, several ap­ proaches can be considered. One of them is cen­ tered around the idea of exact knowledge compilation. Knowledge compilation can be viewed as a form of pre­ processing (see [Cadoli and Donini, 1998) for a survey): the original KB is turned into a compiled one during an off-line compilation phase and this compiled KB is used to answer the queries on-line. Assuming that the KB does not often change and that answering queries from the compiled KB is computationally easier than answer­ ing them from the original KB, the compilation time can be balanced over a sufficient number of queries.

Existing researches about knowledge compilation can be split into two categories. The first category gath­ ers theoretical works about compilability, which indi­ cates whether or not the objective can be expected to be reached in the general case by focusing on the size of the compiled form (see e.g., [Cadoli et al., 1997a; Liberatore, 1998]) . Indeed, if the size of the compiled form is exponentially larger than the size of the original KB, significant computational improvements are hard to be expected. Some decision problems are compil­ able, while others are (probably) not compilable. Thus, CLAUSE DEDUCTION (from a fixed KB) is (probably) not compilable: the existence of an equivalence-preserving compilation function COMP s.t. it is guaranteed that for every propositional CNF formula~' CLAUSE DEDUC­ TION from COM P(~) is in P and I COM P(~)l is polyno­ mially bounded in 1~1 would make PH to collapse at the second level (see [Kautz and Selman, 1992; Cadoli et al., 1997a) for more details). The second category contains works that are much more oriented towards the design of compilation algorithms, and their empirical evalua­ tions (see e.g. [Reiter and de Kleer, 1987; Schrag, 1996; Boufkhad et al., 1997; Boufkhad, 1998)).

The compilability of CWR has been analyzed in depth in [Cadoli et al., 1996; 1997b). The results are typically negative. In a nutshell, inference under ECWA from a fixed KB is shown (probably) not compilable. Con­ trastingly, it is shown that CWA CLAUSE INFERENCE

and CCWA CLAUSE INFERENCE from Horn CNF, re­ verse Horn CNF or Krom formulas are compilable (the fixed part of the problem is the KB plus the partition in the CCWA case) .

From the practical side, Nerode, Ng and Subrah­ manian [1995) present an algorithm for compiling a KB interpreted under circumscription into the set of its minimal models. The algorithm is based on a mixed integer linear programming. The circumscrip­ tion policy (i.e., the partition of the symbols) is fixed. Several other approaches show how CWR can be re­ duced to deduction through the computation of the closure of the KB (or the computation of any equiv­ alent formula), see e.g. [Raiman and de Kleer, 1992; Castell et al., 1996). All these approaches confirm the (probable) non compilability of the most sophisticated forms of CWR in the sense that in the worst case, the compilation phase outputs a formula that is not polyno­ mially bounded in the size of the original KB.

4 Complexity Results

In the following, the complexity of CWR is investigated for some KBs for which CLAUSE DEDUCTION is tractable (tractable KBs for short):

Definition 4.1 (some tractable classes)

Let~ be a formula from PROPps.

• ~ is a Blake formula iff ~ is a CNF formula and for every implicate 1 of ~' there exists a clause 1r in~ s.t. 1r f= 1 holds.
• ~ is a DNF formula iff~ is a (finite) disjunction of terms.
• ~ is a Horn cover formula iff~ is a (finite) disjunc­ tion of Horn CNF formulas.
• ~ is a renamable Horn cover formula iff ~ is a (fi­ nite) disjunction of renamable Horn CNF formulas.

Blake formulas [Blake, 1937) are CNF form~las given by their prime implicates. Clearly enough, they are tractable since for every clause 1, ~ f= 1 holds iff there exists 1r in ~ s.t. 1r f= 1 holds and this test can be easily achieved in time polynomial in l1rl +hi· Indeed, many algorithms for computing prime implicates have been proposed so far (see [Marquis, 1999) for a survey).

DNF formulas are tractable since for every clause 1, ~ f= 1 holds iff for every term 8 in ~' 8 f= 1 holds and this test can be easily achieved in time polynomial in 181 +Ill· Several algorithms for turning a formula into DNF can be found in the literature, e.g. [Schrag, 1996).

Horn (resp. renamable Horn) cover formulas are tractable since for every clause 1, ~ f= 1 holds iff for every <I> in ~' <I> f= 1 holds and this test can be eas­ ily achieved in time polynomial in I<I>I + hi when <I> is a Horn CNF formula [Dowling and Gallier, 1984) (resp. a renamable Horn CNF formula [Lewis, 1978)). Note that Horn CNF formulas and renamable Horn CNF formulas can be recognized (and checked for sat­ isfiability) in polynomial time. Note also that every term is a Horn CNF formula, every Horn CNF for­ mula and every satisfiable Krom formula is a renam­ able Horn CNF formula, and every term (resp. Horn CNF formula, renamable Horn CNF formula) is a DNF formula (resp. a Horn cover formula, a renamable Horn cover formula). Hence every DNF formula is a Horn cover formula and every Horn cover formula is a renamable Horn cover formula. Algorithms for computing Horn cover formulas and renamable Horn cover formulas can be found in [Boufkhad et al., 1997; Boufkhad, 1998].

The next proposition is the central result of this paper:

Proposition 4.1 (complexity of CWR)

The complexity of *CW A CLAUSE INFERENCE and *CW A LITERAL INFERENCE from a Blake formula, a DNF formula, a Horn cover formula and a renamable Horn cover formula is reported in Tables 1 and f22.

Intuitively, the fact that CWR typically is at the sec­ ond level of PH can be explained by the presence of two independent sources of complexity. One of them lies in deduction and the other one in model minimization. As Proposition 4.1 illustrates it, focusing on tractable KBs enables ruling out one source of difficulty in the general case, and both sources in some specific cases.

This work can be related to several studies in which the complexity of non monotonic inference from tractable fragments of propositional logic is analyzed, for instance [Kautz and Selman, 1991; Cadoli and Lenz­ erini, 1994; Ben-Eliyahu and Dechter, 1996]. Cadoli and Lenzerini [1994] investigate the complexity of CWR from Horn CNF, reverse Horn CNF and Krom formulas. In­ terestingly, the tractable classes for CWR we consider are strictly more expressive than some of the most ex­ pressive tractable classes pointed out up to now. Espe­ cially, they include some of the tractable classes given in [Cadoli and Lenzerini, 1994] as subcases. Thus, every Krom formula can be turned into its prime implicates normal form in polynomial time (just because a set of binary clauses has a polynomially bounded number of resolvents). Additionally, every Horn CNF formula be­ longs to the Horn cover class. However, the converse does not hold: the fragments studied here are strictly more expressive that those given in [Cadoli and Lenz­ erini, 1994]. For instance, every monotonic CNF formula (i.e., a CNF formula in which every symbol occurs only positively or negatively) can be put into prime implicates normal form in polynomial time but is not equivalent to a Horn CNF or a Krom formula in the general case.

Another significant difference w.r.t. [Cadoli and Lenz­ erini, 1994] is that our study is directly related to exact knowledge compilation in the sense that the fragments of propositional logic we consider are target classes for exact compilation functions. Thus, every propositional formula can be turned into a Blake formula, a DNF for­ mula, a Horn cover formula and a renamable Horn cover formula without modifying the set of its models. This contrasts with the fragments considered in [ Cadoli and Lenzerini, 1994] since some formulas cannot be repre­ sented either as a Horn CNF, a reverse Horn CNF or a Krom formula while preserving logical equivalence.

2 Some tractability results reported in the two tables can be generalized to any tractable KB. To be more precise, CWA CLAUSE INFERENCE and both CCWA CLAUSE INFERENCE and ECWA CLAUSE INFERENCE under the restriction P = 0 are in P whenever~ belongs to a class for which CLAUSE DEDUCTION is tractable.

Accordingly, the tractability results given in Proposi­ tion 4.1 can be exploited to draw some new conclusions about the usefulness of knowledge compilation for CWR. From the theoretical side, the compilability results for CWR given in [Cadoli et al., 1996] can be completed at the light of our results. Indeed, every polynomially solvable problem is compilable, even if its fixed part is empty since the compilation phase can be achieved in polynomial time. More interestingly, from the prac­ tical side, the connection with knowledge compilation suggests a two step process for computing CWR: the KB is first made tractable through knowledge compila­ tion, then CWR is achieved from the compiled KB. The first step is performed off-line and done once at all (un­ less the KB is modified). Using such an approach, the closed world assumption policy adopted can vary with the queries that are considered; for instance, the set of symbols to be minimized can change with time, with­ out requiring the KB to be re-compiled each time such a modification occurs. This flexibility is particularly inter­ esting when the KB, representing "hard"constraints, is shared by several agents, and different agents may have different preferences, encoded as a CWA policy. Each time an agent asks the KB, the corresponding prefer­ ences can be taken into account without requiring any re-compilation of the KB.

At the light of the complexity results given in Propo­ sition 4.1, our claim is that some approaches to knowl­ edge compilation can prove helpful in practice for some forms of CWR, provided that the compiled KB remains "small enough". For instance, compiling a KB into a Horn cover formula so as to interpret it under EGCWA reduces the complexity of inference from II~-complete to P. Thus, if the compilation phase does not result in an exponential blow up in the size of the KB, the time needed for inference from the compiled KB can be much lower than the corresponding time from the original KB; subsequently, the compilation time can be balanced. Let us stress that our claim concerns some specific cases only, not the general one: since CWR is (probably) not compi­ lable [Cadoli et al., 1996; 1997b], knowledge compilation cannot be expected as valuable for improving CWR in the general case. Nevertheless, it is worth noting that, while compilability results for CWR are mainly negative, they do not prevent from exhibiting some instances for which knowledge compilation proves helpful. Accord­ ingly, many experiments with various compilation func­ tions show the practical utility of such an approach for improving CLAUSE DEDUCTION (see e.g., [Schrag, 1996; Boufkhad et al., 1997]), though the problem is known as

(probably) not compilable. Our results show that, in the many situations in which some compilation techniques are computationally profitable for CLAUSE DEDUCTION, they can be profitable as well for some forms of CWR, with only a polynomial extra cost.

5 Conclusion

In this paper, the complexity of CWR has been investi­ gated for some tractable fragments of propositional logic. Several new tractable cases have been identified, and some new intractability results have been provided as well. Interestingly, the tractable fragments we have fo­ cused on are target classes for some compilation func­ tions; such a connection with exact knowledge compila­ tion can prove valuable from a computational point of view in the situations in which the size of the compiled KB remains "small enough".

Due to close connections between CWR and abduction and between CWR and some simple forms of default reasoning, complexity results for these additional forms of non monotonic inference from tractable KBs can be derived from the results presented in this paper. This is an issue for further research.

Acknowledgements

This work has been supported by the Ganymede II project of the "Contrat de plan Etat/Region Nord Pas­ de-Calais" .