Artificial Intelligence, 57(2-3):227–270, 1992.

On the Complexity of Propositional Knowledge Base Revision, Updates, and Counterfactuals^{∗}

Thomas Eiter and Georg Gottlob

Christian Doppler Laboratory for Expert Systems Information Systems Department^{†} Technical University of Vienna

Abstract

We study the complexity of several recently proposed methods for updating or revising propositional knowledge bases under the principle of minimal change. In particular, we derive complexity results for the following problem: given a knowledge base T, an update p, and a formula q, decide whether q is derivable from T ∘ p, the updated (or revised) knowledge base. Note that this problem includes the evaluation of the counterfactual p > q over T, that is a conditional statement “if p, then q” where p is known or expected to be false. We consider the general case where T is an arbitrary propositional formula (or theory) as well as restricted versions of this problem, in particular where T is a conjunction of Horn clauses, or where the size of the update p is bounded by a constant.

1 Introduction

In many areas of Artificial Intelligence, one has to deal with knowledge in flux, i.e. with knowledge bases that are subject to frequent updates or revisions in the light of new information [15, 58]. Different approaches for changing knowledge bases have been proposed recently by several researchers. All of these methods adhere to the principle of Minimality of Change which states that the knowledge base should change as little as possible if new information is incorporated.

In this paper we deal with the following methods of updating knowledge bases: Ginsberg’s approach [19], also considered by Fagin, Ullman, and Vardi [13], and by Nebel [44, 45], the WIDTIO approach [19, 21, 58], Dalal’s revision [7], the approach by Forbus [14], Borgida’s method [3], Winslett’s “Possible Models Approach” [57], Satoh’s method [53], and Weber’s approach [56].

∗An extended abstract of this paper appeared in the proceedings of the Eleventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, San Diego, CA, June 2-4, 1992.

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

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

Each of these methods is suited for particular application domains; most researchers agree that none of them can be considered as a general purpose means of changing knowledge bases. Moreover, it is now widely believed that there is no general purpose, domain independent means of updating knowledge bases that will “do the right thing” under all circumstances [58].

As pointed out by Katsuno and Mendelzon [30], as well as by various other authors [58, 45, 23], an important problem to explore is the computational complexity of the different approaches. Note that – though all methods are clearly intractable in the general case – for almost all of the cited methods a precise determination of the complexity was left as an open issue. Furthermore, it was not clear under which restrictions the single methods would become tractable.

In this paper we shed light on these complexity problems. In particular, we consider the following “implication problem”: given a knowledge base T, an update p, and a formula q, decide whether q is derivable from T ∘ p, the updated (or revised) knowledge base. For each of the different update or revision methods, we consider the general case where T is an arbitrary propositional formula as well as restricted versions of this problem where T is a conjunction of Horn clauses (or a set of Horn conjunctions), or where the size of the knowledge change p is bounded by a constant. The former restriction is an important special case to consider because many rule-based systems rely on Horn clauses, and the latter restriction is, according to Winslett [58, p.33], reasonable for consideration, since this assumption will certainly be met by human-generated updates. In each case (and for all combinations of cases) we are able to locate the complexity of this decision problem at the appropriate level of the polynomial hierarchy. In particular, we succeed in elucidating the tractability/intractability frontier for many approaches.

Note that the implication problem we consider exactly corresponds to evaluating a counterfactual according to the given revision or update semantics. Counterfactuals are conditional statements of the form “if p were true, then q would hold”, where p is assumed to be false in the actual world. According to the Ramsey Test [15], evaluating such a counterfactual in a given knowledge base T is equivalent to test whether q is a logical consequence of T ∘ p.

By our results it turns out that for all approaches (except for Dalal’s) the implication problem is at the second level of the polynomial hierarchy, thus harder than classical implication in propositional logic. In the Horn case, the complexity level of most approaches is lowered by one, but the problem remains intractable in each case. The same happens if the size of the knowledge change (formula p) is bounded by a constant. Tractability is obtained only if we consider both restrictions simultaneously.

Our results extend and complement very recent results by Nebel [45] and Winslett [58]. Nebel has shown that the implication problem under Ginsberg’s approach is Π_{2}^{P} -complete (thus at the second level of the polynomial hierarchy). His proof, however, does not carry over to most other approaches that we discuss. Nebel also shows that evaluating a counterfactual in Dalal’s setting is both NP-hard and co-NP-hard, but in Δ_{2}^{P}, hence solvable with a polynomial number of calls to an NP oracle (i.e. to a subroutine solving an NP-complete problem). We improve this result by showing that a logarithmic number of such oracle calls suffices for this task and that the problem is, moreover, also complete for the class P^{NP[O(log n)]}, which are the decision problems solvable in polynomial time by a logarithmic number of calls to an NP oracle.

Winslett [58] provides update algorithms for a number of approaches and derives from these algorithms bounds for computing the updated knowledge base T ∘ p from T and p. Note that this problem differs from the implication problem we consider. We will refer to Winslett’s results in Section 8. Winslett poses the following issue as an open problem [58, p.33]: Is it Σ_{2}^{P} -complete to decide if a change under the WIDTIO semantics removes a particular formula f from the knowledge base (the length of the update formula p is bounded by a constant) ? We show that the answer is yes, even under the restriction that f and p are literals (Section 8, discussion of Theorem 8.2).

The rest of this paper is organized as follows. In Section 2 we introduce some notation and introduce the relevant concepts of complexity theory. In Section 3 we report about basic rationality postulates for change operators, review the change operators under consideration, and relate change operators to counterfactuals. Section 4 presents an overview and a thorough discussion of our results. Complexity classes or bounds for each update operator under all possible restrictions are shown in a table. Note that we are able to determine the exact complexity of most change operators by a completeness result. In Section 5, we point out consequences of the complexity findings and consider related results. Sections 6-8 constitute the technical part of this paper, and state the complexity theorems and their proofs. The proofs are succinct; often one single transformation covers a number of different change semantics simultaneously. In particular, Section 6 contains the complexity analysis for the general case, while Sections 7 and 8 treat the Horn case and the case of bounded knowledge change, respectively. Section 9 concludes the paper.

2 Preliminaries

Throughout this paper, the language L of propositional logic with finite variable set V is considered. A knowledge base is a finite set of propositional formulae in L. Unless stated otherwise, T always denotes an arbitrary knowledge base, and p, q are a propositional formulae. As usual, we will identify T with the conjunction of its formulae. If S = {T_{1}, …, T_{n}} is a family of knowledge bases T_{1}, …, T_{n}, we identify S with the formula T_{1} ∨ ⋯ ∨ T_{n}.

V (T) denotes the variables of V that occur in T. Any truth value assignment to V is a model, which we identify with the set of variables that are assigned true by this assignment. Accordingly, set operations on models M, M′ (e.g., M − M′) refer to the respective sets of true variables of M, M′.

A model M is a model of a formula p iff p is satisfied by M (written M ⊧ p). The set of all models of p is denoted by Mod(p). As usual, we write p ⊧ q if satisfaction of p entails satisfaction of q, i.e. Mod(p) ⊆ Mod(q) holds. We say that p is valid in the knowledge base T iff T ⊧ p holds.

T is complete if for every formula p in L it holds that T ⊧ p or T ⊧ ¬p. Every x ∈ V is an atom, and T is called atomic if every formula in T is an atom. Any atom or negated atom is a literal, and T is a literal base if it contains only literals. A clause is a disjunction l_{1} ∨ ⋯ ∨ l_{n} of literals l_{i}.

Given a knowledge base T and a formula p, T ∘p denotes the change of T by incorporating p into the knowledge base applying the change operator ∘. The size, i.e. the length of a formula p is denoted by ∥p∥.

We assume that the reader is familiar with the basic concepts of the theory of NPcompleteness, as excellently presented in [16]. Many of the problems that we will discuss are most probably not in NP or co-NP, but reside in low levels of the polynomial hierarchy (PH). The PH is a hierarchy of complexity classes that account for computations that may query a certain oracle (rf. [16]). An oracle for a class of decision problems C enables to decide any problem in C in unit time; one can think of an oracle as a “subroutine without cost”. P^{C} (NP^{C}) are the decision problems solvable by some deterministic (nondeterministic) Turing machine in polynomial time with an oracle for the problems in C. The classes Δ_{k}^{P} , Σ_{k}^{P} , and Π_{k}^{P} of PH are defined as follows:

Δ_{0}^{P} = Σ_{0}^{P} = Π_{0}^{P} = P

and for all k ≥ 0,

Δ_{k+1}^{P} = P^{Σ_{k}^{P}} , Σ_{k+1}^{P} = NP^{Σ_{k}^{P}} , Π_{k+1}^{P} = co-Σ_{k+1}^{P}.

Note that NP = Σ_{1}^{P}, co-NP = Π_{1}^{P}, and Δ_{2}^{P} = P^{NP}. Moreover, Σ_{2}^{P} = NP^{NP} and Π_{2}^{P} = co-Σ_{2}^{P}. The classes co-NP and Π_{2}^{P} are of main interest in this paper. The “classical” co-NP-complete problem is to decide if a set of propositional clauses is not simultaneously satisfiable (UNSAT); the most prominent Π_{2}^{P} -complete problem is to decide validity of a formula from QBF_{2,∀}, the set of quantified Boolean formulas of the form ∀\underline{x}∃\underline{y}E(\underline{x}, \underline{y}), where \underline{x} =< x_{1}, …, x_{m} >, \underline{y} =< y_{1}, …, y_{n} > are tuples of propositional variables and E(\underline{x}, \underline{y}) is a propositional formula on \underline{x}, \underline{y}.^{1} We say that a problem is at the k-th level of the PH if it is in Δ_{k+1}^{P} and is Σ_{k}^{P} -hard or Π_{2}^{P} -hard (hence, complete for Δ_{k+1}^{P} under Turing reductions). According to this, UNSAT is at the first and QBF_{∀,2} at the second level of the PH.

More recently, P^{NP} has been refined to take into account how many NP oracle calls, i.e. subroutine calls to an NP-complete problem, are needed to solve a problem [46, 33, 27, 55]. This grasps in a certain sense “how much NP-hardness” is in a problem [33]. P^{NP[f(n)]} is the set of problems decidable in polynomial time with no more than f(n) calls to an NP oracle, where n is the input size [26]. For example, for any integer k the class P^{NP[k]} are those problems polynomially decidable with at most k NP oracle calls, and P^{NP[O(log n)]} is the class of problems polynomially decidable with at most O(log n) NP oracle calls. Classes with bounded number f(n) of calls to an arbitrary oracle may be defined analogous to P^{NP[f(n)]}. For example, P^{Σ_{2}^{P} [O(log n)]} contains all problems decidable in polynomial time with at most O(log n) calls to an Σ_{2}^{P} oracle.

1In fact, Quantified Propositional Formula (QPF) rather than QBF would be correct. In abuse of terminology, we do not distinguish between the isomorphic concepts of QPF and QBF.

Intuitively, a problem solvable with one NP oracle call is “easier” than a problem requiring a polynomial number of NP oracle queries; indeed, it is known that P^{NP[k]} = P^{NP[k+1]} for any k ≥ 1 implies the collapse of the PH, which is not expected by the experts [25]. Further, any algorithm for a P^{NP[f(n)]}-hard problem that is polynomial upon subroutine calls to an NP-complete problem is expected to make at least f(n) subroutine calls on input of length n.

3 Knowledge change and counterfactuals

We start with a review of operators for knowledge base change proposed in the literature. The proposed methods differ noticeably from one another, if we compare them according to the following three orthogonal classification criteria:

• Irrelevance of Syntax. In some approaches, the change consists in adding a new formula (the update) and retracting some formulas from the knowledge base T if this is necessary for preserving consistency. In this way, a formula has to be either retracted as a whole or left in the knowledge base. These approaches, referred to as formula-based changes, heavily depend on the syntax of T. On the other hand, model-based changes refer only to the extensions, i.e. models, of T. These methods respect Dalal’s principle of Irrelevance of Syntax [7].

• Revision versus Update. Different change operators are appropriate according to whether the theory-change consists of a revision, i.e. a correction to the actual state of beliefs due to new, more precise, or more reliable information for instance, or of an update reflecting a change in the world described by the knowledge base. This fundamental distinction is extensively discussed in [32, 57, 58, 30]. Katsuno and Mendelzon give a nice characterization of revision versus update for model-based approaches in [30], where they set forth a set of update postulates different from revision postulates [1]. They point out that revision operators operate globally on sets of models, that is, each model of the revised knowledge base must be as close as possible to the set of all models of the initial knowledge base. One particular measure of distance is to define the “distance” between a model M and a set S of models as the minimum over the “distances” between M and any element of S; for a general definition, see [31]. On the other hand, update semantics is always “pointwise”, that is, each model M of the initially given knowledge base is changed separately with minimal change, and the result of the update is the union of the updates of all those models M.

• Measure of Closeness. Both the formula-based approaches and the model-based approaches need a notion of “closeness”. In the formula-based approaches, one compares the closeness between theories, i.e. between sets of formulas. In the modelbased approaches one compares the closeness between models, i.e. between sets of atoms. Two well-known measures of closeness are the cardinality-based and the inclusion-based measure. The cardinality-based measure expresses the distance between two sets by the number of items in which they differ. The inclusion-based measure, instead, states that a set S_{1} is closer to a set S than a set S_{2} if the elements on which S_{1} and S differ are a proper subset of the elements on which S_{2} and S differ, i.e. if S_{1}△S ⊂ S_{2}△S holds (A△B is the symmetric set difference (A ∪ B) − (A ∩ B) ). Note that other measures of closeness are conceivable; Katsuno and Mendelzon developed a very general notion of closeness in terms of pre-orders on the sets of models [28, 31].

3.1 Formula-Based Change

If a knowledge base T is inconsistent with new knowledge p, a straightforward method to gain consistency with p is to remove formulas from the knowledge base. This approach apparently injures the principle of Irrelevance of Syntax in knowledge base change, and is thus rejected by many researchers; but it also has its defenders, cf. [19, 44], and there are scenarios which illustrate the need to differentiate in some epistemic contexts between syntactically deviating descriptions of the world [31]. Nebel points out an important relation between formula-based and model-based change, however, showing that formulabased change operators can be reconstructed as change operators acting on the deductive closure (i.e., as model-based change operators) [44].

Ginsberg’s Approach:

A straight solution for knowledge base change that obeys the principle of Minimal Change is the Set-Of-Theories approach in [13, 12], which is the basis for counterfactuals in [19, 44, 45]. We refer to this approach as “Ginsberg’s approach” throughout this paper. Let T be satisfiable, and let

