Theoretical Computer Science 114, (1993), 231–245. Addendum in 118, (1993), 115.

Propositional Circumscription and Extended Closed World Reasoning are Π_{2}^{P}-complete

Thomas Eiter and Georg Gottlob

Christian Doppler Labor für Expertensysteme Institut für Informationssysteme^{∗} Technische Universität Wien, Austria

revised Technical Report CD-TR 91/20

Abstract

Circumscription and the closed world assumption with its variants are well-known nonmonotonic techniques for reasoning with incomplete knowledge. Their complexity in the propositional case has been studied in detail for fragments of propositional logic. One open problem is whether the deduction problem for arbitrary propositional theories under the extended closed world assumption or under circumscription is Π_{2}^{P} -complete, i.e., complete for a class of the second level of the polynomial hierarchy. We answer this question by proving these problems Π_{2}^{P} -complete, and we show how this result applies to other variants of closed world reasoning.

1 Introduction

The nonmonotonic inference techniques of closed world reasoning are widely used in Artificial Intelligence, Database Theory, and Logic Programming [2]. Starting with the (naive) Closed World Assumption (CWA) introduced by Reiter [26], several formalizations of closed world reasoning have been developed. In this paper, besides the CWA, we consider the following well-known approaches to closed world reasoning: the Generalized Closed World Assumption (GCWA) by Minker [23], the Extended Generalized Closed World Assumption (EGCWA) by Yahya and Henschen [35], the Careful Closed World Assumption (CCWA) by Gelfond and Przymusinska [13], and the Extended Closed World Assumption (ECWA) by Gelfond, Przymusinska, and Przymusinski [12]. Circumscription was introduced by McCarthy in [22]. It is known that circumscription as defined in [36] coincides with the ECWA in the case of propositional logic [12].

∗Mailing address: TU Wien, Paniglgasse 16, A-1040 Wien, Austria.

Internet e-mail: {eiter,gottlob}@vexpert.dbai.tuwien.ac.at

While much work has been devoted to the study of the logical properties of such forms of closed world reasoning and of their applicability in different contexts, the interest in a complexity analysis of these methods has emerged only more recently [2, 20, 21, 29]. Papalaskari and Weinstein [37] show that inference from infinite propositional theories under minimal consequence (i.e. circumscription) is Π_{2}^{0} and not Σ_{2}^{0}. For the first order case, it was shown that a number of closed world inference rules have degrees of unsolvability at different levels of the arithmetical hierarchy. In particular, Apt and Blair [3] show that the CWA is complete for Π_{1}^{0}; Chomicki and Subrahmanian [9] show that GCWA is Π_{2}^{0}-complete; and Schlipf has proven that relevant problems related to circumscription are Σ_{2}^{1}-complete and Π_{2}^{1}-complete [28]. Other complexity results concerning model checking are provided by Kolaitis and Papadimitriou in [18].

Cadoli and Lenzerini present in [6, 5] a very careful analysis of the computational complexity of the above-mentioned forms of closed world reasoning for various fragments of propositional logic. They mainly consider syntactically restricted classes of formulas, such as Horn clauses, dual-Horn formulae, Krom formulae, and various combinations of these classes. Their work accurately elucidates the boundary between tractability and intractability for different forms of closed world reasoning. Other important studies where such restrictions are considered were carried out by Apt [2] and by Lenzerini [20, 21]; for an overview see [5].

Little has been shown concerning the computational complexity arising from the application of closed world inference rules to general propositional clauses or formulae. Cadoli and Lenzerini note that it follows from results in [29] that performing deduction under the CCWA or ECWA is both NP-hard and co-NP-hard [5]. They also observe that the deduction problem under the ECWA is in the class Π_{2}^{P} of the polynomial hierarchy. The question whether deduction under ECWA is complete for Π_{2}^{P} is pointed out as an open problem.

In the present paper we deal with the complexity of closed world reasoning applied to general propositional theories and to unrestricted clause-sets. In particular, we study the deduction problem, i.e., given formulae F and G, does G follow from F under a certain closedworld inference rule. We show by a surprisingly short proof that the deduction problems under the GCWA, the EGCWA, the CCWA, the ECWA are all Π_{2}^{P} -hard. In particular, we show that the deduction problem under both the EGCWA and under the ECWA is Π_{2}^{P} - complete, thus solving the problem posed by Cadoli and Lenzerini. We show that this holds also under the restriction that F is in clause form with at most three literals per clause and G is a literal. This is proved to be a limit case for Π_{2}^{P} -completeness, since if F has at most 2 literals per clause, the deduction problem is co-NP-complete for both EGCWA and ECWA.

For the GCWA and the CCWA we provide upper bounds by showing that the inference problem can be solved with O(log m) calls to a Σ_{2}^{P} -oracle, where m is the number of propositional variables in the formula F. We also show that testing whether the closure under CWA of a formula F is consistent (a co-NP-hard problem) can be done with O(log m) calls to an NP-oracle, where m is the number of propositional variables in F, thus providing a new upper bound for this problem.

Our results can be interpreted as follows: If the polynomial hierarchy does not collapse, then, for all closed world reasoning principles that we consider (except for the simple CWA), the deduction problem is strictly harder than the deduction problem in classical propositional logic. In particular, depending on the chosen closed world principle, the deduction problem is either complete for Π_{2}^{P} or only “mildly” harder than Π_{2}^{P}. The deduction problem under the CWA, on the other hand, is in Δ_{2}^{P}, and most probably not complete for this class. Thus deduction with the CWA is not much harder than the deduction problem in the classical propositional logic. It is harder, however, since we show that this problem is neither in NP nor in co-NP unless the polynomial hierarchy collapses.

2 Preliminaries and Previous Results