W (p, T) = {T′ ⊆ T : T′ |̸= ¬p, T′ ⊂ U ⊆ T ⇒ U ⊧ ¬p}.

(W (p, T) are the “possible worlds” for p from belief in T [19].^{2}) Then, define

T ∘_{G} p = {T′ ∪ {p} : T′ ∈ W (p, T)}.

That is, T ∘_{G} p is the family of maximal subsets T′ ⊆ T that are consistent with p, each of them augmented by p.

2Ginsberg’s term “possible worlds” may be misleading since W (p, T) does not refer to possible worlds (in the technical sense) at all but to subsets of a set of formulas.

Example 3.1 Let T = {a, b, a ∧ b ⇒ c} and p = ¬c. Then, W (p, T) = {{a∧b ⇒ c, b}, {a ∧ b ⇒ c, a}, {a, b}}, hence T ∘_{G} p = {{a ∧ b ⇒ c, b, ¬c}, {a ∧ b ⇒ c, b, ¬c}, {a, b, ¬c}}.

A formula q is true after a change iff it is valid in all knowledge bases of T ∘_{G} p, which are considered to be independent. Thus after a single change, a formula is true iff it is valid in the logical disjunction of the knowledge bases in T ∘_{G} p.^{3} For example, the formula a ∨ b is valid in T ∘_{G} p from Example 3.1. Note that maximal consistent subsets of theories were used in a similar way (but in a different context) by Rescher [50, 51]. The disadvantage that incorporating p into T may result in multiple knowledge bases gave rise to the Cross-Product approach and the WIDTIO approach, which combine all resulting knowledge bases into a single one.

The Cross-Product Approach:

This approach [13] constructs a knowledge base whose formulas are, roughly speaking, all disjunctions with one formula from each knowledge base in T ∘_{G} p. Precisely, if T ∘_{G} p = {T_{1}, …, T_{m}}, then

T ∘_{C} p = {p_{1} ∨ ⋯ ∨ p_{m} : p_{i} ∈ T_{i}, 1 ≤ i ≤ m}.

The difficulty with this change operator is to construct an efficient implementation (the number of formulas may grow exponentially in the size of T ∘_{G} p). It is known that T ∘_{G} p ≡ T ∘_{C} p; therefore we will not explicitily deal with ∘_{C}; all results derived for ∘_{G} are also valid for ∘_{C}.

The WIDTIO Approach:

The WIDTIO (When In Doubt Throw It Out [58]) approach [19, 21] solves the multiple knowledge bases problem by the following definition:

T ∘_{W id} p = ⋂_{W ∈W (p,T)} W ∪ {p},

i.e. only the formulae that appear in all possible worlds are retained. This method is easy to implement in terms of the size of the revised knowledge base, but has the disadvantage that in the worst case all knowledge in T has to be retracted.

Example 3.2 Consider T = {a, b, a ∧ b ⇒ c}, p = ¬c from Example 3.1 again. Then T ∘_{W id} p = {¬c}. Note that a ∨ b is not implied by T ∘_{W id} p.

3Nebel [45] gives an elegant characterization of T ∘_{G} p using deductive closure of a set of formulas.

3.2 Model-Based Change

Model-based change operators refer only to the extensions, i.e. the models of a knowledge base to gain irrelevance of syntactical knowledge representation. Model theoretic characterizations of minimal change are given in [28, 58, 30].

The considered model-based change operators rely heavily on the notion of model closeness defined by M△M, that is the set of propositional variables whose value in M is different than in M′. For quick reference, we provide at the begin of this section a compact definition of all model-based change operators that we consider (Tables 1,2).

(Tables 1,2 go here)

More details and examples are provided in the rest of this section.

3.2.1 Revision

Alchourrón, Gärdenfors, and Makinson [1] proposed eight postulates G*1∼G*8 that a change operator ∘, in their terms revision operator, should satisfy. Katsuno and Mendelzon gave the following equivalent formulation for the specialization to propositional logic and finite knowledge bases (see [28, 31] for a full discussion):

(R1) T ∘ p implies p.

(R2) If T ∧ p is satisfiable, then T ∘ p ≡ T ∧ p.

(R3) If p is satisfiable then T ∘ p is also satisfiable.

(R4) If T_{1} ≡ T_{2} and p_{1} ≡ p_{2}, then T_{1} ∘ p_{1} ≡ T_{2} ∘ p_{2}.

(R5) (T ∘ p_{1}) ∧ p_{2} implies T ∘ (p_{1} ∧ p_{2}).

(R6) If (T ∘ p_{1}) ∧ p_{2} is satisfiable, then T ∘ (p_{1} ∧ p_{2}) implies (T ∘ p_{1}) ∧ p_{2}.

Dalal’s Approach:

Dalal [6] proposes to interpret minimality of change in terms of minimal cardinality of model change. In his approach, T ∘ p has those models of p which have as few variables different from any model of T as possible. Define the distance between formulas p and q as

|△|^{min}(p, q) = min {|M△M′| : M ∈ Mod(p), M′ ∈ Mod(q)} ,

that is |△|^{min}(p, q) is the minimum number of propositional symbols in which models of p and q diverge. Dalal’s revision operator ∘_{D} can be defined as follows: If T is satisfiable, then

Mod(T ∘_{D} p) = {M ∈ Mod(p) : ∃M′ ∈ Mod(T) s.t. |M△M′| = |△|^{min}(T, p)}

M … model, p, q … propositional formulas

△^{min}(p, q) = min_{⊆} ({M△M′ : M ∈ Mod(p), M′ ∈ Mod(q)})
△_{M}^{min}(p) = min_{⊆} ({M△M′ : M′ ∈ Mod(p)})
|△|^{min}(p, q) = min {|M△M′| : M ∈ Mod(p), M′ ∈ Mod(q)}
|△|_{M}^{min}(p) = min {|M△M′| : M′ ∈ Mod(p)}
Ω(p, q) = {x : ∃D ∈ △^{min}(p, q) s.t. x ∈ D}

min_{⊆} selects the minimal elements under set inclusion

Table 1: Summary of functions for closeness measures

operator ∘  Mod(T ∘ p)^{∗}
T ∧ p unsatisfiable  T ∧ p satisfiable

Dalal ∘_{D} {M ∈ Mod(p) : ∃M′ ∈ Mod(T) s.t. |M△M′| = |△|^{min}(T, p)} Mod(T ∧ p)

Forbus ∘_{F}  ⋃_{M∈Mod(T)} {M′ ∈ Mod(p) : |M′△M| = |△|_{M}^{min}(p)}
Borgida ∘_{B} ⋃_{M∈Mod(T)} {M′ ∈ Mod(p) : M△M′ ∈ △_{M}^{min}(p)} Mod(T ∧ p)
Winslett ∘_{W in}  ⋃_{M∈Mod(T)} {M′ ∈ Mod(p) : M△M′ ∈ △_{M}^{min}(p)}

Satoh ∘_{S} {M ∈ Mod(p) : ∃M′ ∈ Mod(T) s.t. M△M′ ∈ △^{min}(p, T)} Mod(T ∧ p) Weber ∘_{W eb} {M ∈ Mod(p) : ∃M′ ∈ Mod(T) s.t. M − Ω(T, p) = M′ − Ω(T, p)} Mod(T ∧ p)

∗Mod(T ∘_{D} p) = Mod(p), Mod(T ∘_{W eb} p) = Mod(T) if T or p is unsatisfiable

Table 2: Model-based revision operators and if T is unsatisfiable, then Mod(T ∘_{D} p) = Mod(p). It is well-known that ∘_{D} satisfies (R1)∼(R6) [28] (Dalal himself already noticed that ∘_{D} satisfies the Gärdenfors postulates [6]).

Example 3.3 Let T = {a, b, c} and p = (¬a ∧ d) ∨ (a ∧ ¬b ∧ ¬c ∧ ¬d). Note that |△|^{min}(T, p) = 1: Since T ∧ p is unsatisfiable, |△|^{min}(T, p) > 0, but {a, b, c, d} ∈ Mod(T), {b, c, d} ∈ Mod(p) and |{a, b, c, d}△{b, c, d}| = 1. It is easily verified that T ∘_{D} p ≡ ¬a ∧ b ∧ c ∧ d.

Satoh’s Approach:

According to Satoh’s approach [53], the change operator selects, similar to Dalal’s approach, only the models of p that are closest to T; the notion of closeness is set-inclusion instead of cardinality of model difference, however. Satoh defined his operator for the first-order case using circumscription. Let for any formulae p, q

△^{min}(p, q) = min_{⊆} ({M△M′ : M ∈ Mod(p), M′ ∈ Mod(q)}) ,

that is △^{min}(p, q) is the family of ⊆-minimal sets of differences between models of p and q. Satoh’s change operator ∘_{S} can be defined in the propositional context by

Mod(T ∘_{S} p) = {M ∈ Mod(p) : ∃M′ ∈ Mod(T) s.t. M△M′ ∈ △^{min}(T, p)} .

It is well-known that if T is satisfiable, ∘_{S} satisfies (R1)∼(R5) but not (R6) [28].

Example 3.4 Let T = {a, b} and p = (¬a ∧ c) ∨ (¬a ∧ ¬b ∧ ¬c). Note that T ∧ p is unsatisfiable. It is easily checked that △^{min}(T, p) = {{a}} and that {b, c} is the only model of p selected by ∘_{S}. Therefore, T ∘_{S} p ≡ ¬a ∧ b ∧ c.

Borgida’s Approach:

The revision operator ∘_{B} proposed by Borgida [3] uses like ∘_{S} set inclusion instead of cardinality to interpret minimality of change. Let for a model M and a formula p be

△_{M}^{min}(p) = min_{⊆} ({M△M′ : M′ ∈ Mod(p)}) ,

that is, △_{m}^{min}(p) is the family of ⊆-minimal difference sets between any model of p and M. Borgida’s operator can be defined as follows. If T ∧ p is satisfiable, then T ∘_{B} p ≡ T ∧ p; otherwise, for every M ∈ Mod(T) all models of p that are closest to M with respect to set inclusion are selected, that is

Mod(T ∘_{B} p) = ⋃_{M∈Mod(T)} {M′ ∈ Mod(p) : M△M′ ∈ △_{M}^{min}(p)} .

If T is satisfiable, ∘_{B} satisfies (R1)∼(R5) but not (R6) [28]. Note that ∘_{B} operates globally if T ∧ p is satisfiable, but pointwise if T ∧ p is not satisfiable.

Example 3.5 Consider T = {a, b} and p = (¬a ∧ c) ∨ (¬a ∧ ¬b ∧ ¬c) from Example 3.4 again. T has two models M_{1}, M_{2} on variables a, b, c: M_{1} = {a, b} and M_{2} = {a, b, c}. Then, △_{M_{1}}^{min}(p) = {{a, c}, {a, b}}, and changing M_{1} yields the two models {} and {b, c}; △_{M_{2}}^{min}(p) = {{a}}, and changing M_{2} yields the model {b, c}. Thus T ∘_{B} p ≡ (¬a ∧ ¬b ∧ ¬c) ∨ (¬a ∧ b ∧ c). Note that T ∘_{B} p ≢ T ∘_{S} p.

Weber’s Approach:

Weber [56] proposes a change operation that eliminates first all variables from T that occur in any minimal model change under Satoh’s semantics and then joins p to the resulting knowledge base.

Define res_{x}(T) = T_{x}^{+} ∨ T_{x}^{−} for variable x, where T_{x}^{+} (T_{x}^{−}) denotes the formula obtained by replacing all occurrences of x in T by true (false). For any set U = {u_{1}, …, u_{n}} of variables, define res_{U}(T) = res_{u_{1}}(res_{u_{2}}(⋯ res_{u_{n}}(T) ⋯)). Let for formulas p, q be Ω(p, q) the variables in △^{min}(p, q), i.e.

Ω(p, q) = {x : ∃D ∈ △^{min}(p, q) s.t. x ∈ D} .

If T or p is unsatisfiable, then T ∘_{W eb} p is defined as T; otherwise, T ∘_{W eb} p = res_{Ω}(T) ∧ p, Ω = Ω(T, p). In terms of models, ∘_{W eb} can be defined for satisfiable p by

Mod(T ∘_{W eb} p) = {M ∈ Mod(p) : ∃M′ ∈ Mod(T) s.t. M − Ω(T, p) = M′ − Ω(T, p)} .

If T and p are satisfiable, then ∘_{W eb} satisfies (R1)∼(R4), but neither (R5) nor (R6) [31].

Example 3.6 Consider T = {a, b} and p = (¬a ∧ c) ∨ (¬a ∧ ¬b ∧ ¬c) from Example 3.4 for the third time. Since △^{min}(T, p) = {{a}}, we get Ω(T, p) = {a} and res_{{a}}(T) = (true ∧ b) ∨ (false ∧ b). Thus T ∘_{W eb} p, which is res_{Ω}(T) ∧ p, is equivalent to ¬a ∧ b ∧ c.

3.2.2 Update

A clear distinction between the notions of revision and update in theory and knowledge base change, as provided for databases in [32], emerged more recently [30]. Revision describes the incorporation of new knowledge about the unchanged world into the knowledge base, whereas updating means to bring the knowledge base up to date when the described world changes. Katsuno and Mendelzon set up the following postulates that any update operator ⋄ should obey (see [31, 30] for a full discussion):

(U1) T ⋄ p implies p.

(U2) If T implies p then T ⋄ p is equivalent to T.

(U3) If both T and p are satisfiable, then T ⋄ p is also satisfiable.

(U4) If T_{1} ≡ T_{2} and p_{1} ≡ p_{2}, then T_{1} ⋄ p_{1} ≡ T_{2} ⋄ p_{2}.

(U5) (T ⋄ p_{1}) ∧ p_{2} implies T ⋄ (p_{1} ∧ p_{2}).

(U6) If T ⋄ p_{1} implies p_{2} and T ⋄ p_{2} implies p_{1}, then T ⋄ p_{1} ≡ T ⋄ p_{2}.

(U7) If T is complete, then (T ⋄ p_{1}) ∧ (T ⋄ p_{2}) implies T ⋄ (p_{1} ∨ p_{2}).

(U8) (T_{1} ∨ T_{2}) ⋄ p ≡ (T_{1} ⋄ p) ∨ (T_{2} ⋄ p).

The most important differences between update and revision are that updating means changing every model of the knowledge base separately (U8) and that an unsatisfiable knowledge base remains unsatisfiable when updated (U2). For convenience, we use ∘ for both kinds of knowledge base change.

Forbus’s Approach:

Forbus developed a method for updating in the context of qualitative simulation [14]. As Dalal, Forbus bases change semantics on cardinality of model differences, but decides to change each model of T independently (cf. [58, p.24]). Define the distance |△|_{M}^{min}(p) between a model M and a formula p as

|△|_{M}^{min}(p) = min{|M△M′| : M′ ∈ Mod(p)},

i.e. as the minimum number of variables in which M and a model of p diverge. In our framework, Forbus’s change operator ∘_{F} can be defined by

Mod(T ∘_{F} p) = ⋃_{M∈Mod(T)} {M′ ∈ Mod(p) : |M′△M| = |△|_{M}^{min}(p)} .

It is easily verified from Theorem 3.1 in [30] that ∘_{F} satisfies (U1)∼(U8).^{4}

Example 3.7 Consider T = {a, b, c} and p = (¬a∧d)∨(a∧¬b∧¬c∧¬d) from Example 3.3 again. T has two models M_{1} = {a, b, c} and M_{2} = {a, b, c, d} on variables a, b, c, d. Then, |△|_{M_{1}}^{min}(p) = 2 and changing M_{1} yields the models {a}, {b, c, d}, and |△|_{M_{2}}^{min}(p) = 1 and changing M_{2} yields the model {b, c, d}. Therefore, T ∘_{F} p ≡ (a∧¬b∧¬c∧¬d)∨(¬a∧b∧c∧d). Note that T ∘_{D} p ≢ T ∘_{F} p.

Winslett’s Approach:

Winslett introduced her “Possible Models Approach” for reasoning about action in firstorder calculus [57, 58]. Let for a model M and a formula p denote

△_{M}^{min}(p) = min_{⊆} ({M△M′ : M′ ∈ Mod(p)}) ,

4[31, Example 6.2] considers an operator that operates as ∘_{F} if T ∧ p is unsatisfiable and yields T ∧ p if T ∧ p is satisfiable. Our complexity results for ∘_{F} carry over to this operator analogously as the results for ∘_{W in} carry over to ∘_{B}.

i.e. △_{M}^{min}(p) is the family of minimal differences between a M and modeled of p. Winslett’s change operator can be defined for the propositional case by

Mod(T ∘_{W id} p) = ⋃_{M∈Mod(T)} {M′ ∈ Mod(p) : M△M′ ∈ △_{M}^{min}(p)} .

The operator ∘_{W in} satisfies (U1)∼(U8) [30]. Note that the only case in which ∘_{W in} may diverge from ∘_{B} is if T ∧ p is satisfiable: here ∘_{W in} operates pointwise while ∘_{B} operates global (hence, (U8) is not satisfied by ∘_{B}). This subtle difference, however, proved to be favorable for appropriate change semantics for reasoning about action.

Example 3.8 Consider the classic example T = {a ≡ ¬b} and p = a [57]. Note that T ∧p is satisfiable; hence, T ∘_{B} p ≡ a∧¬b. Note that T has the two models M_{1} = {a}, M_{2} = {b} on variables a, b; changing M_{1} yields the model {a} (△_{M_{1}}^{min}(p) = {}), and changing M_{2} yields the model {a, b} (△_{M_{2}}^{min}(p) = {{a}}), thus T ∘_{W in}p ≡ a. If a means “a book is on the floor” and b “a magazine is on the floor”, T states that either the book or the magazine is on the floor. If a robot is ordered to put the book on the floor, it is reasonable to accept only that a holds after this action; why should we accept that a∧¬b is true afterwards, i.e. the magazine is not on the floor, as suggested by revision operators satisfying (R2)? This indicates that Winslett’s approach is more appropriate for describing change actions.

3.3 Counterfactuals

A counterfactual is a conditional statement such as “If p, then q”, where it is known or expected that p is false [34, 19].^{5} The epistemic semantics for counterfactuals of our concern is based on the Ramsey Test [15, p. 147]:

Accept a sentence of the form ‘If A, then C’ in a state of belief K if and only if the minimal change of K needed to accept A also requires accepting C.

For extensive studies of such counterfactuals refer to [19, 15]. Ginsberg [19] points out the importance of counterfactuals for a large number of areas within AI.

Technically, counterfactuals are definable under all change operators from above. Given T and change operator ∘, define that “If p, then q” (denoted by p > q) is true over T iff T ∘ p ⊧ q holds, and that that p > q is false over T iff T ∘ p |̸= q holds.

Gärdenfors tried to define a counterfactual connective based for the object language based upon a change operator subject to revision semantics, but found that this is incompatible with the Ramsey Test in all but in a certain sense “trivial” logics (Gärdenfors’s Triviality Theorem, cf. [15, p.158,Theorem 7.10]). Recent investigations showed that update semantics is not subject to the Triviality Theorem and may be a more fruitful way of modeling counterfactuals [23, 29]. (Lewis’s logic of conditionals [34], in which a system of spheres plays an important role in defining “most similar worlds”, also has an updatesemantics flavor.) Note that we consider counterfactuals at the meta-level, to which the triviality result does not apply.

5In a somewhat weaker notion it is sufficient that p may be false, e.g. [23]. Under the Ramsey principle, this notion matches inference from a knowledge base which has to be updated or revised under minimal change.

The problem of our study is the following basic issue in counterfactual reasoning: Given a knowledge base T and formulae p, q, is p > q true over T ? We name this problem COUNTERFACTUAL (CF); an index will indicate which change semantics is applied.

Example 3.9 Consider the following example. Let r denote “It is raining”, c, “It is cold” h, “I stay at home”, and g, “Gorbachev is president of the United States”. Assume that the knowledge base T is given by T = {r, ¬c, ¬g, r ∧ c ⇒ h}. Consider the counterfactual c > h, which means, “If it would be cold, I would stay at home”. We get W (T, c) = {{r, ¬g, r ∧ c ⇒ h}}, and hence T ∘_{G} c = {{r, ¬g, r ∧ c ⇒ h, c}}. Clearly T ∘_{G} c ⊧ h holds, and therefore c >_{G} h is true over T. On the other hand, the counterfactual “If it would be cold, Gorbachev would be president of the United States” is false over T, because T ∘_{G} c |̸= g holds. Note that the “classical” implications c ⇒ h and c ⇒ g are both valid in the knowledge base T.

Example 3.10 Consider Winslett’s example T = {a ≡ ¬b}, p = a again. The counterfactual a >_{W in} ¬b, which means “If the robot would put the book on the floor (assuming it’s not already there), then the magazine would not be on the floor”, is not true over T since T ∘_{W in} p ≡ a. Not that a > b is true over T under all semantics but >_{W in} and >_{F}.

Example 3.11 Assume a court has to hear three independent witnesses W_{1}, W_{2}, and W_{3} in a trial. The belief that W_{i} tells the truth is denoted by the atom t_{i}. The initial assumption of the court is that all witnesses are sincere, i.e. T = {t_{1}, t_{2}, t_{3}}. The testimonies of the witnesses are contradictory, however, such that if W_{1} is honest, then W_{2} and W_{3} are liars, but if one of W_{2}, W_{3} is honest, then W_{1} is a liar. This amounts to the following formula p:

p = (t_{1} ⇒ ¬t_{2} ∧ ¬t_{3}) ∧ (t_{2} ∨ t_{3} ⇒ ¬t_{1}).

The court usually tends to assume that a maximum number of independent witnesses are honest, and therefore concludes that W_{1} is a liar (for otherwise both W_{2} and W_{3} would lie). This policy is appropriately represented by a cardinality-based revision operator like Dalal’s. Indeed, the counterfactual p >_{D} ¬t_{1}, which means “If honesty of W_{1} would entail that W_{2} and W_{3} lie, and if honesty of W_{2} or W_{3} would mean that W_{1} lies, then the court would belief that W_{1} lies”, is true over T = {t_{1}, t_{2}, t_{3}}. Note that p > ¬t_{1} evaluates to false over T under all considered semantics but >_{D} and >_{F}.

The examples show that different change semantics are appropriate in different situations, and that choosing a particular approach over another is domain dependent. It is currently unclear for which domains the consider change semantics are favorable, and further research will be necessary to clarify this issue; our concern is with their computational properties, however.

We will pay special attention to the following restrictions of CF: the case in which T is a set of Horn formulas and p, q are Horn formulas, and the case in which the change knowledge described by p involves only a few facts. Moreover, we will consider most time counterfactuals on knowledge bases that contain only atoms or negated atoms, as our hardness results will hold even under this restriction.

4 Overview and discussion of results

In this section we summarize and discuss our results and indicate possible extensions that we are currently investigating.

The main results of this paper are compactly presented in Table 3. Different methods according to the different change semantics for evaluating a counterfactual p > q over a propositional knowledge base correspond to different rows in this table. Recall that a counterfactual p > q over a knowledge base T is true iff T ∘ p ⊧ q where “∘” is the chosen change operator; in other terms, evaluating a counterfactual p > q is equivalent to testing whether q could be inferred after a hypothetical knowledge base change p.

The table contains four columns. The first two columns account for the case where T is a general propositional knowledge base, while the last two columns reflect the Horn case. In the Horn case we assume that p,q and all formulae in T are conjunctions of Horn clauses. Columns one and three describe those cases in which no bound is imposed on the size ∥p∥ of the knowledge base change (or antecedent) p, columns two and four account for those cases where the size of p is bounded by a constant.

Let us discuss the results. The first thing to notice is that in the general case with no restriction on p, for all approaches except Dalal’s, the complexity of testing p > q is at the second level of the polynomial hierarchy. More precisely, for most change operators the problem is Π_{2}^{P} -complete and for two (WIDTIO and Weber’s) it is very close to Π_{2}^{P}. Under the assumption that the polynomial hierarchy does not collapse,^{6} this means that counterfactual inference is harder than classical inference. On the other hand, the second level of the polynomial hierarchy is still a very low level, and, in a certain sense, much closer to the first level than to PSPACE.

In more practical terms, the Π_{2}^{P} -hardness results state that with current methods, if we have at our disposal any subroutine for solving NP-complete problems, we would need (in the worst case) an exponential number of calls to this subroutine for deciding whether the counterfactual p > q holds.

Loosely speaking, the Π_{2}^{P} -hardness is mostly due to the interaction of two different sources of complexity. The first source is the complexity of inference in propositional logic (co-NP-hard) and the second source is the large number of choices that we have in general to make a knowledge base (or a model) consistent with a proposition p performing a minimal change.

6We will make this generally accepted assumption [25] for the rest of the discussion in this section.

COUNTERFACTUAL  GENERAL CASE  HORN FORMULAS
p > q true in T?  arbitrary p  ∥p∥ ≤ k  arbitrary p  ∥p∥ ≤ k

Ginsberg: p >_{G} q Π_{2}^{P}-complete co-NP-complete

WIDTIO: p >_{W id} q Π_{2}^{P}-hard, in PΣ^{2}^{P}^{[O(log n)]} co-NP-hard, in P^{NP^{[O(log n)]}}

Dalal: p >_{D} q P^{NP^{[O(log n)]}}-complete NP- and co-NP-hard,

in P^{NP^{[O(1)]}} P^{NP^{[O(log n)]}}-complete

O(∥T ∥·∥q∥)

Forbus: p >_{F} q

Π_{2}^{P}-complete  co-NP-complete  Π_{2}^{P}-complete

O(∥T ∥·∥q∥)

Borgida: p >_{B} q Π_{2}^{P}-complete NP- and co-NP-hard,

in P^{NP^{[2]}} co-NP-complete

O(∥T ∥·∥q∥)

Winslett: p >_{W in} q

Π_{2}^{P}-complete  co-NP-complete  co-NP-complete

O(∥T ∥·∥q∥)

Satoh: p >_{S} q Π_{2}^{P}-complete NP- and co-NP-hard,

in P^{NP^{[O(1)]}} co-NP-complete

O(∥T ∥·∥q∥)

Weber: p >_{W eb} q

Π_{2}^{P}-hard, in PΣ^{2}^{P}^{[O(log n)]} NP- and co-NP-hard,

in P^{NP^{[O(1)]}}

co-NP-hard, in P^{NP^{[O(log n)]}}

O(∥T ∥·∥q∥)

Table 3: Complexity results for propositional counterfactual evaluation The only exception in the first column of our table is Dalal’s approach, which is complete for the class P^{NP[O(log n)]}. This means that the we can decide p > q with O(log n) calls to an NP oracle, where n stands for the size of T plus p plus q. As will become clear from the proof in Section 6, the deep reason for this relative easiness is that in Dalal’s approach the two sources of complexity are not intermingled and can be separated from one another.

Interestingly, the syntax-based approaches remain Π_{2}^{P} -hard even if the size of p is bounded by a constant k. This insensitivity towards the size of the knowledge change p can be intuitively explained as follows: even a small change may be have drastic effects by forcing some originally unessential part of a formula in T to become true. For instance, if T contains two formulas f_{1} = ¬u ∨ (x_{1} ∧ x_{2} ∧ … ∧ x_{n}), f_{2} = ¬u and if p is equal to u, then p forces the originally completely irrelevant conjunction (x_{1} ∧ x_{2} ∧ … ∧ x_{n}) to become true.

On the other hand, the complexity of the model-based approaches decreases when the size of p is bounded by a constant. The intuitive reason for this is that a small change p can affect only few literals; since in this case there are only few alternatives for changing a given model, the second source of complexity disappears.

In the Horn case, the complexity of all approaches except Forbus’s is at the first level of the polynomial hierarchy, more precisely, co-NP-equivalent. Intuitively, this lowering of complexity is due to the fact that with Horn clauses the inference problem becomes polynomial, and hence the first of the aforementioned two sources of complexity is eliminated. The cardinality based approaches of Dalal and Forbus are the only ones whose complexity does not decrease under the Horn restriction. This is because their cardinality-based measure of closeness between models has a detrimental effect on the benign properties of Horn clauses.

Let us finally consider the case where both restrictions, Horn formulas and bounded p, are combined. The complexity results corresponding to this case are shown in the fourth column of our table. As in the general case, bounding the size of p does not improve the complexity of the formula-based methods. The model-based methods, however, all become polynomial under these restrictions and allow counterfactual evaluation even in O(∥T ∥·∥q∥) time in this case.

Note that the theorems presented in the following sections often state yet more acute results than the ones shown in Table 3. For instance, we show that most hardness and completeness results hold even in case T is literal base, i.e. T consists of a set (or conjunction) of atoms or negated atoms.

All results presented in Table 3 are new except the Π_{2}^{P} -completeness of Ginsberg’s approach for the general case. The latter has recently been shown by Nebel in [45]. Note that in Nebel’s proof it is assumed that the given knowledge base T is unsatisfiable. This assumption is not reasonable in the context of counterfactuals [19]. Our proof is completely different and does not make this unsatisfiability assumption. We note, however, that Nebel’s proof could be easily transformed using Corollary 1 in [45] into a proof that works also for a satisfiable T. Nebel’s proof, on the other hand, does not generalize to most other approaches (in particular, the model based approaches require a different proof technique).