A theory T is, unless stated otherwise, a finite set of propositional formulae. As usual, we identify T with the conjunction of all its formulae. Closed world reasoning attaches each theory T a set of formulae that are assumed to be false in lack of deducibility. Which formulae are added to T depends on the closed world reasoning rule (CWR-rule) obeyed. The union of T and the conjoined formulae is called the closure of T with respect to the applied CWR-rule.

We consider all the major CWR-rules proposed in the literature and follow the notation in [5]. The more sophisticated CWR-rules require to partition the variables into three sets, usually denoted by P, Q, and Z. The set P contains the variables to be minimized, Z are those variables that can vary in minimizing P, and Q are all other variables. For every set R of variables, the sets R^{+} and R^{−} denote the positive and negative literals corresponding to R, i.e., the formulae R^{+} = {x | x ∈ R} and R^{−} = {¬x | x ∈ R}, respectively. A clause is a disjunction of literals. A clause is positive iff it has no negative literals. A formula is in conjunctive normal form (CNF) is it is a conjunction of clauses. A formula in CNF is in kCNF if each clause contains at most k literals, and it is in kXCNF if each clause contains exactly k distinct literals.

Cadoli and Lenzerini characterize the CWR-rules abstractly as follows.

Definition 2.1 ([5]) Let T be a propositional formula, <P; Q; Z> a partition of the variables in T, and let C be a CWR-rule. The closure of T with respect to C is

C(T; P; Q; Z) = T ∪ {¬K | K is free for negation in T with respect to C}.

A formula K is called C-ffn if it is free for negation in T with respect to the CWR-rule C (given <P; Q; Z>).

The CWR-rules differ in the formulae that are free for negation as follows. Formula K is free for negation if and only if

CWA (Closed World Assumption [26]): K is a positive literal and T |̸= K.

GCWA (Generalized CWA [23]): K is a positive literal and for every positive clause B with T |̸= B, it holds that T |̸= B ∨ K.

EGWCA (Extended GCWA [35]): K is a conjunction of positive literals and for every positive clause B with T |̸= B, it holds that T |̸= B ∨ K.

CCWA (Careful CWA [13]): K is a positive literal from P and for each clause B whose literals belong to P^{+} ∪ Q^{+} ∪ Q^{−} such that T |̸= B, it holds that T |̸= B ∨ K.

ECWA (Extended CWA [12]) K is an arbitrary formula not involving literals from Z and for each clause B whose literals belong to P^{+} ∪ Q^{+} ∪ Q^{−} such that T |̸= B, it holds that T |̸= B ∨ K.

Since CWA, GCWA, and EGCWA are independent of <P; Q; Z>, we write CWA(T) for CWA(T; P; Q; Z) etc.

The closure of T under naive CWA may be inconsistent though T is consistent. The other CWR-rules, however, preserve consistency. Note that GCWA is a restricted version of EGCWA as well as CCWA, and both EGCWA and CCWA are restrictions of ECWA. Recently, a weakened form of GCWA has been introduced [25] for syntactically restricted theories, called disjunctive database rule in [27]; this CWR-rule has a polynomial-time algorithm for deduction [5].

An alternative characterization of the CWR-rules is possible in terms of minimal Herbrand models. Recall that in the propositional case, a Herbrand model is the set of propositional variables that are true in a truth value assignment. We write M ⊧ F if the formula F is satisfied by the model M. Let M(T) denote the set of all models of theory T. The relation ≤ on M(T) is defined by M ≤ M′ iff M ⊆ M′, i.e., all variables true in M are also true in M′. Clearly, ≤ is a partial order. For a partition <P; Q; Z>, the relation ≤_{P;Z} is defined on M(T) by M ≤_{P;Z} M′ iff M ∩ Q = M′ ∩ Q and M ∩ P ⊆ M′ ∩ P. Relation ≤_{P;Z} is a pre-order; note that ≤_{P;Z} coincides with ≤ for Q = Z = ∅. Model M ∈ M(T) is minimal if no M′ ∈ M(T) satisfies M′ ≤ M and M ≰ M′, and M is called <P; Z>-minimal if no M′ ∈ M(T) satisfies M′ ≤_{P;Z} M and M ≰_{P;Z} M′. The minimal models of T are denoted by MM(T) and the <P; Z>-minimal models by MM(T; P; Z).

Now a formula K is free for negation iff the following property is satisfied (cf.[5]):

CWA: K is a positive literal and there is some M ∈ M(T) such that M |̸= K.

GCWA: K is a positive literal and for each M ∈ MM(T), M |̸= K.

EGCWA: K is a conjunction of positive literals and for each M ∈ MM(T), M |̸= K.

CCWA: K is a positive literal from P and for each M ∈ MM(T; P; Z), M |̸= K.

ECWA: K is an arbitrary formula not involving literals from Z and for each M ∈ MM(T; P; Z), M |̸= K.

Note that CWA, GCWA, and CCWA only add literals to T. Thus the closure of T with respect to each of these CWR-rules can be written down in space linear in the size of T if only the variables of T are considered. For the other CWR-rules, EGCWA and ECWA, exponential space is required in the worst case.

We refer to the standard notation in complexity theory [10, 15]. Recall that P^{A} (NP^{A}) corresponds to the class of decision problems that are solved by deterministic (nondeterministic) Turing machines with an oracle for A in polynomial time. Problem B is polynomial-time Turing reducible to problem A (B ≤_{T}^{P} A) iff B ∈ P^{A}. The classes Σ_{k}^{P}, Π_{k}^{P}, and Δ_{k}^{P} of the polynomial hierarchy are defined by Σ_{0}^{P} = Π_{0}^{P} = Δ_{0}^{P} = P, and for k ≥ 0, Σ_{k+1}^{P} = NP^{Σ_{k}^{P}}, Π_{k+1}^{P} = co-Σ_{k+1}^{P}, and Δ_{k+1}^{P} = P^{Σ_{k}^{P}}. In particular, Σ_{2}^{P} = NP^{NP} and Π_{2}^{P} = co-NP^{NP}. The class of decision problems that are polynomially solvable with no more than f(n) calls to an Σ_{k}^{P} oracle is denoted by P^{Σ_{k}^{P} [f(n)]}, where f(n) is a function in the size n of the problem instance.