An important extension that we do not deal with explicitly is the possibility of protecting formulas in T. The set I ⊆ T of protected formulas of T can be viewed as integrity constraints that must not be violated by any change. It is thus required that the changed knowledge base T ∘ p satisfies I, i.e. T ∘ p ⊧ I. Note that in the case where p is not restricted, this can always be enforced by “adding” I to the change p, i.e. computing T ∘ (p ∧ I). Hence in such cases, the possibility of protecting formulas does not alter our complexity results. It is also quite easy to see that even in the case where ∥p∥ is bounded by a constant the worst case complexity of CF is not altered if protection of formulas is allowed. For these reasons, we do not treat this feature as a special case in this paper.

Nebel has also studied in [45] a restriction for the syntax based methods that we do not consider here: disambiguating the knowledge base change by attaching different priorities to the sentences in T. Clearly, such a policy eliminates the second source of complexity, and therefore the complexity level will be lowered by one in general. Note that this prioritization of sentences cannot be applied in the model-based cases. Here we could use a total order on the propositional variables (similar in some sense to the partial order used in prioritized circumscription [35, 38]) indicating which variable should change its value first if an inconsistency has to be removed. We leave a detailed study of such restrictions for the future.

Another very interesting issue are compound counterfactuals and sequences of knowledge change. A counterfactual of the form p > (q > r) corresponds to the question “if p would hold, would q counterfactually imply r ?”. Some recent preliminary results of the authors indicate that as long as we use nested sequences of counterfactuals, the problem remains Π_{2}^{P} -complete for most approaches. However, if we mix counterfactual implication (>) with classical connectives (such as negation) then the problem becomes PSPACE-complete. Independently, Grahne and Mendelzon obtained a closely related PSPACE-completeness result in [24], where, loosely speaking, the complexity of evaluating formulas built with classical connectives and a counterfactual connective that adheres to the ∘_{W in} semantics on a set of models is considered. Their results entail also that, in our terms, evaluating in this setting a nested counterfactual mixed with classical connectives over a knowledge base is PSPACE-complete.

5 Related results and further consequences

Counterfactuals are just one form of nonmonotonic reasoning, and their relationship to other well-known nonmonotonic reasoning mechanisms auch as circumscription, default logic, and truth maintenance systems has already been investigated by Ginsberg [19]. It is interesting to observe that similar complexity results have recently been derived for these approaches, which locate reasoning problems in all these formalism at the second level of the polynomial hierarchy. In particular, the following results have been found.

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 [48], several formalizations of closed world reasoning have been developed: the Generalized Closed World Assumption (GCWA) by Minker [41], the Extended Generalized Closed World Assumption (EGCWA) by Yahya and Henschen [60], the Careful Closed World Assumption (CCWA) by Gelfond and Przymusinska [18], and the Extended Closed World Assumption (ECWA) by Gelfond, Przymusinska, and Przymusinski [17]. Circumscription was introduced by Mc-Carthy in [37]. It is known that circumscription coincides with the ECWA in the case of propositional logic [17].

[10] deals with the complexity of closed world reasoning applied to general propositional theories and to unrestricted clause-sets. In particular, the deduction problem is studied, i.e., given formulae F and G, does G follow from F under a certain closed-world inference rule. It is shown that the deduction problems under the GCWA, the EGCWA, the CCWA, the ECWA are all at the second level of PH. In particular, the deduction problem both under the EGCWA and the ECWA (= propositional circumscription) is shown Π_{2}^{P} - complete, and Π_{2}^{P} -hardness is demonstrated for 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 (co-NP-hardness is shown in [5]).

For the GCWA and the CCWA, upper bounds are provided 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. It is also shown testing whether the closure under CWA of a formula F is consistent (a co-NP-hard problem, but most likely not in co-NP) can be done with O(log m) calls to an NP-oracle, where m is the number of propositional variables in F.

The results in [10] can be interpreted as follows: If the polynomial hierarchy does not collapse, then, for all considered closed world reasoning principles, the deduction problem is strictly harder than the deduction problem in classical propositional logic. In particular, depending on the chosen closed world principle except for the naive CWA, the deduction problem is either complete for Π_{2}^{P} or only “mildly” harder than Π_{2}^{P}. The deduction problem under the CWA is complete for Δ_{2}^{P} under Turing reductions, and thus not much harder than the deduction problem in the classical propositional logic. It is harder, however, since it is shown that this problem is neither in NP nor in co-NP unless the polynomial hierarchy collapses.

The complexity of several reasoning tasks in nonmonotonic propositional logics is investigated in [22]. The systems of logics considered are Reiter’s default logic [49], McDermott’s and Doyle’s nonmonotonic logic [40, 39], Moore’s autoepistemic logic [43], and Marek’s and Truszczyński’s nonmonotonic logic N [36]. All these logics have in common that the semantics of an initially given set of premises is explained through a corresponding set of fixed points (also called extensions or expansions). Given a set of premises, the main reasoning tasks in these logics are (i) testing for existence of a fixed point; (ii) deciding whether a given formula belongs to at least one fixed point (brave reasoning); and (iii) deciding whether a given formula belongs to all fixed points (cautious reasoning). It is shown that for all mentioned logics, problems (i), (ii) are complete for Σ_{2}^{P}, while problem (iii) is complete for Π_{2}^{P}.

Similar complexity results on abductive reasoning are given in [11], while in [52] it is shown that some special reasoning task in a generalization of De Kleer’s assumption-based truth management system (ATMS) [8] is complete for Σ_{2}^{P}.

In summary, it appears that the complexity of almost all approaches to nonmonotonic propositional reasoning is located at the second level of the polynomial hierarchy. As a practical consequence, most formalizations of nonmonotonic reasoning can be polynomially translated into one another, and existing algorithms or proof procedures for one approach can be fruitfully applied to the other.

For instance, Π_{2}^{P} -completeness of Winslett’s method and cautious default reasoning guarantees that the problem of evaluating a counterfactual p >_{W in} q can be polynomially transformed into an equivalent problem of brave reasoning in default logic. Thus, one can take profit of existing sophisticated procedures for default reasoning and of implemented default theorem-provers to solve counterfactuals. Similarly, by the established complexity results, one can polynomially translate most decision problems related to theory update or revision under various approaches to the problem of inferencing under (propositional) circumscription. Practical methods for inferencing under circumscription have been developed by [4, 20, 47]. Note that in the more general context of first-order logic, Winslett already pointed out the translatability of theory-update problems to circumscription [59].

6 Computational complexity: the general case

We consider CF in the most general case first, where p, q, and all formulas in T are arbitrary propositional formulas. We will see, however, that the worst case complexity of CF still occurs even if the knowledge base T contains only facts, that is, atomic chunks of knowledge.

Prior to complexity considerations, we make several observations on changing literal bases under various change semantics. If T is a literal base, then all knowledge in the knowledge base is represented by facts and negated facts, and if all facts of interest are considered (i.e. if the literal base is complete), the knowledge base is a unique description of the world. Certain change operators from above behave identical when applied to a literal base; several noticeable relationships in this context are captured by the following Lemma.

Lemma 6.1 Let T be a satisfiable literal base, and let p, q be propositional formulas.

(1) T ∘_{G} p ≡ T ∘_{S} p and p >_{G} q is true over T iff p >_{S} q is true over T.

(2) If V (p) ⊆ V (T), then T ∘_{S} p ≡ T ∘_{B} p ≡ T ∘_{W in} p, and the validity of p >_{S} q, p >_{B} q, and p >_{W in} q over T is equivalent.

(3) If V (p) ⊆ V (T), then T ∘_{D} p ≡ T ∘_{F} p, and p >_{D} q is true over T iff p >_{F} q is true over T.

(4) If p is satisfiable, then T ∘_{W id} p ≡ T ∘_{W eb} p, and p >_{W id} q is true over T iff p >_{W eb} q is true over T.

(5) Let q ∈ T, and let p be satisfiable. Then the validity of p >_{G} q, p >_{W id} q, p >_{S} q, and p >_{W eb} q over T is equivalent, and q ∈ T ∘_{W id} p iff p >_{G} q is true over T.

Proof: The equivalence of counterfactual validity under different change semantics is trivial if the knowledge bases are logically equivalent after change; thus for (1)–(4) it suffices to consider the equivalence of the change operators.

The definition of ∘_{S} entails that each D ∈ △^{min}(T, p) satisfies D ⊆ V (T) ∩ V (p), i.e. the models of T change merely on the common variables of T and p. It is obvious that either W ∧ p ⊧ f or W ∧ p ⊧ ¬f holds, for every W ∈ W (p, T) and f ∈ T. Therefore, if T is a literal base, maximality of W in Ginsberg’s approach is equivalent to Satoh’s minimality of truth value change of the variables in V (T) ∩ V (p). Thus (1), i.e. Mod(T ∘_{G} p) = Mod(T ∘_{S} p), holds.

Next we verify (2) and (3). Under change operation ∘ ∈ {∘_{B}, ∘_{W in}, ∘_{F} }, the models of T change only on the variables V (p) to become models of T ∘ p, but for ∘ ∈ {∘_{S}, ∘_{D}}, changes restrict to V (p) ∩ V (T). Since V (p) ⊆ V (T) and T has only one model on V (T), however, all stated equivalences must obviously hold (note: if in this case T ∧ p is satisfiable, Mod(T ∘_{B} p) = Mod(T) = Mod(T ∘_{W in} p) ).

(4) and (5) are verified as follows. Consider any formula f in the literal base T. From the definition of ∘_{G} follows that p >_{G} f is true over T iff f ∈ W, for all W ∈ W (p, T), which holds by the definition of ∘_{W id} iff f ∈ T ∘_{W id} p; an easy consideration is that the latter is true iff p >_{W id} f is true over T. Thus p >_{G} f is equivalent to p >_{W id} f over T; applying (1) we conclude that f ∈ T ∘_{W id} p iff p >_{S} f is true over T. As T is a literal base, it is straightforward that the variable of the literal f is in Ω(T, p) exactly if p >_{S} f is false over T. As f is arbitrary from T, it follows that Ω(T, p) = T − (T ∘_{W id} p), and by the model characterization of T ∘_{W eb} p (T and p are assumed satisfiable) we get easily Mod(T ∘_{W eb} p) = Mod(T ∘_{W id} p); thus (4) is true, and hence (5) is clearly also true. □

This interrelation of various change semantics will be heavily exploited to derive several complexity results with few proofs. For example, Lemma 6.1 is useful for one single proof of Π_{2}^{P} -hardness of CF under all change operators in Section 3 but Forbus’s and Dalal’s. In fact, we show the following.

Lemma 6.2 Let T be an atomic knowledge base. To decide if p > q is true over T is Π_{2}^{P} -hard for > ∈ {>_{G}, >_{W id}, >_{B}, >_{W in}, >_{S}, >_{W eb}}, even if q is an atom with q ∈ T.

Proof: Given an instance F = ∀\underline{x}∃\underline{y}E(\underline{x}, \underline{y}) of QBF_{2,∀}, we construct in polynomial time an atomic knowledge base T and formulae p, q such that q is an atom from T and p >_{G} q is true over T iff F is valid; since V (p) ⊆ V (T) holds, the claim will be easy to prove with Lemma 6.1.

Let \underline{x} =<x_{1}, …, x_{m}> and \underline{y} =<y_{1}, …, y_{n}>. Let z_{1}, …, z_{m} and r be additional propositional variables. We define T, p, and q as follows:

T = {x_{1}, …, x_{m}, z_{1}, …, z_{m}, y_{1}, … y_{n}, r}  (1)
p = [(x_{1} ≡ ¬z_{1}) ∧ … ∧ (x_{m} ≡ ¬z_{m}) ∧ (r ⇒ E(\underline{x}, \underline{y})) ∧ ((y_{1} ∨ … ∨ y_{n}) ⇒ r)]
q = r

Note that T and p are satisfiable, but T ∧ p is unsatisfiable. The construction of T, p, q is obviously feasible in time polynomial in the size of F.^{7}

Before proving that F is valid iff p >_{G} q is true over T, let us say a few words about the spirit behind our transformation.

Recall that each “possible world” is a maximal subset of T′ ⊆ T such that T′ ∧ p is satisfiable. It is easy to see that the counterfactual p >_{G} q is true over T iff r belongs to each “possible world” in W (p, T). The conjuncts of p serve for the following purposes:

• The conjuncts x_{i} ≡ ¬z_{i} make sure that each W ∈ W (p, T) contains at most one atom from {x_{i}, z_{i}}. Moreover, by the maximality requirement, W contains exactly one atom from {x_{i}, z_{i}}. Thus, W_{1}, W_{2} ∈ W (p, T) differing in their x_{i} elements are incomparable with respect to set inclusion.

• The conjunct r ⇒ E(\underline{x}, \underline{y}) makes sure that for each W ∈ W (p, T) such that r ∈ W, W ∧ p ⊧ E(\underline{x}, \underline{y}) holds.

• The conjunct (y_{1} ∨ ⋯ ∨ y_{n}) ⇒ r enforces that for each W ∈ W (p, T) with r ∉ W, W ⊆ {x_{1}, z_{1}, …, x_{m}, z_{m}} holds.

Let us now show that F is valid iff p >_{G} q is true over T.

First observe that for each W ∈ W (p, T), either x_{i} ∈ W or z_{i} ∈ W, 1 ≤ i ≤ m. Indeed, assume that {x_{i}, z_{i}}∩W = ∅ for some i. Then, since W ∧p is satisfiable, M ∈ Mod(W ∧p) exists such that M ⊧ x_{i} or M ⊧ z_{i}. Thus W ∧ x_{i} ∧ p or W ∧ z_{i} ∧ p is satisfiable, and hence W ∉ W (p, T), contradiction. Note that clearly at most one of x_{i}, z_{i} is contained in W.

It thus holds that every W ∈ W (p, T) “fixes” together with p a unique truth assignment ϕ_{W} to \underline{x} by ϕ_{W} (x_{i}) =true if x_{i} ∈ W and ϕ_{W} (x_{i}) =false if z_{i} ∈ W, for 1 ≤ i ≤ m. Conversely, for any truth assignment ϕ to \underline{x}, the set

W_{ϕ} = {x_{i} : ϕ(x_{i}) =true, 1 ≤ i ≤ m} ∪ {z_{i} : ϕ(x_{i}) =false, 1 ≤ i ≤ m}