To generalize the concept of NP-completeness, in [10] the notions NP-easy, NP-hard and NP-equivalent are introduced for search problems (Turing-computable functions). In this spirit, we say that a search problem is Σ_{k}^{P} -equivalent, if it is Σ_{k}^{P} -easy and Σ_{k}^{P} -hard, where k ≥ 1. A search problem A is Σ_{k}^{P} -hard (k ≥ 1) if B ≤_{T}^{p} A for every problem B ∈ Σ_{k}^{P}, and A is Σ_{k}^{P} -easy if A ≤_{T}^{p} B for some B ∈ Σ_{k}^{P} (Note that for decision problems polynomial-time transformability (many-one reducibility ≤_{m}^{p}) is the standard notion of hardness).

The complexity of computing the CWA closure is an easy corollary to the following proposition, which follows from a result in [29].

Proposition 2.1 Deciding if variable x is CWA-ffn in T is NP-complete.

Corollary 2.2 Computing the closure of a propositional theory T with CWA is NP-equivalent.

The next proposition is well-known, cf. [5].

Proposition 2.3 For any formula F, EGCWA(T) ⊧ F iff for all M ∈ MM(T), M ⊧ F, and ECWA(T; P; Q; Z) ⊧ F iff for all M ∈ MM(T; P; Z), M ⊧ F.

An extensive study of the complexity of closed world reasoning for the propositional case is presented by Cadoli and Lenzerini in [5, 6]. Their work covers important propositional theories for which the deduction problem is tractable, among them Horn and Krom theories.

They point out that the analysis of Schlipf in [29] entails that propositional deduction with CCWA is NP-hard as well as co-NP-hard, and they also show that closed world reasoning with the ECWA-rule for arbitrary propositional theories is in Π_{2}^{P}. It is posed as an open problem in [5] whether this problem is Π_{2}^{P} -complete.

One of the most powerful CWR-rules is circumscription, which was introduced by Mc-Carthy [22] for first-order theories. Informally, the circumscription CIRC(T; P; Z) of a list of predicates P in a first-order theory T states that the predicates in P have minimal extension in T if the predicates in list Z are free to vary for minimization [36].

In the propositional case, P = {p_{1}, …, p_{n}} and Z = {z_{1}, …, z_{m}} are sets of propositional variables, and the circumscription of theory T = T (P; Q; Z) (Q are the variables of T not in P ∪ Z) is

CIRC(T; P; Z) = T (P; Q; Z) ∧ [ ∀P′, Z′( T (P′; Q; Z′) ∧ (P′ ⇒ P)) ⇒ (P ⇒ P′) ]

where P′ = {p′_{1}, …, p′_{n}}, Z′ = {z′_{1}, …, z′_{m}} are disjoint sets of propositional variables, T (P′; Q; Z′) denotes the theory obtained from T (P; Q; Z) by replacing the variables p_{i}, z_{j} with p′_{i}, z′_{j}, for 1 ≤ i ≤ n, 1 ≤ j ≤ m, ∀P′, Z′ stands for ∀p′_{1} … ∀p′_{n}∀z′_{1} ⋯ ∀z′_{m}, and P′ ⇒ P, P ⇒ P′ stand for ⋀_{1≤i≤n}(p′_{i} ⇒ p_{i}) and ⋀_{1≤i≤n}(p_{i} ⇒ p′_{i}), respectively.

A closer look at circumscription yields the following relation (cf. [12], Theorem 5.1):

Proposition 2.4 Circumscription and the ECWA-rule are equivalent for propositional theories.

3 Complexity Results

The deduction problem for CWR-rule C is as follows: Given a theory T and a formula F, does C(T; P; Q; Z) ⊧ F hold, where T,P, Q, Z, and F is part of the input ?

Cadoli and Lenzerini conjecture that this problem is Π_{2}^{P} -complete for ECWA. We show that this is true even if T is in 3XCNF and F is a literal. Moreover, the deduction problem is (even for a single literal) Π_{2}^{P} -hard for GCWA, EGCWA, and CCWA. This result on the complexity of literal deduction entails that computing the closure of a theory under GCWA and CCWA is at least as hard as the deduction problem.

The key lemma in our proof is the following.

Lemma 3.1 Let T be a propositional theory and let x be a propositional variable. It is Π_{2}^{P} - hard to decide if for every M ∈ MM(T), M ⊧ ¬x. This holds even if T is in 3CNF or in 3XCNF.

Proof: We proceed as follows. First, we give a ≤_{m}^{p} transformation of the generic Π_{2}^{P} - complete problem into this problem where the constructed theory is not in 3CNF, and then we show how to transform the constructed theory into an equivalent theory in 3XCNF form.

The “generic” Π_{2}^{P} -complete problem is to decide if a quantified Boolean formula of the form

F = ∀x_{1} ⋯ ∀x_{n}∃y_{1} ⋯ ∃y_{m}E(x_{1}, … x_{n}, y_{1}, …, y_{m}),

where E(x_{1}, …, x_{n}, y_{1}, …, y_{m}) is a Boolean expression in variables x_{1}, …, x_{n}, y_{1}, …, y_{m}, is true [30].

The transformation is as follows. Let z_{1}, …, z_{n} and u be new variables. We define the following theory T:

T = [ ⋀_{1≤i≤n}(x_{i} ≢ z_{i}) ] ∧ [ (u ∧ y_{1} ∧ y_{2} ∧ ⋯ ∧ y_{m}) ∨ E(x_{1}, …, x_{n}, y_{1}, …, y_{m}) ]

We claim that F is true if and only if for every M ∈ MM(T), M ⊧ ¬u.

First, note that T is consistent and that for T′ = ⋀_{1≤i≤n}(x_{i} ≢ z_{i}), every M ∈ M(T′) is extendible to a model of T assigning true to u, y_{1}, …, y_{m} and false to all other variables; denote this model by E_{0}(M). It is easy to see that E_{0}(M) is a maximal element in M(T) under ≤. Moreover, arbitrary extensions of models M, M′ ∈ M(T′), M ≠ M′, to models of T are always incomparable under ≤. Since only extensions of models of T′ are models of T, it follows that every model M ∈ M(T′) is extendible to some minimal model M′ ∈ MM(T).

“⇒”: Let F be true and assume that there exists M ∈ MM(T) such that u ∈ M. Then M |̸= E, for otherwise M − {u} ∈ M(T) which contradicts the minimality of M. Therefore, M ⊧ u ∧ y_{1} ∧ ⋯ ∧ y_{m} holds, that is, M = E_{0}(M_{xz}), where M_{xz} = M ∩ {x_{1}, z_{1}, …, x_{n}, z_{n}}. By the minimality of M, there exists no extension M′ of M_{xz} such that M′ ≠ M and M′ ∈ M(T); any such M′ would satisfy M′ ≤ M, M ≰ M′. Consequently, F is not true, a contradiction.

“⇐”: If for each M ∈ MM(T) it holds that M ⊧ ¬u, we have that for all M′ ∈ M(T′), E_{0}(M′) ∉ MM(T). We conclude that for each model M′ ∈ M(T′) there exists an extension E_{1}(M′) ≠ E_{0}(M′) to T with E_{1}(M′) ≤ E_{0}(M′). Note that u ∉ E_{1}(M′) and that E_{1}(M′) satisfies E. Since M(T′) corresponds one by one to all truth assignments to x_{1}, …, x_{n}, it follows that F is true.

Since T is clearly computable in polynomial time from F, the first part of the lemma is proved. For the second part of the lemma, it suffices to show that the claim holds if T is in 3XCNF.

By the results in [30] the formula F remains Π_{2}^{P} -complete even if E is in 3XCNF. Thus we assume that E = C_{1} ∧ C_{2} ∧ ⋯ ∧ C_{k}, where each clause C_{i} contains three literals. By simple algebraic manipulations T can be transformed into the logically equivalent theory T_{1} = T_{xz} ∧ T_{uy}, where

T_{xz} = ⋀_{1≤i≤n}[(x_{i} ∨ z_{i}) ∧ (¬x_{i} ∨ ¬z_{i})], T_{uy} = [ ⋀_{1≤i≤k}(u ∨ C_{i})] ∧ [ ⋀_{1≤i≤k} ⋀_{1≤j≤m} (y_{j} ∨ C_{i})].

Note that T_{xz} is in 2CNF, T_{uy} is in 4CNF, and that each clause of T_{uy} has at least three distinct literals. Let T_{uy} = C′_{1}, …, C′_{l}, C′_{l+1}, …, C′_{l+p} where C′_{l+1}, …, C′_{l+p} are the clauses with a double occurence of a literal. Let T′_{uy} be the formula obtained from T_{uy} as follows. All double literal occurences are removed, and each clause C′_{i} for 1 ≤ i ≤ l, is split into two clauses C′_{i,1}, C′_{i,2} in the following way (cf. [10, p.48]). Let U = {u, y_{1}, …, y_{m}}, and let r_{1}, …, r_{l} be new variables. For clause C′_{i} = l_{i,1} ∨ l_{i,2} ∨ l_{i,3} ∨ l_{i,4}, 1 ≤ i ≤ l, define C′_{i,1} = l_{i,1} ∨ l_{i,2} ∨ ¬r_{i} and C′_{i,2} = r_{i} ∨ l_{i,3} ∨ l_{i,4}. Note that l_{i,1} ∈ U, thus C′_{i,1} ∧ C′_{i,2} is satisfied if l_{i,1}, r_{i} are true.

Now define a formula G = (¬u ∨ y_{1}) ∧ … ∧ (¬u ∨ y_{m}) ∧ (¬u ∨ r_{1}) ∧ … ∧ (¬u ∨ r_{l}) and a theory T_{2} by T_{2} = T_{xz} ∧ T′_{uy} ∧ G.

It is straightforward to verify that for each M ∈ M(T′), the set E′_{0}(M) = M∪{u, y_{1}, …, y_{n}, r_{1}, …, r_{l}} is a model of T_{2}. Clearly, E′_{0}(M) is maximal under ≤, and G assures that E′_{0}(M) is the only possible extension of M to a model of T_{2} in which u is true.

On the other hand, it is not difficult to see that each M ∈ M(T′) is extendible to a model of T_{2} in which u is false iff M is extendible to a model of T_{1} in which u is false. For if M ∈ M(T′) extends to M_{1} ∈ M(T_{1}) such that u ∉ M_{1}, then M_{1} is a model of T_{xz} ∧ G, and for 1 ≤ i ≤ l, at least one of C′_{i,1}, C′_{i,2} is satisfied by M_{1} since M_{1} satisfies C′_{i}. Thus a proper truth assignment to r_{i} satisfies C′_{i,1} ∧ C′_{i,2}. Consequently, some M_{2} ⊇ M_{1} with u ∉ M_{2} is a model of T_{2}. Since M_{2} ⊇ M, the only if claim holds. Conversely, every model M of T_{2} restricted to the variables of T_{1} is a model of T_{1}; hence, M − {r_{1}, …, r_{l}} ∈ M(T_{1}). Thus if M_{2} ∈ M(T_{2}) such that M_{2} ⊇ M for M ∈ M(T′), then M_{1} = M_{2} − {r_{1}, …, r_{l}} ∈ M(T_{1}), where M_{1} ⊇ M. Hence also the if direction is true.