is consistent with p (just assign false to y_{1}, …, y_{n},r), and W_{ϕ} ∧ p fixes ϕ; it follows immediately that for any ϕ there exists a W ∈ W (p, T) such that W ∧ p fixes ϕ.

7Note that a straightforward simpler construction for >_{G} obtained by removal of all y_{i} from T and cancellation of y_{1} ∨ ⋯ ∨ y_{n} ⇒ r in p does not allow application of Lemma 6.1.

Now assume that p >_{G} q is true over T. Then for all W ∈ W (p, T) we have W ∧ p ⊧ r and thus clearly r ∈ W. Consequently, for every truth assignment ϕ to \underline{x}, there is some W ∈ W (p, T) such that W ⊃ W_{ϕ} (hence ϕ_{W} = ϕ) and r ∈ W. Since W ∧ p is satisfiable and W ∧ p ⊧ r ⇒ E(ϕ(\underline{x}), \underline{y}), this implies that some truth assignment ψ to \underline{y} exists such that E(ϕ(\underline{x}), ψ(\underline{y})) is true. Thus F is valid.

Conversely, assume F is valid, but p >_{G} q is false over T. Then W ∈ W (p, T) exists such that W ∧ p |̸= r, which means r ∉ W. By the conjunct (y_{1} ∨ ⋯ ∨ y_{n}) ⇒ r of p, it is immediately clear that y_{i} ∉ W, for 1 ≤ i ≤ n. Consequently, W = W_{ϕ} for some truth value assignment ϕ to \underline{x}. Since F is valid, E(ϕ(\underline{x}), \underline{y}) is satisfiable, hence clearly W ∧ p ∧ r is satisfiable. Thus W ∉ W (p, T), since W is not a maximal subset of T consistent with p. Contradiction. Therefore, if F is valid, p >_{G} q is true over T, and the claim is proved.

Thus the lemma holds for >_{G} and by (1) in Lemma 6.1 also for >_{S}. Since V (p) ⊆ V (T) and q ∈ T, it is by (2) and (5) in Lemma 6.1 further true for > ∈ {>_{B}, >_{W in}, >_{W id}, >_{W eb}}. □

We have not considered the cardinality-based change operator by Forbus yet. Π_{2}^{P} - hardness of CF_{F} does not follow from construction (1) (this would imply by (3) in Lemma 6.1 Π_{2}^{P} -hardness of CF_{D}, which is in Δ_{2}^{P}), but is not difficult to show.

Lemma 6.3 Let T be an atomic knowledge base. To test if p >_{F} q is true over T is Π_{2}^{P} -hard.

Proof: Let F = ∀\underline{x}∃\underline{y}E(\underline{x}, \underline{y}), where \underline{x} =<x_{1}, …, x_{m}>, \underline{y} =<y_{1}, …, y_{n}>. Let z_{1}, …, z_{n} and r be new propositional variables. Define

T = {y_{1}, …, y_{n}, z_{1}, …, z_{n}, r}  (2)
p = [(y_{1} ≡ ¬z_{1}) ∧ … ∧ (y_{n} ≡ ¬z_{n}) ∧ (r ⇒ E(\underline{x}, \underline{y}))]
q = r

This transformation is clearly possible in polynomial time. Notice that every model M ∈ Mod(T) determines a truth assignment ϕ_{M} to \underline{x}, and that every possible truth assignment to \underline{x} is extendible to a model of T. It is not difficult to see that for any model M ∈ Mod(T), it holds that n ≤ |△|_{M}^{min}(p) ≤ n + 1: The truth value of either y_{i} or z_{i} has to be changed to false, and if the resulting assignment to the y_{i} together with ϕ_{M} does not satisfy E(\underline{x}, \underline{y}), just r has to be switched to false to get a model of p. Notice that if the truth value of any x_{i} is changed, then at least n + 1 changes in total are necessary. Thus we conclude that for ϕ_{M} there exists a truth assignment ψ to y_{1}, …, y_{n} such that E(ϕ_{M}(\underline{x}), ψ(\underline{y})) is true iff |△|_{M}^{min}(p) = n iff M′ ⊧ r for all models M′ ∈ Mod(p) with |M△M′| = |△|_{M}^{min}(p). □

We thus get the following result.

Theorem 6.4 Deciding if a counterfactual p > q is true over a knowledge base T is Π_{2}^{P} - complete for > ∈ {>_{G}, >_{W in}, >_{B}, >_{S}, >_{F} }, and Π_{2}^{P} -hardness holds even if T is atomic and q is an atom with q ∈ T.

Proof: By Lemmas 6.2 and 6.3 it remains to show membership in Π_{2}^{P}. We outline how to disprove nondeterministically p > q in polynomial time with a NP oracle, without treatment of special cases (e.g., T, p unsatisfiable).

• >_{G}: Guess T′ ⊆ T. Call for every f ∈ T − T′ the oracle whether T′ ∪ {f, p} is unsatisfiable. Call the oracle to check that T′ ∧ p |̸= q.

• >_{W in}: Guess M ∈ Mod(T) and M′ ∈ Mod(p). Test whether M′ ⊧ ¬q holds. Call the oracle whether there is no M′′ ∈ Mod(p) such that M△M′′ ⊂ M△M′.

• >_{B}: Test by oracle call whether T ∧ p is satisfiable; if this is true, check T ∧ p |̸= q by oracle call, else proceed as for >_{W in}.

• >_{S}: Guess M ∈ Mod(T) and M′ ∈ Mod(p). Test whether M′ ⊧ ¬q holds. Call the oracle whether there exist no M ∈ Mod(T), M′′ ∈ Mod(p) such that M△M′′ ⊂ M△M′.

• >_{F}: Guess M ∈ Mod(T) and M′ ∈ Mod(p). Test whether M′ ⊧ ¬q holds. Call the oracle whether there is no M′′ ∈ Mod(p) such that |M△M′′| < |M△M′|.

□

Note that >_{W id} and >_{W eb} do not appear in Theorem 6.4. In fact, it seems to be difficult to show membership of CF_{W id}, CF_{W eb} in Π_{2}^{P}. An observation supporting this intuition is the complexity of verifying a guess for T ∘_{W id} p or, in case of ∘_{W eb}, Ω(T, p); an easy corollary to Lemma 6.2 is that this problem is Π_{2}^{P} -hard, hence a polynomial time algorithm is impossible even if an NP oracle is provided, unless Π_{2}^{P} = Δ_{2}^{P}. A guess for W ∈ W (p, T) in Ginsberg’s approach or for D ∈ △^{min}(T, p) in Satoh’s approach is, in contrast to this, verifiable in polynomial time with a NP oracle.

Closer inspection yields the – yet not surprising – result that CF_{W id} and CF_{W eb} are computationally equivalent, at least for satisfiable knowledge changes. (Note that this has been shown for literal bases in Lemma 6.1 already.)

Theorem 6.5 Let T = {f_{1}, …, f_{m}} be a satisfiable knowledge base and let p, q be propositional formulae where p is satisfiable. Then, the problem “p >_{W id} q true over T?” is equivalent to “p >_{W eb} q true over T?” under polynomial time transformations.

Proof: To transform CF_{W id} polynomially into CF_{W eb}, we define a knowledge base T′ and a formula p′ as follows. Let s_{1}, …, s_{m} be new propositional variables. Define

T′ = {s_{1}, …, s_{m}}, p′ = p ∧ [(s_{1} ⇒ f_{1}) ∧ ⋯ ∧ (s_{m} ⇒ f_{m})]  (3)

Verify that {s_{i_{1}}, …, s_{i_{l}}} ∈ W (p′, T′) iff {f_{i_{1}}, …, f_{i_{l}}} ∈ W (p, T), for any {i_{1}, …, i_{l}} ⊆ {1, …, m}. Consequently, by (4) in Lemma 6.1 (T′, p′ are satisfiable) we get immediately that p >_{W id} q is true over T iff p′ >_{W id} q is true over T′ iff p′ >_{W eb} q is true over T′.

To transform CF_{W eb} polynomially into CF_{W id}, set X = {x_{1}, …, x_{n}} = V (T) ∩ V (p). Let y_{1}, …, y_{n} and z_{1}, …, z_{n} be new propositional variables. Let T_{1} be the knowledge base obtained by replacing in T each x_{i} by y_{i}, for all i. Define

T′ = {z_{1}, …, z_{n}}, p′ = T_{1} ∧ p ∧ [(z_{1} ⇒ (x_{1} ≡ y_{1})) ∧ ⋯ ∧ (z_{n} ⇒ (x_{n} ≡ y_{n}))].  (4)

As T′ is atomic and satisfiable, and as p′ is satisfiable, by (4) in Lemma 6.1 we immediately obtain that p′ >_{W eb} q is true over T′ iff p′ >_{W id} q is true over T′. Every W ∈ W (p′, T′) corresponds one to one to a D_{W} ∈ △^{min}(T, p) by D_{W} = {x_{i} : z_{i} ∉ W, 1 ≤ i ≤ n}. This implies that x_{i} ∉ Ω(T, p) iff z_{i} ∈ T′ ∘_{W id} p′, for 1 ≤ i ≤ n. One can infer that the models of T′ ∘_{W id} p′ are, restricted to V (T ∧ p ∧ q), equivalent to the models of T ∘_{W eb} p; hence, p >_{W eb} q is true over T iff p′ >_{W id} q is true over T′. □

Deciding whether a formula f ∈ T is not in T ∘_{W id} p is in Σ_{2}^{P}, as well as deciding whether a variable x is in Ω(T, p) (note that x ∈ Ω(T, p) implies x ∈ V (T) ∩ V (p)). Therefore, CF_{W id} and CF_{W eb} are solvable in polynomial time with a Σ_{2}^{P} oracle as follows:

• >_{W id}: First compute T ∘_{W id} p, eliminating from T each formula f ∈ T that does not appear in all W ∈ W (p, T), which is checked with the Σ_{2}^{P} oracle, and add p subsequently. Then, check with the oracle whether T ∘_{W id} p ⊧ q holds.

• p >_{W eb} q: Check whether T or p is unsatisfiable; if so, check T ⊧ q. Otherwise, compute Ω(T, p), checking for each x ∈ V (T) ∩ V (p) with the Σ_{2}^{P} oracle whether x ∈ D for some D ∈ △^{min}(T, p). Then, check with the oracle whether there exist no M ∈ Mod(T), M′ ∈ Mod(p) such that M − Ω(T, p) = M′ − Ω(T, p) and M′ ⊧ ¬q.

By Lemma 6.2, we have thus the following result.

Theorem 6.6 CF_{W id} and CF_{W eb} are equivalent to the Σ_{2}^{P} -complete problems under Turing transformations, and thus have roughly the same complexity as those problems.

In other terms, CF_{W id} and CF_{W eb} are under Turing transformations complete for P^{Σ_{2}^{P}}, which is the class of decision problems solvable in polynomial time with a Σ_{2}^{P} oracle. This characterization does not account for the number of necessary calls to an Σ_{2}^{P} oracle, however. The algorithms from above require about m such calls, where m = |T | and m = |V (T) ∩ V (p)|, respectively. This straightforward upper bound can be improved upon substantially.

Theorem 6.7 Let m be the number of formulas in a knowledge base T (the number of variables in V (T) ∩ V (p) ). Then CF_{W id} (CF_{W eb}) is polynomially decidable with O(log m) calls to an Σ_{2}^{P} oracle.

Proof: The basic idea for such an algorithm is to get certain information about T ∘p that is computable with O(log m) calls to the Σ_{2}^{P} oracle and enables verification of a guess for a model of T ∘ p with a Δ_{2}^{P} algorithm. If this information is available, one oracle call will suffice to decide p > q. In our case, the information is the cardinality of T ∘_{W id} p and the cardinality of Ω(T, p), respectively.

We outline an algorithm for CF_{W id} as claimed, where we assume for sake of simplicity that p ∉ T. |T ∘_{W id} p| is computable by binary search with O(log m) Σ_{2}^{P} oracle calls, since the following problem is in Σ_{2}^{P}: Given T, p and an integer k, is |T ∘_{W id} p| ≤ k? This is true iff at least l = |T | − (k − 1) distinct formulae f_{1}, …, f_{l} are removed from T. This is decidable as follows: Guess f_{1}, …, f_{l} ∈ T and “witnesses” W_{1}, …, W_{l} ⊆ T for the guess of the f_{i}. W_{i} is a witness that f_{i} is removed from T if W_{i} ∈ W (p, T) and f_{i} ∉ W_{i}; this is verifiable in polynomial time with an NP oracle. Thus the whole procedure sketches an Σ_{2}^{P} algorithm for |T ∘_{W id} p| ≤ k?. If |T ∘_{W id} p| is known, call the Σ_{2}^{P} oracle whether there exist f_{1}, …, f_{l} ∈ T, W_{1}, …, W_{l} ⊆ T (l = |T | − (|T ∘_{W id} p| − 1)) and a model M such that the f_{i} are pairwise distinct, W_{i} is a witness that f_{i} is removed from T, and M ⊧ (T − {f_{1}, …, f_{l}}) ∧ p ∧ ¬q. The answer to this call is “no” iff p >_{W id} q is true over T.

An algorithm for CF_{W eb} can be defined in an analogous manner. The case in which T or p is unsatisfiable is treated as above. Concerning the other case, |Ω(T, p)| is computable by binary search with O(log m) calls of a Σ_{2}^{P} oracle, as deciding |Ω(T, p)| ≥ k? is in Σ_{2}^{P}: a guess for sets D_{1}, …, D_{k} ∈ △^{min}(T, p) such that |D_{1} ∪ ⋯ ∪ D_{k}| ≥ k can be verified with a NP oracle in polynomial time. If |Ω(T, p)| is known, check with the Σ_{2}^{P} oracle whether D_{1}, …, D_{|Ω|} ∈ △^{min}(T, p) and M ∈ Mod(T), M′ ∈ Mod(p) exist such that |D| = |Ω(T, p)|, D = D_{1} ∪ ⋯ ∪ D_{|Ω|}, M − D = M′ − D, and M′ ⊧ ¬q holds. The oracle answers “no” iff p >_{W eb} q is true over T. Consequently, p >_{W eb} q is polynomially decidable with O(log m) calls to a Σ_{2}^{P} oracle. □

Recall that P^{Σ_{2}^{P} [O(log n)]} is the class of problems decidable in polynomial time with O(log n) calls to a Σ_{2}^{P} oracle, where n is the input size. Thus we have the following result.

Corollary 6.8 CF_{W id} and CF_{W eb} are in P^{Σ_{2}^{P} [O(log n)]}.

Last but not least we consider Dalal’s operator ∘_{D}, for which we provide the following already announced result.