We conclude from this that there is some M_{2} ∈ MM(T_{2}) with M_{2} |̸= ¬u iff there is some M_{1} ∈ MM(T_{1}) with M_{1} |̸= ¬u iff there is some M ∈ MM(T) with M |̸= ¬u. Note that T_{2} = T_{xz} ∧ T′_{uy} ∧ G is in 3CNF, and T′_{uy} is already in 3XCNF, but T_{xz} and G are only in 2XCNF. Let T_{xz} ∧ G = C′′_{1}, …, C′′_{h}, and let s_{1}, …, s_{h} be new variables. Let H denote

H = [(C′′_{1} ∨ s_{1}) ∧ (¬s_{1} ∨ C′′_{1})] ∧ ⋯ ∧ [(C′′_{h} ∨ s_{h}) ∧ (¬s_{h} ∨ C′′_{h})],

and define a theory T_{3} as T_{3} = T′_{uy} ∧ H. Then, T_{3} is clearly in 3XCNF and as easily seen, each model of T_{3} induces a model of T_{2} and each M_{2} ∈ M(T_{2}) is extendible to some M_{3} ∈ M(T_{3}) by assigning the s_{i} any truth value; this entails that for all M ∈ M(T_{3}), then M − {s_{i}} ∈ M(T_{3}). Thus clearly there exists an M ∈ MM(T_{3}) with M |̸= ¬u iff there exists an M ∈ MM(T_{2}) with M |̸= ¬u iff there exists M ∈ MM(T) with M |̸= ¬u. Obviously, T_{2} and T_{3} can be constructed in polynomial time ¿from the formula F, thus the proof of the lemma is complete. □

We remark that Lemma 3.1 grasps the case of the “simplest” formula type for which the problem MM(T) ⊧ F is Π_{2}^{P} -hard. Indeed, if F is a single variable x, then MM(T) ⊧ F iff T ⊧ F, hence the problem is in co-NP.

Lemma 3.1 also marks a boundary of the complexity of deduction from the minimal models of a theory T that is in kCNF for constant k. Indeed, for k = 2 deduction is no longer Π_{2}^{P} -hard, even in case of <P; Z>-minimality, as the following lemma shows.

Lemma 3.2 Let T be a propositional theory in 2CNF, and let F be a propositional formula. To decide if for all M ∈ MM(T; P; Z) it holds that M ⊧ F is in co-NP.

Proof: To show that for some M ∈ MM(T; P; Z) it holds M |̸= F, make a guess for M and check that M ⊧ T and M |̸= F. Checking <P; Z>-minimality of M can be done in polynomial time as follows. Join to T for each variable x such that x ∉ (P ∪Z) or x ∈ P −M, the singleton clause x if x ∈ M and ¬x if x ∉ M. Let T′ denote the resulting theory. Then, M ∈ MM(T; P; Z) iff for all x ∈ P ∩M, the theory T_{x} = T′ ∧¬x is inconsistent. Note that T_{x} is in 2CNF; consistency checking for 2CNF theories is well-known as a polynomial problem [10]. □

3.1 ECWA, Circumscription, and EGCWA

Our main result is easily proved with Lemma 3.1.

Theorem 3.3 In the propositional case, the deduction problem C(T; P; Q; Z) ⊧ F ? is Π_{2}^{P} - complete for C = EGCWA, C = ECWA, and C = CIRC. This holds even if the theory T is in 3XCNF and F is a single literal.

Proof: By Proposition 2.4 circumscription and ECWA are equivalent, thus to consider ECWA suffices.

Membership of EGCWA and ECWA in Π_{2}^{P} is immediate from Proposition 2.3: To disprove ECWA(T; P; Q; Z) ⊧ F, guess a <P; Z>-minimal model M of T and check if F is false in M.^{1} Verification of the minimality of the guess can be done with a single NP oracle call: Join to T the clause ¬x_{1} ∨¬x_{2} ∨⋯∨¬x_{r}, where {x_{1}, …, x_{r}} = P ∩M, and for each variable x such that x ∈ P − M or x ∉ (P ∪ Z), join the clause x if x ∈ M and ¬x if x ∉ M. Let T′ be the theory obtained this way. Then, T′ is inconsistent if and only if M ∈ MM(T; P; Z). If M |̸= F, then a proof of ECWA(T; P; Q; Z)|̸= F is found. For EGCWA the same procedure applies with Q = Z = ∅. Π_{2}^{P} -hardness of the deduction problem with EGCWA and ECWA follows immediately from Lemma 3.1, thus the theorem is proved. □

Note that for 2CNF theories we have the following result.

Theorem 3.4 Let T be a propositional theory in 2CNF. Then the deduction problem C(T; P; Q; Z) ⊧ F? is co-NP-complete for C = EGCWA, C = ECWA, and C = CIRC.

1In [5] a proof of membership of ECWA in Π_{2}^{P} is already sketched.

Proof: Membership in co-NP is immediate from Proposition 2.3 and Lemma 3.2. co-NP-hardness of the deduction problem under EGCWA, under ECWA, and under circumscription for 2CNF theories is shown by Cadoli and Lenzerini in [5]. Thus the theorem follows. □

3.2 CWA

Since the “naive” CWA does not preserve consistency of T in general, checking the consistency of the closure with CWA is an additional – though not unrelated problem – to consider.

A semantical characterization of CWA in terms of minimal Herbrand models appears in [32], which states that CWA(T) is consistent iff the intersection of all Herbrand models of T is a model of T. Hence clearly,

Lemma 3.5 CWA(T) is consistent iff T has a unique minimal model M and CWA(T) is logically equivalent to M.

CWA consistency checking turns out to be the unique solution variant (cf. [14] for uniqueness questions) of the following problem MINSAT: Has T a minimal model ? Note that the latter is simply the NP-complete SATISFIABILITY (SAT) problem, since every consistent theory has a minimal model. The uniqueness variant UMINSAT is to decide if T has exactly one minimal model. Note that this problem is similar to the well-studied USAT problem, which asks if a Boolean expression E has a unique satisfying assignment [4]. Another similar problem is UOASAT, which asks if the truth assignment that satisfies the maximum number of a set of clauses is unique [16]. As for USAT and UOASAT, UMINSAT is easily proved co-NP-hard, but it is not clear how to reduce SAT to it. USAT is complete for the class D^{P} [24] under the randomized reduction ≤_{m}^{vv} of Valiant-Vazirani [31] and, as recently proved, USAT is not in co-D^{P}, which contains NP∪co-NP, unless the polynomial hierarchy collapses [8, 7].

We now show that UMINSAT, and thus CWA consistency checking, is at least as hard as USAT.

Lemma 3.6 USAT ≤_{m}^{p} UMINSAT.

Proof: Let E(x_{1} …, x_{n}) be a Boolean expression in variables x_{1}, …, x_{n}. Let y_{1}, …, y_{n} be new variables. Define a theory T by

T = E(x_{1}, …, x_{n}) ∧ (x_{1} ≢ y_{1}) ∧ ⋯ ∧ (x_{n} ≢ y_{n}).

It is easy to see that the truth assignments to x_{1}, …, x_{n} satisfying E correspond one to one with the models of T on variables x_{1}, y_{1} …, x_{n}, y_{n} and that all models of T are minimal. Thus E has a unique satisfying truth assignment iff T has a unique minimal model.

□ We thus have the following result.

Theorem 3.7 Consistency checking for propositional theories with CWA is co-NP-hard, and this problem is not in co-D^{P} unless the polynomial hierarchy collapses.

Proof: By Lemma 3.5 and Lemma 3.6. □

The deduction problem with CWA is close to the consistency checking problem. It is important to note that deciding if a variable x is CWA-ffn in theory T is different from deciding if CWA(T) ⊧ ¬x. The former problem is NP-complete, while the latter turns out to be more difficult. It is easy to show by conjoining a new variable z to theory T in the proof of Lemma 3.6 that CWA(T ∧ z) ⊧ ¬z iff CWA(T) is inconsistent iff T has not a unique minimal model. Thus co-USAT is ≤_{m}^{p} reducible to CWA(T) deduction, and we get the following result.

Theorem 3.8 The deduction problem for propositional theories with CWA is NP-hard, and this problem is not in D^{P} unless the polynomial hierarchy collapses.

Note that both CWA consistency checking and deduction can be done in polynomial time with O(m) calls to an NP oracle, where m is the number of distinct variables in T. This upper bound can be considerably improved as follows.

Theorem 3.9 Let m be the number of distinct variables in T. CWA consistency checking and CWA deduction can be done with O(log m) calls to an NP oracle, hence the problems are in P^{NP[O(log n)]}.

Proof: If T is consistent, first the size k of a model of minimal cardinality is computed with binary search, which takes O(log m) oracle calls. Then it is checked by another oracle call if there is a unique minimal model; this is true iff there are no models M ≠ M′ ∈ M(T) such that |M| = k and M ≰ M′. Recall that CWA(T) is consistent iff T has a unique minimal model. If CWA(T) is consistent, testing CWA(T) ⊧ F is possible with one additional oracle call asking if every model M ∈ M(T) of size k satisfies F. □

Since CWA consistency checking is in P^{NP[O(log n)]}, this problem is unlikely to be ≤_{m}^{p}- complete in Δ_{2}^{P}, although it is unknown if this would imply NP = co-NP, cf. [15]. It is tempting to assume that CWA consistency checking is ≤_{m}^{p}-complete for P^{NP[O(log n)]}. Since it seems difficult, however, to show how to solve SAT with it, we think this will be, as UOASAT, rather difficult to prove.

3.3 GCWA and CCWA

For GCWA and CCWA we get the following results.

Theorem 3.10 It is Π_{2}^{P} -complete to check if a variable is GCWA-ffn or CCWA-ffn in a propositional theory T, even if T is in 3XCNF.

Proof: Immediate from the model characterization of ffn and by Lemma 3.1. □

Corollary 3.11 In the propositional case, the deduction problem C(T; P; Q; Z) ⊧ F? is Π_{2}^{P} -hard for C = GCWA and C = CCWA, even if T is in 3XCNF and F is a single literal.

Corollary 3.12 The computation of the closure for a propositional theory with GCWA or CCWA is Σ_{2}^{P} -equivalent.

Proof: Polynomial time algorithms to compute the closures with an oracle for freeness for negation in T are straightforward, thus the problems are Σ_{2}^{P} -easy. By Lemma 3.1 it follows that the problems are Σ_{2}^{P} -hard under ≤_{T}^{p} reductions; thus the result follows. □

Note that for the deduction problem with GCWA and CCWA, Π_{2}^{P} -hardness is a lower bound. It is not clear, however, whether these problems are in Π_{2}^{P}. Both problems are clearly in P^{Σ_{2}^{P} [O(n)]}, since the problem is solved with one call to a SATISFIABILITY oracle once the closure of T is computed. This algorithm makes m + 1 calls to a Σ_{2}^{P} oracle, where m is the number of distinct variables in T.

We can improve this straightforward upper bound drastically to only O(log m) calls, as shown in the proof of the next theorem.

Theorem 3.13 Let m be the number of distinct variables in T. Deduction under GCWA or under CCWA can be done with O(log m) calls to a Σ_{2}^{P} oracle, hence these problems are in P^{Σ_{2}^{P} [O(log n)]}.

Proof: We outline a polynomial-time algorithm that makes only O(log m) calls to a Σ_{2}^{P} oracle for CCWA. Since GCWA is CCWA with Q = Z = ∅, we need no extra argument for GCWA.

The basic idea is to proceed in two steps. Given T and F, first the number of variables that are not CCWA-ffn in T is computed, which will take O(log m) oracle calls. Then one additional oracle call will suffice to check if CCWA(T; P; Q; Z) implies F.