Theorem 6.9 To decide if p >_{D} q is true over T is P^{NP[O(log n)]}-complete, and P^{NP[O(log n)]}- hardness holds even if T is atomic.

Proof: We show first membership in P^{NP[O(log n)]} and then completeness for this class.

To prove membership in P^{NP[O(log n)]}, we sketch an algorithm that decides p >_{D} q in polynomial time with O(log m) calls to an NP oracle, where m = |V (T) ∩ V (p)|. Check with the oracle whether T or p is unsatisfiable; if so, then p >_{D} q equals p ⊧ q, which is decided by one oracle call. Otherwise, proceed in two steps. First, the distance d = |△|^{min}(T, p) between T and p is determined. Note that d ≤ |V (T) ∩ V (p)| since for M ∈ Mod(T), M′ ∈ Mod(p) such that |M△M′| = d (hence M′ ∈ Mod(T ∘_{D}p)), M△M′ ⊆ V (T) ∩ V (p) must hold. d can be computed by binary search with O(log m) oracle calls (deciding d ≤ k ? for given k is obviously in NP). The second step is to call the oracle whether there exist M ∈ Mod(T), M′ ∈ Mod(p) such that M′ ⊧ ¬q and |M△M′| = d; such M, M′ do not exist iff p >_{D} q is true over T.

For the proof of P^{NP[O(log n)]}-hardness, we refer to the problem UOCSAT: Given a set C = {C_{1}, …, C_{m}} of clauses, decide if all truth assignments that satisfy a maximum number of clauses in C always satisfy the same set of clauses in C. This problem is proved P^{NP[O(log n)]}-complete in [27]. It can be transformed into CF_{D} in polynomial time as follows. Let c_{1}, …, c_{m} be new variables that do not appear in C. Define

T_{1} = {c_{1}, …, c_{m}}, p_{1} = (C_{1} ∨ ¬c_{1}) ∧ ⋯ ∧ (C_{m} ∨ ¬c_{m})  (5)

It is not difficult to see that a model M is in Mod(T_{1} ∘_{D} p_{1}) iff the truth assignment by M to the variables in V (C) satisfies as many clauses in C as simultaneously satisfiable (C_{i} is satisfied by M iff M ⊧ c_{i}). Now let T′_{1} and p′_{1} be the knowledge base resp. formula that results if all of its variables are primed, i.e. T′_{1} = {c′_{1}, …, c′_{m}}, and p′_{1} = (C′_{1} ∨ ¬c′_{1}) ∧ ⋯ ∧ (C′_{m} ∨ ¬c′_{m}). (C′_{i} is the modified clause C_{i}.) Then, T_{1} and T′_{1} resp. p_{1} and p′_{1} are equivalent upon renaming of variables. Define

T = T_{1} ∪ T′_{1}, p = p_{1} ∧ p′_{1}, q = (c_{1} ≡ c′_{1}) ∧ ⋯ ∧ (c_{m} ≡ c′_{m})  (6)

T ∘_{D} p “combines” each model of T_{1} ∘_{D} p_{1} on V (T_{1} ∧ p_{1}) with each model of T′_{1} ∘_{D} p′_{1} on V (T′_{1} ∧ p′_{1}); thus it is easily verified that p >_{D} q is true over T iff all truth assignments that satisfy a maximum number of clauses in C always satisfy the same clauses in C. □

7 Horn formulas

So far, we have considered counterfactuals on arbitrary propositional knowledge bases. Since in this case already the implication problem “T ⊧ p?” is intractable, the complexity increase for implication testing under counterfactual semantics from co-NP-hardness to Π_{2}^{P} -hardness is not drastic. But what if the implication problem is tractable? It is an interesting question if in this case counterfactual semantics does not raise complexity of implication testing considerably such that tractability is preserved.

The most important restriction of this kind is the Horn case, for which the implication problem p ⊧ q for Horn formulae p, q is decidable in O(∥p∥ · ∥q∥) time (this follows easily from the linear time algorithms for Horn satisfiability in [9, 42]). It turns out that the complexity of counterfactuals restricted to the Horn case falls back one level in the polynomial hierarchy under all but cardinality based semantics. Horn counterfactuals are (at least) co-NP-hard under any of the change operations considered, however, and thus this restriction does not gain tractability as it does for the implication problem.

Recall that a (propositional) Horn clause is a disjunction l_{1}∨⋯∨l_{n} of negated atoms and at most one atom (also written as implication v_{1}∧⋯∧v_{n−1} ⇒ v_{n}, where l_{1} = ¬v_{1}, …, l_{n−1} = ¬v_{n−1} and l_{n} = v_{n} for variables v_{1}, …, v_{n}). A Horn formula is a conjunction of Horn clauses, and a we say that a knowledge base is Horn if it is a set of Horn formulas. Note that atomic knowledge bases and literal bases are Horn. The restriction of CF to the case where T is a set of Horn formulas and p, q are Horn formulae is referred to as HORN-CF.

Now here is the basic result on the lower complexity bound of HORN-CF.

Lemma 7.1 Let T be a knowledge base, p and q propositional formulae where T, p, and q are Horn. To decide if p > q is true over T is co-NP-hard for > ∈ {>_{G}, >_{W id},>_{B}, >_{W in}, >_{S}, >_{W eb}}, even if T is a literal base and q ∈ T.

Proof: In the spirit of the principle of Minimal Change, we describe one transformation that works for all change semantics for which co-NP-hardness is claimed.

We transform the problem UNSAT, which is well-known co-NP-complete [16], into HORN-CF for >_{G}. UNSAT is as follows: Given a set C = {C_{1}, …, C_{m}} of clauses, decide if it is impossible to satisfy all clauses in C simultaneously. We assume without loss of generality that no clause C_{i} is empty.

The transformation is as follows. Let V (C) = {x_{1}, …, x_{n}}, and let y_{1}, …, y_{n},z_{1}, …, z_{n}, and s be new variables. Let F [y] denote the formula obtained if in the Boolean formula F all positive occurrences of x_{i} are replaced by ¬y_{i}, for 1 ≤ i ≤ n. Define

T = {x_{1}, y_{1}, …, x_{n}, y_{n}, ¬z_{1}, …, ¬z_{n}, ¬s}  (7)
p = [z_{1} ∧ ⋯ ∧ z_{n} ⇒ s] ⋀_{1≤i≤n}[(¬x_{i} ∨ ¬y_{i}) ∧ (x_{i} ⇒ z_{i}) ∧ (y_{i} ⇒ z_{i})] ∧ ⋀_{1≤j≤m} C_{j}[y]
q = ¬s

(C_{j}[y] is certainly a Horn clause). Note that both T and p are satisfiable (to see the satisfiability of p, set all x_{i}, y_{i} false and s and all z_{i} true).

Let us briefly explain the intuition behind this transformation. The positive occurrences of x_{i} in C are replaced by ¬y_{i} to make the clause set Horn; if the truth value of y_{i} is different from the truth value of x_{i} for all y_{i}, then C is satisfied by this assignment iff C[y] is satisfied. z_{i} indicates if x_{i} and y_{i} have actually different truth values; z_{i} is true in a “possible world” W ∈ W (p, T) exactly if x_{i} ≢ y_{i} is valid in W. If C is satisfiable, there will be a “possible world” W in which all z_{i} are valid, and hence s will be valid in W; otherwise, ¬s will be contained in every “possible world” W.

We claim that p >_{G} q holds in T if and only if C is unsatisfiable.

Assume C is not unsatisfiable, i.e. there is some truth assignment ϕ(x) to x_{1}, …, x_{n} such that C is satisfied. Consider W = {x_{i} : ϕ(x_{i}) = true, 1 ≤ i ≤ n} ∪ {y_{i} : ϕ(x_{i}) = false, 1 ≤ i ≤ n}. It is easily verified that W ∧ p is satisfiable: W ∧ p ⊧ [x_{i} ≡ ¬y_{i}], for 1 ≤ i ≤ n, hence each clause C_{j}[y] is satisfied, 1 ≤ j ≤ m; thus if all z_{i} and s are set true, W ∧ p is satisfied. Moreover, W is maximal consistent with p, as W ∧ p ⊧ z_{1} ∧ ⋯ ∧ z_{n}, and W ∧ p ⊧ s. Thus W ∈ W (p, T). Because W ∧ p |̸= ¬s, it follows that p >_{G} q is false over T.

Conversely, assume that p >_{G} q does not hold, i.e. for some W ∈ W (p, T), we have W ∧ p |̸= ¬s. Since ¬s ∈ T, we infer that W ∧ p ∧ ¬s is unsatisfiable. The only part of p that forces implication of s is z_{1} ∧ ⋯ ∧ z_{n} ⇒ s. Thus we infer that W ∧ p ⊧ z_{1} ∧ ⋯ ∧ z_{n}. Maximality of W with respect to set inclusion entails that either x_{i} or y_{i} must be in W in this case, which implies that W ∧ p ⊧ [x_{i} ≡ ¬y_{i}] for 1 ≤ i ≤ n. Consequently, C is satisfied by the truth assignment ϕ defined by ϕ(x_{i}) = true if x_{i} ∈ W and ϕ(x_{i}) = false if x_{i} ∉ W, 1 ≤ i ≤ n, and hence C is not unsatisfiable.

Thus the transformation is proved correct for >_{G}. For the other change semantics, we notice that T is a satisfiable literal base and that V (p) ⊆ V (T) holds; thus by (1),(2) in Lemma 6.1 the transformation is correct for > ∈ {>_{S}, >_{B}, >_{W in}}, too. Since T is a satisfiable literal base, p is satisfiable, and q ∈ T, by (5) in Lemma 6.1 the transformation works also for > ∈ {>_{W id}, >_{W eb}}. □

Counterfactuals in Horn knowledge bases are by this Lemma co-NP-hard under any of the considered change semantics (except Forbus’s and Dalal’s approach, which go uncovered by this Lemma). We show co-NP-completeness for the following cases.

Theorem 7.2 To decide if a counterfactual p > q is true over a Horn knowledge base T, where p and q are Horn formulae is co-NP-complete for > ∈ {>_{G}, >_{W in}, >_{B}, >_{S}}, even if T is a literal base and q ∈ T.

Proof: By Lemma 7.1 it remains to show membership in co-NP. We sketch how to disprove validity of p > q in T with an NP algorithm, without taking care of the rather trivial special cases for T and p. Recall that implication and satisfiability checking is polynomial for Horn knowledge bases resp. Horn formulae.

• >_{G}: Guess T′ ⊆ T. Check if T′ ∪ {p, f} is unsatisfiable for every f ∈ T − T′. Check if T′ ∧ p |̸= q.

• >_{W in}: Guess M ∈ Mod(T) and M′ ∈ Mod(p). Test whether M′ ⊧ ¬q holds. Let for every variable z, t(z) = z if M ⊧ z and t(z) = ¬z if M |̸= z, and let D = M△M′. Check if for each x ∈ D, the following Horn formula is unsatisfiable:

p ∧ t(x) ∧ ⋀_{y∈V (T)−D} t(y).

• >_{B} If T ∧ p is satisfiable, then check T ∧ p |̸= q, else proceed as for >_{W in}.

• >_{S}: Guess M ∈ Mod(T) and M′ ∈ Mod(p). Check whether M′ ⊧ ¬q holds. Let D = M△M′ and V (T ∧ p) = {x_{1}, …, x_{n}}. Substitute y_{i} for x_{i} in p for all x_{i}, where the y_{i} are new variables that appear nowhere else, and let p[y] denote the resulting formula. Test for each x_{j} ∈ D ∩ V (T ∧ p) whether the following Horn formula is unsatisfiable:

T ∧ p[y] ∧ (x_{j} ⇒ y_{j}) ∧ (y_{j} ⇒ x_{j}) ∧ ⋀_{x_{i}∈V (T ∧p)−D}[(x_{i} ⇒ y_{i}) ∧ (y_{i} ⇒ x_{i})].

□

Similar to the issue whether CF_{W id} and CF_{W eb} are in Π_{2}^{P} for arbitrary knowledge bases and formulae, it is not clear if HORN-CF_{W id} and HORN-CF_{W eb} are in co-NP. The computational equivalence of these problems under polynomial transformations follows easily from constructions (3) and (4) in the proof of Theorem 6.5 (note that [z_{i} ⇒ (x_{i} ≡ y_{i})] is logically equivalent to [(z_{i} ∧ x_{i} ⇒ y_{i}) ∧ (z_{i} ∧ y_{i} ⇒ x_{i})], hence p′ can be replaced by an equivalent Horn formula, and that satisfiability of T, p is polynomially decidable, thus special cases make no troubles). Moreover, one can show that both problems are solvable with logarithmically many calls to an NP oracle: Analogous to the algorithms sketched in the proof of Theorem 6.7, first the number of formulas of T ∘_{W id} p resp. Ω(T, p) is computed, which takes O(log m) oracle calls, where m is the cardinality of T resp. the number of variables in V (T) ∩ V (p), and then one final oracle call decides p > q. These algorithms settle both problems in P^{NP[O(log n)]}.

It remains to consider cardinality based change semantics. Horn counterfactuals have the same complexity as counterfactuals in arbitrary knowledge bases under Forbus’s or Dalal’s change operation. We show by proper modification of the transformations in the proofs of Lemma 6.3 and Theorem 6.9 that Π_{2}^{P} -hardness resp. P^{NP[O(log n)]}-hardness still stands under this restriction.

For the sake of intelligibility and readability, we introduce a notational shorthand for a formula that fixes equivalence of variables. Let Y = {y_{1}, …, y_{n}} be a set of variables. We denote by EQ(Y) the formula (y_{1} ⇒ y_{2}) ∧ ⋯ ∧ (y_{n−1} ⇒ y_{n}) ∧ (y_{n} ⇒ y_{1}). Note that EQ(Y) is Horn.

Let us turn our attention to Forbus’s approach first.

Theorem 7.3 HORN-CF under Forbus’s change semantics is Π_{2}^{P} -complete, and Π_{2}^{P} - hardness holds even if T is a literal base.

Proof: Recall that in the proof of Lemma 6.3 we constructed T = {y_{1}, z_{1}, …, y_{n}, z_{n}, r}, p = [(y_{1} ≡ ¬z_{1})∧⋯∧(y_{n} ≡ ¬z_{n})∧(r ⇒ E(\underline{x}, \underline{y}))] and q = r for formula F = ∀\underline{x}∃\underline{y}E(\underline{x}, \underline{y}) where \underline{x} =<x_{1}, …, x_{m}>, \underline{y} =<y_{1}, …, y_{n}>, such that p >_{F} q is true over T iff F is true. Without loss of generality we may assume that E(\underline{x}, \underline{y}) = C_{1} ∧ ⋯ ∧ C_{l} is a conjunction of clauses C_{1}, …, C_{l} [54].