Let V_{min} = ⋃_{M∈MM(T;P;Z)} M. Then V_{min} are the variables that are not CCWA-ffn in T; clearly, |V_{min}| ≤ m, where m is the number of different variables in T. We note that the following problem is in Σ_{2}^{P}: Does |V_{min}| ≥ k hold ? given T, <P; Q; Z>, and k for input. The answer to this question is, as easily seen, “yes” iff there exist M_{1}, …, M_{k} ∈ MM(T; P; Z) such that | ⋃_{1≤i≤k} M_{i}| ≥ k. On a guess for the M_{i}’s and polynomial time verification of the minimality of the guess with an NP oracle (this can be done for each M_{i} as described in the proof of Theorem 3.3), testing | ⋃_{1≤i≤k} M_{i}| ≥ k is easy; so, the problem |V_{min}| ≥ k ? is in Σ_{2}^{P}. This implies that |V_{min}| is computable under binary search with O(log m) calls to a Σ_{2}^{P} oracle.

Now let r = |V_{min}|. Disproving CCWA(T; P; Q; Z) ⊧ F reduces to determining whether there exists a structure S of the following form:

S =<{p_{1}, …, p_{r}}, {M_{1}, …, M_{r}}, M>

where p_{1}, …, p_{r} are pairwise distinct variables, M_{1}, …, M_{r} ∈ MM(T; P; Z) satisfying p_{i} ∈ M_{i} for 1 ≤ i ≤ r, and M ∈ M(T) such that M ⊆ {p_{1}, …, p_{r}} and M |̸= F.

It is clear that CCWA(T; P; Q; Z) |̸= F iff such an S exists. Indeed, for every such structure S, all variables except p_{1}, …, p_{r} are CCWA-ffn in T, thus M is truly a model of CCWA(T; P; Q; Z). Since M |̸= F holds, CCWA(T; P; Q; Z) does not entail F. On the other hand, it is easy to see that such a structure S must exist if CCWA(T; P; Q; Z) does not entail F.

The existence of such a structure S can be inquired by one call to a Σ_{2}^{P} oracle, as this problem is certainly in Σ_{2}^{P}: Upon guessing S, the guess can be verified with an NP oracle in polynomial time, as easily seen. (In fact, this goes through with only one oracle call to check simultaneously if M_{1}, …, M_{r} are in MM(T; P; Z).)

Altogether, deciding CCWA(T; P; Q; Z) ⊧ F is possible with O(log m) + 1 = O(log m) oracle calls; from this the claim follows immediately. □

This result suggests that the deduction problem under GCWA and under CCWA is not ≤_{m}^{p}-complete for Δ_{3}^{P}, since it seems rather unlikely that a problem in P^{Σ_{2}^{P} [O(log n)]} is ≤_{m}^{p}- complete for Δ_{3}^{P}, cf. [16, 34].

4 Conclusion

Our main results are summarized in Table 1.

Answering the question in [5], we have shown that the deduction problem with ECWA and with circumscription is Π_{2}^{P} -complete for propositional theories, even for theories in 3XCNF and a single literal. Moreover, we proved the same result for EGCWA, and we gave fairly close bounds for CWA, GCWA, and CCWA. It remains an issue for further research whether CWA deduction is ≤_{m}^{p}-complete in P^{NP[O(log n)]} and whether GCWA and CCWA are ≤_{m}^{p}-complete in P^{Σ_{2}^{P} [O(log n)]}.

Another question to investigate is a refined complexity classification of closure computation. Σ_{k}^{P} -equivalence does not precisely indicate “how much” Σ_{k}^{P} -completeness is in a

CWR-rule  lower bound  upper bound
CWA(T) ⊧ F  NP-hard  P^{NP[O(log n)]}

GCWA(T) ⊧ F  Π_{2}^{P}-hard  P^{Σ_{2}^{P} [O(log n)]}

EGCWA(T) ⊧ F
Π_{2}^{P}-complete
CCWA(T; P; Q; Z) ⊧ F  Π_{2}^{P}-hard  P^{Σ_{2}^{P} [O(log n)]}

ECWA(T; P; Q; Z) ⊧ F
⇔
CIRC(T; Q; P; Z) ⊧ F

Π_{2}^{P}-complete

Table 1: Complexity Results for Propositional Closed World Deduction

problem, cf. [19, 34]. This may be measured by the number of necessary calls to a Σ_{k}^{P} oracle [19, 17, 33]. Closure computation with O(n) oracle calls is straightforward for CWA, GCWA, and CCWA. For CWA, it is not difficult to show that closure computation is (under suitable polynomial transformability) equivalent to the following problem QUERY [11]: Given Boolean expressions E_{1}, …, E_{m}, compute b_{1}, …, b_{m} where b_{i} = 1 if E_{i} is satisfiable and b_{i} = 0 if E_{i} is unsatisfiable. This problem requires at most m oracle calls; by results in [1], sufficiency of fewer calls is unlikely. It is unknown, however, whether QUERY is complete for FP^{NP}, the functions computable in deterministic polynomial time with unrestricted NP oracle access. Similarly, computing the GCWA and the CCWA closure can be shown equivalent to QUERY generalized to ∃∀-quantified Boolean formulas, that is, determining the outcome of m independent calls to a Σ_{2}^{P} oracle, and hence has a complexity characterization analogous to QUERY. The exact complexity classification of closure computation under polynomial reductions is, in any way, interesting for identifying “harder” and “easier” NP-equivalent or Σ_{2}^{P} -equivalent problems.

Acknowledgement

The authors are grateful to the referees for suggesting improvements to the draft of this paper.

References

[1] A. Amir and W. Gasarch. Polynomial Terse Sets. Information and Computation, 77:37– 56, 1988.

[2] K. Apt. Introduction to Logical Programming. Technical report, University of Texas, Department of Computer Science, 1987.