Let s_{y_{1}}, s_{z_{1}}, …, s_{y_{n}}, s_{z_{n}} be additional variables not contained in V (T ∧ p ∧ q). Define

T_{1} = {r, x_{1}, …, x_{m}, y_{1}, s_{y_{1}}, z_{1}, s_{z_{1}}, …, y_{n}, s_{y_{n}}, z_{n}, s_{z_{n}}}
p_{1} = ⋀_{1≤i≤n}[(¬y_{i} ∨ ¬z_{i}) ∧ EQ({y_{i}, s_{y_{i}}}) ∧ EQ({z_{i}, s_{z_{i}}})] ∧ ⋀_{1≤j≤n}(C_{j}[z] ∨ ¬r)

where C_{j}[z] denotes the clause obtained from C_{j} replacing every positive y_{i} by ¬z_{i}, for all i. Note that this transformation is obviously computable in polynomial time.

Consider any model M ∈ Mod(T_{1}). Let ϕ be the truth assignment to \underline{x} in M. The distance of M to p_{1} satisfies the following relation: 2n ≤ |△|^{min}(M, p_{1}) ≤ 2n + 1. To verify this, the lower bound is reached if and only if there exists a truth assignment ψ to \underline{y} such that E(ϕ(\underline{x}), ψ(\underline{y})) is true (in this case, merely one of y_{i}, z_{i} and the corresponding s_{y_{i}} resp. s_{z_{i}} must switch to false to get a model of p_{1}). The upper bound follows from the observation that any model fixing ϕ and satisfying ¬r and (¬y_{i} ∨ ¬z_{i}) ∧ EQ({y_{i}, s_{y_{i}}}) ∧ EQ({z_{i}, s_{z_{i}}}) is a model of p_{1}. This entails that no more than 2n + 1 truth values have to be switched in M to get a model of p_{1}.

As a consequence, p_{1} >_{F} q is false over T_{1} iff there is some model in Mod(T_{1}∘_{F} p_{1}) in which r is false iff |△|_{M}^{min}(p_{1}) = 2n + 1 for some M ∈ Mod(T_{1}), which means that E(ϕ(\underline{x}), \underline{y}) is unsatisfiable, i.e. F is false. □

Introducing redundant variables is also appropriate for a proof that the lower complexity bound for CF under Dalal’s change semantics remains unchanged in the Horn case.

Theorem 7.4 HORN-CF under Dalal’s change semantics is P^{NP[O(log n)]}-complete, and P^{NP[O(log n)]}-hardness holds even if T is a literal base.

Proof: By Theorem 6.9 we only need to show hardness for this class. Recall that in the proof of Theorem 6.9, the problem UOCSAT for clause set C = {C_{1}, …, C_{m}} is transformed into evaluation of the counterfactual p >_{D} q in a knowledge base T defined in (6), (5) by T = T_{1} ∪ T′_{1}, p = p_{1} ∧ p′_{1} and q = (c_{1} ≡ c′_{1}) ∧ ⋯ ∧ (c_{m} ≡ c′_{m}), where T_{1} = {c_{1}, …, c_{m}}, p_{1} = (C_{1} ∨ ¬c_{1}) ∧ ⋯ ∧ (C_{m} ∨ ¬c_{m}), and T′_{1}, p′_{1} are the “primed versions” of T and p, respectively.

Let V (C) = X = {x_{1}, …, x_{n}}, and let Y = {y_{1}, …, y_{n}}, Z_{x_{1}}, Z_{y_{1}}, …, Z_{x_{n}}, Z_{y_{n}} be pairwise disjoint sets of additional new propositional variables that do not occur elsewhere such that |Z_{x,i}| = |Z_{y,i}| = m. We define

T_{2} = X ∪ Y ∪ {c_{1}, …, c_{m}} ∪ Z_{x_{1}} ∪ Z_{y_{1}} ∪ ⋯ ∪ Z_{x_{n}} ∪ Z_{y_{n}}
p_{2} = ⋀_{1≤i≤n}[(¬x_{i} ∨ ¬y_{i}) ∧ EQ(Z_{x_{i}} ∪{x_{i}}) ∧ EQ(Z_{y_{i}} ∪{y_{i}})] ∧ ⋀_{1≤j≤m}(C_{j}[y] ∨ ¬c_{j}),

where C_{j}[y] denotes the clause C_{j} with each positive occurrence of x_{i} replaced by ¬y_{i}, for all i. This transformation is clearly computable in polynomial time.

It is obvious that every model of T_{2} ∘_{D} p_{2} satisfying x_{i} ≡ ¬y_{i} for all i is also a model of T_{1} ∘ p_{1}. The formulae EQ(Z_{x_{i}} ∪ {x_{i}}), EQ(Z_{y_{i}} ∪ {y_{i}}) make sure that x_{i} ≡ ¬y_{i} must be true in any model of T_{2} ∘ p_{2}, however: If for some i both x_{i} and y_{i} have value false in model M ∈ Mod(p_{2}), then |△|_{M}^{min}(T_{2}) ≥ (n − 1)(m + 1) + 2(m + 1). But any model M′ satisfying ¬c_{1} ∧ ⋯ ∧ ¬c_{m} and (x_{i} ≡ ¬y_{i}) ∧ EQ(Z_{x_{i}} ∪ {x_{i}}) ∧ EQ(Z_{y_{i}} ∪ {y_{i}}) for all i is a model of p_{2} such that |△|_{M′}^{min}(T_{2}) = n(m+1)+m < |△|_{M}^{min}(T_{2}), hence M ∉ Mod(T_{2}∘_{D} p_{2}). On the other hand, every model of T_{1} ∘_{D} p_{1} that satisfies x_{i} ≡ ¬y_{i} and EQ(Z_{x_{i}} ∪ {x_{i}}), EQ(Z_{y_{i}} ∪ {y_{i}}) for all i, is a model of T_{2} ∘_{D} p_{2}.

Since none of the variables c′_{1}, …, c′_{m} appears in V (T_{1} ∧ p_{1}), V (T_{2} ∧ p_{2}), it follows that Mod(T_{1} ∘_{D} p_{1}) and Mod(T_{2} ∘_{D} p_{2}) are identical under restriction to the variables in the set V (T_{1} ∧ p_{1} ∧ q).

Now let T′_{2} and p′_{2} be the “primed versions” of T_{2} and p_{2}, and define T^{∗} = T_{2} ∪ T′_{2}, p^{∗} = p_{2} ∧ p′_{2}. It is not difficult to verify that restricted to V (T ∧ p ∧ q), Mod(T^{∗} ∘_{D} p^{∗}) and Mod(T ∘_{D} p) are identical; it follows that p >_{D} q is true over T iff and p^{∗} >_{D} q is true over T^{∗}. Since q = (c_{1} ≡ c′_{1}) ∧ ⋯ ∧ (c_{m} ≡ c′_{m}) can be efficiently rewritten as a Horn formula, this completes the proof. □

8 Bounding the knowledge change

Lemma 6.2 is a strong result on the lower complexity bound of CF, because it states that evaluating p > q in T is Π_{2}^{P} -hard even in the case in which the knowledge base T and q are very “elementary”. The complexity is entirely introduced by the formula p describing the knowledge change. Therefore it is near at hand to investigate into cases in which the knowledge change meets constraints.

A reasonable constraint of this kind is to assume that that p involves only a small number of facts. This can be modeled by a constant upper bound for the length ∥p∥ of p, cf. [58].

Bounding the knowledge change to a small number of facts yields lower complexity for counterfactual evaluation, at least under model-based change. Nevertheless, this problem remains intractable under all change semantics considered. The following theorem is easily obtained from results in [58].

Theorem 8.1 Let T be a knowledge base and let p, q be propositional formulae where ∥p∥ ≤ k for a constant k. To decide if p > q is true over T is co-NP-complete for > ∈ {>_{W in}, >_{F} } and is NP-hard as well as co-NP-hard, but solvable with a constant number of calls to an NP oracle for > ∈ {>_{B}, >_{S}, >_{D}, >_{W eb}} (two oracle calls for >_{B}).

Proof: co-NP-hardness for all these change semantics is easy: Any set C of clauses is unsatisfiable iff x > ¬C is true over T = {}, where x ∉ V (C).

Winslett presents in [58] algorithms that compute T ∘p in time O(log t) if ∥p∥ is bounded by a constant, where t is the number of occurrences of variables in T for ∘ ∈ {∘_{W in}, ∘_{F} }. Thus membership of CF_{W in}, CF_{F} in co-NP for ∥p∥ ≤ k is obvious; hence co-NP-completeness is proved.

Obviously, p >_{B} q is decidable with two calls to an NP oracle if ∥p∥ ≤ k, as p >_{W in} q is in co-NP in this case. Unless NP = co-NP, to decide p >_{B} q is neither in NP nor in co-NP, however, as this is both co-NP-hard and NP-hard. NP-hardness for >_{B} and >_{S}, >_{D}, >_{W eb} is easily shown exploiting the fact that for ∘ ∈ {>_{B}, >_{S}, >_{D}, >_{W eb}}, the satisfiability of T ∘p implies that T ∘p ≡ T ∧p (this follows immediately from the properties of these change operators with respect to the revision postulates in Section 3.2.1). Thus if C is a set of clauses that is without loss of generality falsifiable, x > C is true over T = {x ≡ C} iff C is satisfiable, where x ∉ V (C) (if C is unsatisfiable, then T ∘ x ≡ x, otherwise T ∘ x ≡ x ∧ C for ∘ ∈ {>_{B}, >_{S}, >_{D}, >_{W eb}}).

The upper complexity bound for the operators >_{S}, >_{D}, >_{W eb} follows from the observation that △^{min}(T, p) is computable with a constant number of NP oracle calls if ∥p∥ ≤ k, cf. [58]. (The constant depends on |V (p)|.) Once △^{min}(T, p) is known, a formula for T ∘ p is easily constructed in polynomial time for ∘ ∈ {∘_{S}, ∘_{D}, ∘_{W eb}}, and then p > q is decidable with one NP oracle call. □

Under formula-based changes, however, the lower complexity bound of unrestricted CF still stands for small knowledge change.

Theorem 8.2 It is Π_{2}^{P} -complete for >_{G} and Π_{2}^{P} -hard for >_{W id} to decide if p > q is true over a complete knowledge base T, and Π_{2}^{P} -hardness holds in both cases even if q ∈ T and p, q are atoms.

Proof: Let s be a new propositional variable. Define T′, p′, q′ from T, p, q in (1) by T′ = T ∪ {¬s, ¬s ∨ p}, p′ = s, q = r. It is immediately verified that T is complete for variable set V = T ∪ {s} and that p′ >_{G} q′ is true over T′ iff p >_{G} q is true over T. Thus by (5) in Lemma 6.1 for T′, p′, q′ it follows that p′ >_{G} q′ iff ¬r ∈ T′ ∘_{W id} p′ iff p′ >_{W id} q′. □

We note that by this theorem the open problem in [58, p.33], if it is Σ_{2}^{P} -complete to decide if WIDTIO change removes a formula from the knowledge base, where the length of the change formula p is bounded by a constant, is immediately answered positively (a proof of membership in Σ_{2}^{P} is already sketched by Winslett). We remark that Nebel’s proof of Π_{2}^{P} -hardness of p >_{G} q in [45] also would solve the hardness part of this problem, provided that the knowledge base T is allowed to be unsatisfiable.

A positive result

In view of all the negative results from above on tractability of propositional counterfactuals, the question arises which restrictions make the problem tractable. A straightforward trial is to combine the Horn constraint and small knowledge change; this yields tractability for counterfactual evaluation, indeed, but merely for model-based change semantics.

Theorem 8.3 Let T be a set of Horn formulas and let p, q be Horn formulas, where ∥p∥ ≤ k for k a constant. Deciding the validity of p > q over T is possible in O(∥T ∥·∥q∥) time for > ∈ {>_{D}, >_{F} , >_{B}, >_{W in}, >_{S}, >_{W eb}}.

Proof: Denote by M(T) and M(p) the models of T and p on the variables V (p). For ∘_{W in} and ∘_{S}, changes of models of T to models of p are restricted to V (p), and the change of M ∈ Mod(T) is determined by M ∩V (p), which is in M(T). The key observation is that under the constraint ∥p∥ ≤ k, |M(p)| as well as |M(T)| is bounded by the constant 2^{k}, and M(p), M(T) can be computed in O(∥T ∥) time (using the linear algorithms in [9, 42], for instance). As an immediate consequence, △_{M}^{min}(p) for every M ∈ Mod(T) as well as △^{min}(T, p) is also computable in O(∥T ∥) time (note that |△_{M}^{min}(p)|,|△^{min}(T, p)| < 2^{k}).

T ∘_{S} p is representable as a disjunction D = D_{1} ∨ ⋯ ∨ D_{l} of Horn formulas, which is efficiently constructible in from T, p, △^{min}(T, p) in time linear in the size of T follows. Let for M ∈ M(p), t_{M} : V (p) → {v, ¬v : v ∈ V (p)} be defined by t_{M}(v) = v if M ⊧ v and t_{M}(v) = ¬v if M |̸= v. For all M ∈ M(T), M′ ∈ M(p) such that M△M′ ∈ △^{min}(T, p), set up a disjunct D^{M,M′} = T [M] ∧ ⋀_{v∈V (p)} t_{M′}(v), where T [M] is a Horn formula obtained from T as follows: First, for each variable v in V (p) all occurrences of v in T are replaced by the truth value of v in M, and then the formula resulting from this step is simplified by removing false literals and clauses with true literals such that a Horn formula is obtained. This is certainly possible in O(∥T ∥) time, and hence D^{M,M′} is constructible in O(∥T ∥) time. The number of disjuncts D^{M,M′} is trivially bounded by the constant 2^{2k}, thus D can be constructed in O(∥T ∥) time. Given D, p >_{S} q is false over T iff there is some disjunct D_{i} in D such that D_{i} |̸= q; Since l is bounded by the constant 2^{2k}, and since D_{i} is Horn and ∥D_{i}∥ ≤ ∥T ∥ + k, this can be checked in O(∥T ∥·∥q∥) time. Consequently, p >_{S} q is evaluable over T in O(∥T ∥·∥q∥) time.

For ∘_{W in}, note that if M, M′ ∈ Mod(T) such that M ∩V (p) = M′ ∩V (p), then △_{M}^{min}(p) = △_{M′}^{min}(p). Thus as for T ∘_{S} p, a disjunction D = D_{1} ∨ ⋯ ∨ D_{l}, l ≤ 2^{2k}, of Horn formulas D_{i} that represents T ∘_{W in} p can be constructed in O(∥T ∥) time, setting up for each M ∈ M(T) and all M′ ∈ M(p) such that M△M′ ∈ △_{M}^{min}(p) a disjunct D^{M,M′} in D. Therefore, evaluation of p >_{W in} q over T is possible in O(∥T ∥·∥q∥) time; it is immediately verified that the same holds for p >_{B} q, too.

For ∘_{D}, if T is unsatisfiable, then p >_{D} q is equivalent to p ⊧ q; if T is satisfiable, then △^{min}(T, p) just has to be “pruned” to {S ∈ △^{min}(T, p) : |S| = |△|^{min}(T, p)}, which can be done in constant time, and then the same procedure as for ∘_{S} applies. Thus p >_{D} q can be evaluated over T in O(∥T ∥·∥q∥) time (satisfiability of T and p ⊧ q is checkable in O(∥T ∥), O(∥q∥) time, respectively).

Similarly, for ∘_{F} only △_{M}^{min}(p) has to be “pruned” to {S ∈ △_{M}^{min}(p) : |S| = |△|_{M}^{min}(p)}, and then one can proceed as in case of >_{W in}. Thus, O(∥T ∥·∥q∥) time complexity for evaluating p >_{F} q over T follows.

Last but not least, Weber’s set Ω(T, p) is immediately obtained from △^{min}(T, p), and since Ω(T, p) ⊆ V (p), |Ω(T, p)| is bounded by the constant k; Hence, res_{Ω}(T) = D_{1} ∨ ⋯ ∨ D_{l} where l ≤ 2^{k} and each D_{i} can be transformed in O(∥T ∥) time into a Horn formula. Consequently, res_{Ω}(T)∧p ⊧ q is decidable in O((∥T ∥+∥p∥)∥q∥) time, hence in O(∥T ∥·∥q∥) time. From this, O(∥T ∥·∥q∥) time for evaluating p >_{W eb} q over T is straightforward. □

Note that by the proof of Theorem 8.3 it is immediately clear that p needs not necessarily be Horn; the theorem still holds for arbitrary formulas p if ∥p∥ is bounded by a constant. Furthermore, the bound ∥p∥ ≤ k can be relaxed to an O(log(∥T ∥ + ∥p∥ + ∥q∥)) bound on |V (p)| and we still stay polynomial, since in this case |M(T)| and |M(p)| are bounded by a polynomial in the input size and M(T), M(p) etc. are computable in polynomial time.

In contrast to Theorem 8.3, bounding the length of p by a constant does not lower worst case complexity for formula-based change.

Theorem 8.4 Let T be a knowledge base of Horn formulas, and let p, q be Horn formulas where ∥p∥ ≤ k for some constant k. To decide if p > q is true over T is co-NP-complete for >_{G} and co-NP-hard for >_{W id}. co-NP-hardness holds in both cases even if q ∈ T and p, q are literals.

Proof: A slight modification of the construction (7) in Lemma 7.1 will show this. Let t be a new variable, and let p_{t} be the formula obtained from p adding ¬t to each clause of p. Define T′, p′, q′ from T, p, q by T′ = T ∪ {p_{t}}, p′ = t, q′ = ¬s. Then p >_{G} q is true over T iff p′ >_{G} q′ is true over T′, which holds iff p′ >_{W id} q′ is true over T′ iff q′ ∈ T′ ∘_{W id} p′ by (5) in Lemma 6.1; hence we are done. □

This result can be sharpened to the case in which T is a set of Horn clauses rather than Horn formulas, at least for Ginsberg’s notion of change.

Theorem 8.5 Let T be a set of Horn clauses, and let p, q be literals. To decide if p >_{G} q is true over T is co-NP-hard.

Proof: We transform UNSAT into this problem (rf. to the proof of Lemma 7.1 for UNSAT). Let C = {C_{1}, …, C_{m}} be a set of clauses, where V (C) = {x_{1}, …, x_{n}}. Let y_{1}, …, y_{n}, u, f be new variables and define

T_{f} = {x_{1} ∧ y_{1} ⇒f, …, x_{n} ∧ y_{n} ⇒f, C_{1}[y]∨f, …, C_{m}[y]∨f},

where C_{j}[y] is the clause obtained from C_{j} replacing each positive occurrence of x_{i} by ¬y_{i}, for all i. Note that T_{f} is a set of Horn clauses that is satisfied if f is set true. Then, define

T = T_{f} ∪ {x_{1}, y_{1}, …, x_{n}, y_{n}, x_{1} ∧ y_{1} ⇒ u, …, x_{n} ∧ y_{n} ⇒ u},  (8)
p = ¬u,
q = f.

Since f occurs within in T only in formulas of T_{f}, it is obvious that for every W ∈ W (p, T) it holds that T_{f} ⊆ W and that for all 1 ≤ i ≤ n, exactly two of x_{i}, y_{i}, and x_{i} ∧ y_{i} ⇒ u are in W. Hence it is easily verified that p >_{G} q is false over T, i.e. there is some W ∈ W (p, T) such that W ∧ p ∧ ¬f is satisfiable, if and only if C is satisfied by some truth assignment ϕ to x_{1}, …, x_{n}. □

Finally, we remark that transformation (8) does not work to show co-NP-hardness of CF under WIDTIO change (note that T ⊧ f, but f ∉ T). It is an interesting open question whether HORN-CF_{W id} remains intractable if the length of p is bounded, especially since this problem goes hand in hand with efficient computation of T ∘_{W id} p.

9 Conclusion

We have considered the computational cost of inferencing a formula q from a propositional knowledge base T that has to be updated or revised with a formula p before, according to a minimal change approach; this problem amounts to the evaluation of the counterfactual p > q over T under the respective change semantics.

The main finding was that evaluating a counterfactual is for almost all proposed change operators at the second level of the polynomial hierarchy, and in many cases complete for the class Π_{2}^{P}; roughly speaking, this is due to two different sources of complexity, namely propositional inference and the number of choices to make T consistent with p under minimal change. The complexity results give strong evidence that it is for most approaches unrealistic to expect a polynomial algorithm for evaluating counterfactuals under the respective semantics, even if an algorithm can solve arbitrarily many NPcomplete problems (e.g., calls to a theorem prover for classical propositional logic) without cost.

We also have considered counterfactuals under the two restrictions of Horn formulas, i.e. all formulas are conjunctions of Horn clauses, and bounded knowledge change, i.e. the case where the change is described by a formula with size bounded by a constant. Note that inference in classical propositional logic is tractable for Horn formulas. These restrictions have different effects on the complexity of counterfactuals according to the underlying change operators. Most noticeably, we found tractability of evaluating counterfactuals only if both restrictions are imposed simultaneously, and only for model-based change operators, but not for formula-based change methods. Counterfactuals are still intractable if only one of the restrictions applies.

Comparing counterfactuals to other common formalisms of nonmonotonic reasoning such as circumscription, default logic, abduction, and truth maintenance systems, we found similar complexity results. Two conclusions from all these complexity results may be drawn. Firstly, nonmonotonic propositional reasoning seems to be inherently harder than classical propositional logic from the computational point of view. Secondly, all of the major formalisms of nonmontonic reasoning are roughly of the same difficulty, and reasoning tasks can be polynomially transformed from one formalism to most of the other formalisms. As a practical consequence, existing algorithms or theorem provers for the one approach can be fruitfully applied to the other.

It remains for the future to find ways for efficient processing of propositional nonmonotonic reasoning. An important issue therefor are suitable restrictions for the various formalisms that eliminate all sources of intractability; a lot work has to be done in that direction.

References

[1] C. Alchourrón, P. Gärdenfors, and D. Makinson. On the Logic of Theory Change: Partial Meet Contraction and Revision Functions. Journal of Symbolic Logic, 50:510– 530, 1985.

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

[3] A. Borgida. Language Features for Flexible Handling of Exceptions in Information Systems. ACM Trans. on Database Syst., 10:563–603, 1985.

[4] G. Bossu and P. Siegel. Saturation, Nonmonotonic Reasoning and the Closed World Assumption. Artificial Intelligence, 25:13–63, 1985.

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

[6] M. Dalal. Investigations into a Theory of Knowledge Base Revision: Preliminary Report. In Proceedings AAAI-88, pages 475–479, 1988.

[7] M. Dalal. Updates in Propositional Databases. Technical Report DCS-TR-222, Rutgers University, Dept. of Computer Science, Feb. 1988.

[8] J. de Kleer. An Assumption-Based Truth Maintenance System. Artificial Intelligence, 28:127–162, 1986.

[9] W. Dowling and J. H. Gallier. Linear-time Algorithms for Testing the Satisfiability of Propositional Horn Theories. Journal of Logic Programming, 1(3):267–284, 1984.

[10] T. Eiter and G. Gottlob. Propositional Circumscription and Extended Closed World Reasoning are Π_{2}^{P} -complete. Technical Report CD-TR 91/20, Christian Doppler Laboratory for Expert Systems, Vienna University of Technology, Austria, May 1991. To appear in Theoretical Computer Science.

[11] T. Eiter and G. Gottlob. Higher Level Complexity Results for Abduction. Technical Report CD-TR 92/35, Christian Doppler Laboratory for Expert Systems, TU Vienna, March 1992.

[12] R. Fagin, G. Kuper, J. Ullman, and M. Y. Vardi. Updating Logical Databases. In P. Kanellakis and F. Preparata, editors, Advances in Computing Research, volume 3. JAI Press, 1986.

[13] R. Fagin, J. D. Ullman, and M. Y. Vardi. On the Semantics of Updates in Databases. In Proceedings PODS-83, pages 352–365, 1983.

[14] K. D. Forbus. Introducing Actions into Qualitative Simulation. In Proceedings IJCAI-89, pages 1273–1278, 1989.

[15] P. Gärdenfors. Knowledge in Flux. Bradford Books, MIT Press, 1988.

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

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

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

[19] M. L. Ginsberg. Counterfactuals. Artificial Intelligence, 30:35–79, 1986.

[20] M. L. Ginsberg. A Circumscriptive Theorem Prover. Artificial Intelligence, 39:209– 230, 1989.

[21] M. L. Ginsberg and D. E. Smith. Reasoning About Action I: A Possible Worlds Approach. In F. Brown, editor, Proc. Workshop “The Frame Problem in Artificial Intelligence”, pages 233–258. Morgan Kaufmann Publ., 1987. also in Artificial Intelligence, 35(165–195), 1988.

[22] G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2:3, June 1992.

[23] G. Grahne. Updates and Counterfactuals. In Proceedings KR-91, pages 269–276, 1991.

[24] G. Grahne and A. O. Mendelzon. Updates and Subjunctive Queries. Technical Report KRR-TR-91-4, University of Toronto, CS Dept., July 1991. Also Proceedings Workshop on Nonstandard Queries and Answers, Toulouse, July 1-3, 1991, pp. 33-52.

[25] J. Hartmanis. New Developments in Structural Complexity Theory. Theoretical Computer Science, 71:79–93, 1990.

[26] 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.

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

[28] H. Katsuno and A. O. Mendelzon. A Unified View of Propositional Knowledge Base Updates. In Proceedings IJCAI-89, pages 1413–1419, 1989.

[29] H. Katsuno and A. O. Mendelzon. On the Difference Between Updating a Knowledge Base and Revising it. Technical Report KRR-TR-90-6, University of Toronto, CS Dept., August 1990.

[30] H. Katsuno and A. O. Mendelzon. On the Difference between Updating a Knowledge Base and Revising it. In Proceedings KR-91, pages 387 – 395, 1991.

[31] H. Katsuno and A. O. Mendelzon. Propositional Knowledge Base Revision and Minimal Change. Artificial Intelligence, 52:253–294, 1991.

[32] A. Keller and M. Winslett-Wilkinson. On the Use of an Extended Relational Model to Handle Changing Incomplete Information. IEEE Transactions on Software Engineering, SE:11(7):620–633, 1985.

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

[34] D. Lewis. Counterfactuals. Harvard University Press, Cambridge, MA, 1973.

[35] V. Lifschitz. Closed-World Databases and Circumscription. Artificial Intelligence, 27:229–235, 1985.

[36] W. Marek and M. Truszczyńsky. Modal logic for default reasoning. Annals of Mathematics and Artificial Intelligence, 1:275–302, 1990.

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

[38] J. McCarthy. Applications of Circumscription to Formalizing Common-Sense Knowledge. Artificial Intelligence, 28:89–116, 1986.

[39] D. McDermott. Non-Monotonic Logic II: Nonmonotonic Modal Theories. Journal of the ACM, 29:33–57, 1982.

[40] D. McDermott and J. Doyle. Non-Monotonic Logic I. Artificial Intelligence, 13:41–72, 1980.

[41] 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.

[42] M. Minoux. LTUR: a simplified linear time unit resolution for Horn formulae and computer implementation. Information Processing Letters, 29:1–12, 1988.

[43] R. Moore. Semantical Considerations on Nonmonotonic Logics. Artificial Intelligence, 25:75–94, 1985.

[44] B. Nebel. A Knowledge Level Analysis of Belief Revision. In Proceedings KR-89, pages 301–311, 1989.

[45] B. Nebel. Belief Revision and Default Reasoning: Syntax-Based Approaches. In Proceedings KR-91, pages 417–428, 1991.

[46] 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.

[47] T. Przymusinski. An Algorithm to Compute Circumscription. Artificial Intelligence, 38:49–73, 1989.

[48] 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.

[49] R. Reiter. A Logic for Default Reasoning. Artificial Intelligence, 13:81–132, 1980.

[50] N. Rescher. Hypothetical Reasoning. North-Holland, Amsterdam, 1964.

[51] N. Rescher. The Coherence Theory of Truth. Oxford University Press, 1973.

[52] V. Rutenburg. Complexity Classification in Truth Maintenance Systems. In Proceedings STACS-91, number 480 in Lecture Notes in Computer Science, pages 373–383, 1991.

[53] K. Satoh. Nonmonotonic Reasoning by Minimal Belief Revision. In Proceedings of the International Conference on Fifth Generation Computer Systems, pages 455–462, 1988.

[54] 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.

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

[56] A. Weber. Updating Propositional Formulas. In Proceedings of the First Conference on Expert Database Systems, pages 487–500, 1986.

[57] M. Winslett. Reasoning about Action Using a Possible Models Approach. In Proceedings AAAI-88, pages 89–93, 1988.

[58] M. Winslett. Updating Logical Databases. Cambridge University Press, 1990.

[59] M. Winslett. Circumscriptive Semantics for Updating Databases. Annals of Mathematics and Artificial Intelligence, 3:429–450, 1991.

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