[3] K. Apt and H. Blair. Arithmetic Classification of Perfect Models of Stratified Programs. In R. Kowalski and K. Bouwen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 766–779. MIT Press, 1988.

[4] A. Blass and Y. Gurevich. On the Unique Satisfiability Problem. Information and Control, 55:80–88, 1982.

[5] M. Cadoli and M. Lenzerini. The Complexity of Closed World Reasoning and Circumscription. In Proceedings AAAI-90, pages 550–555, 1990.

[6] M. Cadoli and M. Lenzerini. The Complexity of Closed World Reasoning and Circumscription. Technical Report RAP. 17.91, Universitá di Roma “La Sapienza”, Dipartimento di Informatica e Sistemistica, September 1991.

[7] R. Chang and J. Kadin. On the Structure of Uniquely Satisfiable Formulas. Technical Report 90-1124, Department of Computer Science, Cornell University, May 1990.

[8] R. Chang and P. Rohatgi. On Unique Satisfiability and Randomized Reductions. Bulletin of the EATCS, 47:151–159, 1990.

[9] J. Chomicki and V. S. Subrahmanian. Generalized Closed World Assumption is ∏_{2}^{0}- Complete. Information Processing Letters, 34:289–291, 1990.

[10] M. Garey and D. S. Johnson. Computers and Intractability – A Guide to the Theory of NP-Completeness. W. H. Freeman, New York, 1979.

[11] W. Gasarch. The Complexity of Optimization Functions. Technical Report 1652, Dept. of Computer Science, University of Maryland, 1986.

[12] M. Gelfond, H. Przymusinksa, and T. Przymusinski. On the Relationship Between Circumscription and Negation as Failure. Artificial Intelligence, 38:75–94, 1989.

[13] M. Gelfond and H. Przymusinska. Negation as Failure: Careful Closure Procedure. Artificial Intelligence, 30:273–287, 1986.

[14] D. S. Johnson. The NP-Completeness Column – An Ongoing Guide. Journal of Algorithms, 6(2):291–305, 1985. Column 15: Uniqueness.

[15] D. S. Johnson. A Catalog of Complexity Classes. volume A of Handbook of Theoretical Computer Science, chapter 2. Elsevier Science Publishers B.V. (North-Holland), 1990.

[16] J. Kadin. The Polynomial Time Hierarchy Collapses if the Boolean Hierarchy Collapses. SIAM J. Comp., 17(6):1262–1283, 1988.

[17] J. Kadin. P^{NP [O(log n)]} and Sparse Turing-Complete Sets for NP. Journal of Computer and System Sciences, 39:282–298, 1989.

[18] P. Kolaitis and C. Papadimitriou. Some Computational Aspects of Circumscription. Journal of the ACM, 37(1):1–15, 1990.

[19] M. Krentel. The Complexity of Optimization Problems. Journal of Computer and System Sciences, 36:490–509, 1988.

[20] M. Lenzerini. Covering and Disjointness Relationships in Hierarchy Networks. Technical Report RAP. 17.88, Universitá di Roma “La Sapienza”, Dipartimento di Informatica e Sistemistica, 1988.

[21] M. Lenzerini. Reasoning About Inheritance Networks. Technical Report RAP. 22.88, Universitá di Roma “La Sapienza”, Dipartimento di Informatica e Sistemistica, 1988.

[22] J. McCarthy. Circumscription – A Form of Non-Monotonic Reasoning. Artificial Intelligence, 13:27–39, 1980.

[23] J. Minker. On Indefinite Data Bases and the Closed World Assumption. In Proceedings of the 6^{th} Conference on Automated Deduction (CADE), pages 292–308, 1982.

[24] C. H. Papadimitriou and M. Yannakakis. The Complexity of Facets (And Some Facets of Complexity). Journal of Computer and System Sciences, 28:244–259, 1984.

[25] A. Rajasekar, J. Lobo, and J. Minker. Weak Generalized Closed World Assumption. Journal of Automated Reasoning, 5:293–307, 1989.

[26] R. Reiter. On Closed-World Databases. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 55–76. Plenum Press, New York, 1978.

[27] K. Ross and R. Topor. Inferring Negative Information From Disjunctive Databases. Journal of Automated Reasoning, 4(2):397–424, 1988.

[28] J. Schlipf. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic, 35:173–191, 1987.

[29] J. S. Schlipf. When is Closed World Reasoning Tractable ? In Z. Ras and L. Saitta, editors, Proceedings of the Third International Symposium on Methodologies for Intelligent Systems, pages 485–494, Turin, Italy, October 12-15 1988. Elsevier Science Publishers B.V. (North-Holland).

[30] L. Stockmeyer and A. Meyer. Word Problems Requiring Exponential Time. In Proceedings of the Fifth ACM Symposium on the Theory of Computing, pages 1–9, 1973.

[31] L. G. Valiant and V. V. Vazirani. NP is as easy as detecting unique solutions. Theoretical Computer Science, 47(1):85–93, 1986.

[32] M. H. van Emden and R. Kowalski. The Semantics of Logic as a Programming Language. Journal of the ACM, 3:733–742, 1976.

[33] K. Wagner. More Complicated Questions about Maxima and Minima, and Some Closures of NP. In Proceedings ICALP-86, pages 434–443, 1986. also Theoretical Computer Science, 51:53–80, 1987.

[34] K. Wagner. Bounded query classes. SIAM J. Comp., 19(5):833–846, 1990.

[35] A. Yahya and L. Henschen. Deduction in Non-Horn Databases. Journal of Automated Reasoning, 1(2):141–160, 1985.

[36] V. Lifschitz. Computing Circumscription. In Proceedings IJCAI-85, pages 121–127, 1985.

[37] M.-A. Papalaskari and S. Weinstein. Minimal Consequence in Sentential Logic. Journal of Logic Programming, 9:19–31, 1990.