The Complexity of Logic-Based Abduction

Thomas Eiter, Georg Gottlob

Christian Doppler Labor für Expertensyteme Technische Universität Wien Paniglgasse 16, 1040 Wien

{eiter,gottlob}@vexpert.dbai.tuwien.ac.at

October 4, 1993

CD-TR 92/35, final version.

To appear in Journal of the ACM.

To appear in Journal of the ACM.

The Complexity of Logic-Based Abduction^{∗}

Thomas Eiter and Georg Gottlob

Christian Doppler Laboratory for Expert Systems

Institut für Informationssysteme

Technische Universität Wien

Paniglgasse 16, A-1040 Wien, Austria

        e-mail: (eiter,gottlob)@vexpert.dbai.tuwien.ac.at

Abstract

Abduction is an important form of nonmonotonic reasoning allowing one to find explanations for certain symptoms or manifestations. When the application domain is described by a logical theory, we speak about logic-based abduction. Candidates for abductive explanations are usually subjected to minimality criteria such as subsetminimality, minimal cardinality, minimal weight, or minimality under prioritization of individual hypotheses. This paper presents a comprehensive complexity analysis of relevant decision and search problems related to abduction on propositional theories. Our results indicate that abduction is harder than deduction. In particular, we show that with the most basic forms of abduction the relevant decision problems are complete for complexity classes at the second level of the polynomial hierarchy, while the use of prioritization raises the complexity to the third level in certain cases.

Categories and Subject Descriptors: I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods; F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic

General Terms: Theory

Additional Key Words and Phrases: Abduction, Complexity Analysis, Diagnosis, Reasoning, Propositional Logic.

∗An extended abstract of this paper appeared in the Proceedings of the Tenth Symposium on Theoretical Aspects of Computing (STACS), February 1993, Würzburg, Germany, P. Enjalbert, A. Finkel, K.W. Wagner eds, pp. 70-79, Springer LNCS 665, 1993.

1 Introduction

This paper is on the computational complexity of abduction, a method of reasoning extensively studied by C.S. Peirce [58, 33]. Abduction has taken on fundamental importance in Artificial Intelligence and related disciplines. Abductive reasoning is used to generate explanations for observed symptoms and manifestations. Abduction appears to be a powerful concept underlying commonsense reasoning. The importance of abduction to Artificial Intelligence was first emphasized by Morgan [52] and Pople [64]. One important application field within AI is diagnosis. As pointed out by Peng and Reggia [59] and by others, there is a wide consensus that humans typically use abduction in the diagnosis process. Furthermore, diagnosis is one of the most representative and best understood application domains for abductive reasoning, maybe because the diagnostic process is more amenable to being logically formalized than many other problem-solving tasks. Several abduction-based diagnostic expert systems have been built and were successfully applied, mainly in the medical domain [59, 36]. Regarding specifically logic-based abduction, THEORIST by Poole [62] is a framework for abductive and default reasoning and can be used for diagnosis [63] and other problem solving activities [61]. Also Cox and Pietrzykowski [17] and Console, Theseider Dupré, and Torasso [13] present diagnostic systems that use logic-based abduction. Abduction is also fruitfully used for several applications apart from diagnosis in areas such as planning [23], design synthesis [27], database updates [38], natural language understanding and text generation [9, 10, 54, 34] analogical reasoning and machine learning [64, 14], user modeling (cf. [60]), and vision (cf. [11]).

Logic-based abduction

Several models and formalizations of abduction have been introduced. In this paper we are interested in logic-based abduction, which is more general than most other formal approaches to abduction. It has attracted a great deal of interest, especially in recent years, due to progress in logic programming and logic-based knowledge representation [42, 45].

Logic-based abduction can be described more formally as follows: Given a logical theory T formalizing a particular application domain, a set M of atomic formulas describing some manifestations, and a set H of (usually atomic) formulas containing possible individual hypotheses, find an explanation (or solution) for M, i.e., a suitable set S ⊆ H such that T ∪S is consistent and logically entails M. Consider, for instance, the following example from the domain of motor vehicles, inspired by [14]:

T = { ¬(rich mixture ∧ lean mixture),

rich mixture → high fuel consumption, lean mixture → overheating, low oil → overheating, low water → overheating },

H = { rich mixture, lean mixture, low oil, low water },
M = { high fuel consumption, overheating }.

Then, {rich mixture, low oil} and {rich mixture, low water} are abductive explanations of the manifestations M. Note that {rich mixture, lean mixture} is ruled out as an explanation, since it is inconsistent with T. It is easy to see that logic-based abduction is a form of nonmonotonic reasoning. Adding the formula ¬low oil to the theory T has the effect that {rich mixture, low oil} is no longer an admissible explanation. Thus, from stronger theories we may sometimes abduce less approaching categoricity. Logic-based abduction is particularly suitable if one of the following conditions applies:

• the domain knowledge is best represented by a logical theory, e.g. if it involves disjunctive information, integrity constraints, or negative information, which can not be expressed easily by simple mappings between causes and effects.

• rich knowledge about the relationship between causes and effects is available, e.g. about the behavior of a system in case of component failures.

Alternative approaches to logic-based abduction

A number of alternative approaches to logic-based abduction are known. These approaches can be uniformly described in terms of the following three basic concepts, which have already been used in the logic-based approach:

• A structure or theory T representing all the relevant domain knowledge.

• A set M of present manifestations (or observations, symptoms), which is a subset of the set M^{∗} of all possible manifestations.

• A set H of possible individual hypotheses that may be used to form explanations.

(Our formalization, without loss of generality will assume M^{∗} = M.) We briefly describe the most relevant alternative approaches to logic-based abduction, namely abduction by set-covering, probabilistic abduction, and consistency-based diagnosis with simplified definitions in terms of T, M^{∗}, M, and H.

Abduction by set-covering is a prominent and widely used method, cf. [59]. Here H is a finite set of atomic items representing all hypotheses (possible disorders). The domain knowledge T is represented by a function e from subsets of H to subsets of M^{∗} such that X explains e(X); X can be seen as a possible cause for e(X). A solution to a set-covering problem is a subset X ⊆ H such that e(X) = M. The attention is often limited to solutions that are acceptable according to some criteria. (Different concepts of acceptable solutions will be considered below.) There are several variants and refinements of the set-covering approach to abduction. For instance, a plausibility-order may be attached to subsets of H, cf. [6]. Furthermore, it may be useful to require that an abduction problem is independent, i.e. the function e satisfies e(X) = ⋃_{h∈H} e({h}), or that an abduction problem is monotonic, i.e. e satisfies ∀X, Y ⊆ H : X ⊆ Y ⇒ e(X) ⊆ e(Y) [6]. The set-covering model is best suited when the relationships between causes and effects are simple such that they can be easily made explicit in the form of a function.

Probabilistic abduction models the hypotheses in H and the manifestations in M as events. In addition to structural knowledge, T contains probabilistic knowledge about hypotheses and manifestations. In particular, T contains the prior probabilities of the hypotheses and the conditional probabilities between (sets of) hypotheses and (sets of) manifestations. A solution to a probabilistic abduction problem is a set A ⊆ H such that the a-posteriori probability P (A|M) is maximized. Several refinements and variants of probabilistic abduction have been introduced. Among the most important are Pearl’s Belief Networks [56, 57] and Peng and Reggia’s Probabilistic Causal Model [59]. Probabilistic models are best used when the following three conditions are satisfied:

1. The structural relations between hypotheses and manifestations are rather simple;

2. the necessary probabilistic knowledge is available; and

3. certain independence assumptions can be made in order to be able to compute a-posteriori probabilities (e.g. by applying Bayes’ Theorem).

Consistency-based diagnosis is usually considered as a competing approach to logicbased abductive diagnosis. According to this approach, the hypotheses in H represent the single components of the system to be diagnosed. The domain theory T is a set of firstorder sentences (called the system description) describing how the system functions. The system description T involves literals of the form ¬AB(c) to express that a component c ∈ H behaves correctly (i.e., not abnormally). The system behaves incorrectly iff T ∪M ∪ {¬AB(c) : c ∈ H} is inconsistent. A diagnosis is a set A ⊆ H such that T ∪M ∪{¬AB(x) : x ∈ H − A} ∪ {AB(x) : x ∈ H} is consistent.

Translations between this approach and the logic-based abductive approach to diagnosis have been studied in [14, 40]. In [15], Console and Torasso carefully compare the two approaches and point out that the logic-based abductive approach often leads to more precise diagnoses. Konolige also comes to this conclusion and shows that the abductive approach offers several advantages if one is interested in the representation of domain knowledge [40]. Notice that Bylander et al. have shown [6] how to map consistency-based diagnosis into a set-covering abduction problem. The consistency-based approach to diagnosis is particularly useful if we have a good description of how the system functions properly when its components are not faulty.

It should be clear that being totally dogmatic about the virtues of logic-based abduction is by no means justified. The complexity results derived in this paper suggest that logicbased abduction is by far the most general computational formulation, but that does not mean that logic-based abduction is always the method of choice. On the contrary, less complex formulations should be preferred if they are applicable.

Preferred solutions

In accordance with Occam’s razor [59], which states that from two explanations the simpler explanation is preferable, some minimality criterion is usually imposed on abductive explanations. Different minimality criteria correspond to different preference relations (usually preorders) on the solution space, or, more generally, on the powerset of H. Note that each minimality criterion can be regarded as a qualitative version of probability such that the minimal explanations correspond to the most likely ones. We briefly list the most important minimality criteria and explain how they relate to qualitative versions of probability. (Formal definitions are given in Sections 2 and 4.)

Subset-minimality (⊆). The subset-minimality criterion, termed irredundancy in [59], is most frequently used. It adopts each solution S such that no proper subset S′ ⊂ S of S is a solution. In our motor vehicle example, the solution {rich mixture, low oil, low water} is ruled out by this criterion, since e.g. the solution {rich mixture, low oil} is a proper subset of it. Notice that {rich mixture, low oil} is a subset-minimal solution. Subset-minimality is a rather weak minimality criterion. It is particularly appropriate when the hypotheses are events whose chances to be present (resp. absent) obey probabilistic principles, but there is no numeric knowledge about probability values. In this case, a solution A ⊆ H is at least as likely as any superset solution A ∪ B ⊆ H. This justifies discarding superset-solutions and concentrating on subset-minimal solutions.

Minimum cardinality solutions (≤). The minimum cardinality criterion states that a solution A ⊆ H is preferable to a solution B ⊆ H if |A| < |B|. Note that this criterion also rules out the solution {rich mixture, low oil, low water} in the motor vehicle example, since the cardinality of this solution is 3, while the cardinality of the solution {rich mixture, low oil} is 2; the latter solution is a minimum cardinality solution. Notice also that each minimum cardinality solution is also a subset-minimal solution, but not conversely. For this reason, minimum cardinality is a stronger criterion than subsetminimality. The restriction to minimum cardinality solutions is appropriate if the likelihood of solutions is well described by a probability function (just as above) and if we can make the additional assumption that all hypotheses of H are roughly equally probable and mutually independent events. In this case, sets of hypotheses of smaller cardinality will always be assigned a higher probability than sets of higher cardinality.

Prioritization. The method of priorities is a refinement of the above minimality criteria, which roughly operates as follows. The set of hypotheses H is partitioned into groups of different priorities, and solutions which are minimal on the lowest priority hypotheses are selected from the solutions. The quality of the selected solutions on the hypotheses of the next priority level is taken into account for further screening; this process is continued over all priority levels. (For a formal definition, see Section 4.) The subset-minimality criterion or the minimum cardinality measure is used to compare solutions on the hypotheses of a single priority level; the respective criteria, which depend on the prioritization P, are denoted by ⊆_{P} and ≤_{P}. Notice that prioritization can be combined analogously with other minimality criteria for solutions. Priority levels are also used in the context of theory update and revision [25] and [30], in prioritized circumscription [46], and in the preferred subtheories approach for default reasoning [3]. Prioritization is also a qualitative version of probability, where the different priority levels represent different magnitudes of probability. Prioritization is well-suited in case no precise numerical values are known, but the hypotheses can be grouped into clusters such that the probabilities of hypotheses belonging to the same cluster do not differ much compared to the difference between hypotheses from different clusters. If it can be assumed that within any cluster the probabilities of hypotheses are approximately equal, then prioritization is suitably combined with the minimum cardinality criterion; otherwise, the combination with subset-minimality is appropriate.

Penalization (⊑_{p}). The method of penalties is a refinement of the method of priorities combined with the minimum cardinality measure. It allows one to attach a weight (penalty) to each hypothesis from H and look for solutions with minimum total weight. These weights may be subjective values (similar to certainty factors) or the outcome of a statistical analysis. In a more utilitarian fashion, penalties may also be used, e.g. in diagnosis, to represent the cost of cure or repair associated with different hypotheses (= disorders); this would mean that diagnoses (i.e. explanations) entailing less expensive cure or repairs would be preferred, which makes sense in some contexts. In a similarly utilitarian fashion, penalties may be used to quantify the cost or effort required to check whether a hypothesis belonging to a computed explanation effectively applies. A doctor will usually prefer to consider a diagnosis first that can be confirmed or disproved by simply looking into the patient’s mouth and measuring the blood pressure. Only if this diagnosis does not apply, the doctor may want to consider diagnoses whose verification require a time consuming and expensive computer-tomographic analysis (except in the US, where legally defensible medicine is practiced). Finally, penalties are also well-suited for expressing probabilistic knowledge (here of a numeric nature) on the hypotheses. If the hypotheses are assumed to be statistically independent events, then the probability P (h_{i}) that hypothesis h_{i} is present may be represented as the penalty p(h_{i}) = log (\frac{1}{P (h_{i})}). The penalty ∑_{i=1}^{n} p(h_{i}) attached to the composite hypothesis A = {h_{1}, …, h_{n}} then exactly matches the joint probability Π_{i=1}^{n}P (h_{i}) of the events h_{1}, …, h_{n}, since log (\frac{1}{Π_{i=1}^{n}P (h_{i})}) = ∑_{i=1}^{n} log (\frac{1}{P (h_{i})}) = ∑_{i=1}^{n} p(h_{i}).

The main problems

In the context of logic-based abduction, the main decision problems are:

(i) to determine whether an explanation for the given manifestations exists at all;

(ii) to determine whether an individual hypothesis h ∈ H is relevant, i.e., whether it is part of at least one acceptable explanation;

(iii) to determine whether an individual hypothesis is necessary, i.e., whether it occurs in all acceptable explanations.

Furthermore, the search problems of computing an explanation or a best explanation are important. Due to results of Bylander, Allemang, Tanner and Josephson [1, 5, 6], the complexity of these problems in the context of the set-covering approach to abduction is quite well understood. On the other hand, the complexity of logic-based abduction has only been partially investigated. Selman and Levesque [69], Bylander [4], and Friedrich et al. [28] studied the particular case where T is a propositional Horn theory and where the subsetminimality measure is used (for definitions, see Sections 2 and 5). Eshghi [24] studied abduction under further restriction of T to a subclass of Horn theories. The complexity of abductive reasoning in the general propositional case was left open, and it was also unclear how different minimality criteria would affect the complexity in both the general and the Horn case. It is precisely the aim of this paper to shed light on these questions. We give a complete picture of the complexity of the main decision problems related to propositional abduction by providing completeness results for several complexity classes at lower levels of the polynomial hierarchy, and we address some important search problems such as the computation of a best solution.

Overview of results

We consider propositional abduction problems whose domain theories T are of one of the following forms: general propositional theories, clausal theories, Horn clauses, or definite Horn clauses. Our main results are shortly summarized as follows.

• General case. If T is an arbitrary propositional theory and no minimality criterion is applied to the solutions, the complexity of the main decision problems is located at the second level of the polynomial hierarchy. More precisely, checking for the existence of an explanation is Σ_{2}^{P} -complete, testing the relevance of an individual hypothesis is also Σ_{2}^{P} -complete, while checking if a hypothesis is necessary is Π_{2}^{P} -complete. Thus, even the simplest form of abduction is harder^{1} than deduction.

• General theories and subset-minimal explanations. If the subset-minimality criterion is imposed on general explanations, then the same completeness results hold. Thus, surprisingly, reasoning with subset-minimal explanations turns out to be of the same complexity as reasoning with general explanations.

• General theories and minimum cardinality explanations. In case only minimum cardinality explanations are accepted, both checking whether a hypothesis is relevant and checking if it is necessary is complete for Δ_{3}^{P} [O(log n)], the class of decision problems solvable in polynomial time with a logarithmic number of calls to a Σ_{2}^{P} oracle. Δ_{3}^{P} [O(log n)] is at the second level of the polynomial hierarchy. Thus, cardinality-based minimality leads to a “mildly” harder complexity than subset-based minimality. Note that cardinalitybased minimization is equivalently obtained by attaching a penalty of value 1 to each individual hypothesis.

• General theories and penalization. If the method of penalties is used, the same problems become complete for Δ_{3}^{P}. This is the hardest class of problems at the second level of the polynomial hierarchy. Note that our hardness-proof requires the use of very high penalties whose value is exponential in the input size n. If we limit admissible penalty-values to an upper bound p(n), where p is a polynomial, then the complexity falls back to Δ_{3}^{P} [O(log n)]. The same applies if penalties are represented in tally notation.

• General theories and prioritization. We analysis the method of priorities combined with subset-minimality as well as with the minimum cardinality criterion. In the first case, relevance-checking is Σ_{3}^{P} -complete and necessity-checking is Π_{3}^{P} -complete. The complexity thus goes up to the third level of the polynomial hierarchy. In the second case, both problems stay at the second level being complete for Δ_{3}^{P}.

1Under the assumption the polynomial hierarchy does not collapse; we will make this assumption implicitly, whenever we use the term “hard” in the rest of this paper.

• Theories in clause form. For clausal theories, exactly the same complexity results hold as for the general theories.

• Horn theories. If T consists of Horn clauses, then the complexity of each of the described decision problems is lowered by exactly one level in the polynomial hierarchy. More precisely, any problem complete for Σ_{i}^{P} , Π_{i}^{P} , Δ_{i}^{P} , or Δ_{i}^{P} [O(log n)] on general theories is complete for the respective class Σ_{i−1}^{P}, Π_{i−1}^{P}, Δ_{i−1}^{P}, or Δ_{i−1}^{P}[O(log n)] on Horn theories. This is also true for definite Horn theories, except for testing of existence of a solution, as well as for relevance and necessity checking when no minimality criterion at all is applied to the explanations, or where subset-minimality is used together with the method of priorities. In all the latter cases, the complexity is lowered by exactly two levels in the polynomial hierarchy.

• Computation of solutions. Computing a general explanation or a subset-minimal explanation is complete for the class of multivalued search problems solvable by nondeterministic Turing machines with polynomially many NP-oracle calls. Under the cardinalitybased preference relation and with Horn theories, the same problem becomes a member of the class of hard NP optimization problems recently defined by Chen and Toda [12]. These problems can be solved with arbitrarily high probability by randomized algorithms making one free evaluation of parallel queries to NP.

Our results explain how various assumptions on the syntactic form of theories interact with various minimality criteria and may support a designer of an abductive expert system in choosing the right settings. For instance, our results suggest that – if permitted by the application – using the method of penalties is preferable to using the method of priorities together with the usual subset-minimality criterion. Our completeness results also allow one to classify different versions of abduction with respect to different alternative techniques of nonmonotonic reasoning and establish links and translations between reasoning tasks in various formalisms. For example, it is known that relevant reasoning tasks in Reiter’s default logic [66] or in Moore’s autoepistemic logic [51] are Π_{2}^{P} -complete [32]. Thus, one can polynomially transform abductive reasoning problems to default or autoepistemic reasoning tasks and take advantage of existing algorithms and proof procedures. Conversely, any abductive reasoning engine can be used to solve problems in other nonmonotonic logics. Note that a transformation from a relevant fragment of default logic to abduction was already given in [60]. Another example is theory updating. In [22] it is shown that evaluating counterfactuals according to Dalal’s method of updating propositional theories is complete for Δ_{2}^{P} [O(log n)]. It follows from the results of the present paper that this task can be polynomially mapped into a Horn abduction problem with cardinality-based minimality measure. Finally, our results show that the different variations of abduction provide a rich collection of natural problems populating all major complexity classes between P and Σ_{3}^{P}, Π_{3}^{P}. Abduction appears to be one of the few natural problems with this characteristic. Our results may thus be used as a “toolbox” helping to analyze the complexity of yet different problems.

The rest of this paper is organized as follows. In Section 2 we provide the reader with the basic definitions and give a brief review of the relevant complexity concepts. Section 3 reports about related previous work. The complexity results for general propositional theories are shown in Section 4 while Section 5 is dedicated to Horn cases. Section 6 briefly addresses the problem of computing explanations. The main results of the paper are compactly summarized in three tables in Section 7. There, we analyze sources of complexity and conclude the paper by discussing some related results concerning other forms of reasoning and by outlining possible issues for future research.

2 Preliminaries

Abduction model

Let L_{V} be the language of propositional logic over an alphabet V of propositional variables, with syntactic operators ∧, ∨, ¬, →, ↔, ⊤ (a constant for truth), and ⊥ (falsity). We adopt the standard binding rules for operators. A theory is a finite set T ⊆ L_{V}. For convenience, we refer to a theory T also as the conjunction of its formulae. Each variable is an atom, and a literal is an atom or a negated atom. Unless stated otherwise, we assume throughout the paper that distinct variable symbols refer to distinct variables. A clause is a disjunction x_{1} ∨ ⋯ ∨ x_{k} ∨ ¬x_{k+1} ∨ ⋯ ∨ ¬x_{n} of (pairwise distinct) literals. We do not distinguish between clauses with different literal order and refer to a clause also as the set of its literals. A clause is Horn (definite Horn) iff k ≤ 1 (k = 1). A theory is in clausal form iff all its formulae are clauses. A formula is in conjunctive normal form (CNF) iff it is a conjunction of clauses, and is in disjunctive normal form (DNF) iff it is a disjunction D_{1} ∨ ⋯ ∨ D_{n} of conjunctions D_{i} of literals. Truth assignments are defined in the usual way. For every truth assignment ϕ(V) to the variables V and F ∈ L_{V}, V_{ϕ}(F) denotes the truth value of F according to ϕ. F is satisfied by ϕ iff V_{ϕ}(F) = true. As usual, for F, G ∈ L_{V} and T ⊆ L_{V}, G ⊧ F (resp. T ⊧ F) means that for all truth assignments ϕ(V), ϕ satisfies F if ϕ satisfies G (resp. all formulas in T). If E is a formula and ϕ(X) is a truth assignment to variables X = {x_{1}, …, x_{n}} occurring in E, then E_{ϕ(X)} denotes the formula obtained by replacing each occurrence of x in E by ⊤ if ϕ(x) = true and by ⊥ if ϕ(x) = false, for all x ∈ X.

Definition 2.1 A propositional abduction problem (PAP) P consists of a tuple ⟨V, H, M, T ⟩, where V is a finite set of propositional variables, H ⊆ V is the set of hypotheses, M ⊆ V is the set of manifestations, and T ⊆ L_{V} is a consistent theory.

Definition 2.2 Let P = ⟨V, H, M, T ⟩ be a PAP. S ⊆ H is a solution (or explanation) to P iff T ∪ S is consistent and T ∪ S ⊧ M. Sol(P) denotes the set of all solutions to P.

In this model of abduction, a hypothesis plays the role of what in other models is called an abducible proposition (see [14]). Notice that neither H ∩ M = ∅ nor H ∪ M = V is required. H ∩ M ≠ ∅ makes sense since a manifestation m may be an explanation for another manifestation m′. H ∪ M ⊂ V means that explanations are “assumption-based”, as not all propositions are allowed to appear in a solution. This seems natural, however, since, in focusing attention, one will be interested in an explanation from a certain subset of facts rather than from all facts. Anyway, neither H ∩ M = ∅ nor H ∪ M = V would imply a deficiency of our study of computational issues, since our results remain valid under both restrictions. H ∩ M = ∅ will hold in all but few proofs, and H ∪ M = V will with rare exceptions always be considered. In the remaining cases, it will not be difficult to adapt proofs appropriately. Note also that we only allow positive atoms in solutions and exclude negative atoms as well as general propositional formulas F (cf. Konolige’s causal theories [40] for a similar model). This convention is no restriction of generality, since we may add to T a formula x′ ↔ F where x′ is a new variable that we add to the hypotheses H. We do not require T to be in any special form. In implementations, however, theories are often put into some special format. The most common of such formats is clausal form. It appears that clausal form does not affect the computational complexity of logic-based abduction, which is however no surprise. We will consider several restrictions of Sol(P) to a subset of “acceptable” solutions, which is defined by means of a suitable preference relation between solutions. Natural axioms for such a preference relation are reflexivity and transitivity; thus, we model preference relations by preorders. Throughout the paper, ⪯ denotes a preorder on the powerset 2^{H} of the hypotheses H. a ≺ b stands for a ⪯ b ∧ b ⪯̸ a. The preferred (or acceptable) solutions Sol_{⪯}(P) of a PAP P under order ⪯ are defined as follows.

Definition 2.3 Sol_{⪯}(P) = {S ∈ Sol(P) : ∄S′ ∈ Sol(P) : S′ ≺ S}, that is, Sol_{⪯}(P) is the set of minimal elements of Sol(P) under ⪯.

In particular, Sol(P) equals Sol_{=}(P). An important property for preference relations is irredundancy of solutions [59, 69, 6, 40].

Definition 2.4 ⪯ is irredundant iff ∀S, S′ ∈ Sol(P) : S ⊂ S′ ⇒ S ≺ S′.

We will mainly deal with irredundant preference orders in this paper. Two well-known orders of this kind are the subset-minimality order and the minimum cardinality (or mininum solution size) order. The subset-minimality order is just irredundancy itself, that is, S ⪯ S′ iff S ⊆ S′, which we denote by ⊆. The minimum solution size order (e.g.

[59]), which we denote by ≤, is defined by S_{1} ≤ S_{2} iff |S_{1}| ≤ |S_{2}|. Both orders will deserve proper attention in our study. The irredundant solutions Sol_{⊆}(P) can also be characterized as follows.

Proposition 2.1 Let P = ⟨V, H, M, T ⟩ be a PAP. Then, Sol_{⊆}(P) = {S ∈ Sol(P) : S − {h} ∉ Sol(P), for all h ∈ S}.

Proof. Indeed, if S ∈ Sol(P) and S − {h} ∈ Sol(P) for some h ∈ S, then S ∉ Sol_{⊆}(P). Conversely, if S ∈ Sol(P) but S ∉ Sol_{⊆}(P), then there exists S′, S′ ⊂ S such that S′ ∈ Sol(P). By the monotonicity of ⊧, for all S′′ such that S′ ⊆ S′′ ⊂ S, T ∪ S′′ ⊧ M, thus S′′ ∈ Sol(P); hence, S − {h} ∈ Sol(P) for some h ∈ S. □ We conclude this subsection with a simple technical lemma.

Lemma 2.2 Let P_{1}, P_{2}, …, P_{n} be PAPs, P_{i} = ⟨V_{i}, H_{i}, M_{i}, T_{i}⟩, 1 ≤ i ≤ n, such that V_{i} ∩ V_{j} = ∅ for 1 ≤ i < j ≤ n, and let V = ⋃_{i} V_{i}, H = ⋃_{i} H_{i}, M = ⋃_{i} M_{i}, and T = ⋃_{i} T_{i}. Then, Sol_{⪯}(⟨V, H, M, T ⟩) = {S_{1} ∪ ⋯ ∪ S_{n} : S_{i} ∈ Sol_{⪯}(P_{i}), 1 ≤ i ≤ n}, if ⪯ is equality, ⊆-, or ≤-preference.

The main problems

Three interesting issues in abductive reasoning are: Given a PAP P,

1. does there exist a solution for P ?

2. does a hypothesis h contribute to some acceptable solution of P (relevance)?

3. does a hypothesis h occur in all acceptable solutions of P (necessity) ?

The study of the complexity of these problems is the main subject of this paper. The problem of deciding relevance or necessity of hypotheses has previously been dealt with in [5] for set-oriented abduction models and in [69, 28, 4] for certain subclasses of propositional abduction.

Definition 2.5 Let P = ⟨V, H, M, T ⟩ be a PAP, and let h ∈ H. h is ⪯-relevant for P iff there exists S ∈ Sol_{⪯}(P) such that h ∈ S, and h is ⪯-necessary for P iff for all S ∈ Sol_{⪯}(P), h ∈ S.

Note that H is divided into the three disjoint sets of not ⪯-relevant, ⪯-relevant but not ⪯-necessary hypotheses, and ⪯-necessary hypotheses. We say that h is ⪯-irrelevant for P iff h is not ⪯-relevant for P, and that h is ⪯- dispensable for P iff h is not ⪯-necessary for P (in [36], necessity is termed indispensability). Furthermore, in the case where ⪯ is equality, the ⪯-prefix is dropped, and we say necessary instead of =-necessary etc. Throughout our analysis, we will primarily deal with ⪯-dispensability rather than with ⪯-necessity for convenience. Results for ⪯-necessity are easy corollaries to our results on ⪯-dispensability.

Review of complexity classes

For the concepts of complexity theory, refer to [29, 35]. The notion of completeness we employ is many-one polynomial time transformability (≤_{m}^{p}). Recall that the classes Δ_{k}^{P} , Σ_{k}^{P} , and Π_{k}^{P} of the polynomial time hierarchy (PH) [50] are defined as follows (rf. [29]):

Δ_{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}.

In particular, NP = Σ_{1}^{P}, co-NP = Π_{1}^{P}, and Δ_{2}^{P} = P^{NP}. PH is equal to ⋃_{k=0}^{∞} Σ_{k}^{P}. We say that a problem is at the k-th level of PH if it is complete for Δ_{k+1}^{P} under Turing reductions (i.e., it is in Δ_{k+1}^{P} and Σ_{k}^{P} -hard or Π_{k}^{P} -hard). A well-known problem at the k-th level of PH, k ≥ 1, is deciding the validity of a quantified Boolean formula with k “quantifier alternations”. A quantified Boolean formula (QBF) is a sentence of the form Q_{1}x_{1} ⋯ Q_{n}x_{n}E, n ≥ 0, where E is a propositional formula whose variables are from x_{1}, …, x_{n} and where each Q_{i}, 1 ≤ i ≤ n, is one of the quantifiers ∀, ∃ ranging over {true, false}.^{2} Such a formula is said to have a quantifier alternation for Q_{1} and for each Q_{i}, i > 1, such that Q_{i} ≠ Q_{i−1}. The set of valid QBFs with k quantifier alternations and Q_{1} = ∃ (resp. Q_{1} = ∀) is denoted by QBF_{k,∃} (resp. QBF_{k,∀}). For example, the QBF Φ = ∀x_{1}∃x_{2}∃x_{3}∀x_{4} (x_{1} ∧ x_{2} → x_{3} ∨ x_{4}) has 3 quantifier alternations; it is easily seen that Φ is valid, hence Φ ∈ QBF_{3,∃}. It is well-known that deciding whether a QBF Φ satisfies Φ ∈ QBF_{k,∃} (resp. Φ ∈ QBF_{k,∀}) is Σ_{k}^{P} -complete (resp. Π_{k}^{P} -complete). Δ_{k}^{P} also has complete problems for all k ≥ 2; for example, given a formula E on variables x_{1}, …, x_{n},y_{1}, …, y_{r}, r ≥ 0, and a quantifier pattern Q_{1}y_{1} ⋯ Q_{r}y_{r}, decide whether the with respect to ⟨x_{1}, …, x_{n}⟩ lexicographically maximum truth assignment^{3} ϕ to x_{1}, …, x_{n} such that Q_{1}y_{1} ⋯ Q_{r}y_{r}E_{ϕ} ∈ QBF_{k−2,∀} (where such a ϕ is known to exist) fulfills ϕ(x_{n}) = true (cf. [74, 44]).^{4} Δ_{k}^{P} has been refined to account for the required number of oracle calls to solve a problem [73, 43, 44, 37, 35, 74]. The class Δ_{k+1}^{P}[O(log n)] (also denoted by P^{Σ_{k}^{P} [O(log n)]}, or by Θ_{k+1}^{P}) is the class of problems decidable in deterministic polynomial time with O(log n) queries to a Σ_{k}^{P} oracle, where n is the input size [74, 44]. Δ_{k+1}^{P}[O(log n)] has complete problems for all k ≥ 1; for example, given QBFs Φ_{1}, …, Φ_{m}, such that Φ_{i} ∉ QBF_{k,∃} implies Φ_{i+1} ∉ QBF_{k,∃}, for 1 ≤ i < m, decide whether max{i : 1 ≤ i ≤ m, Φ_{i} ∈ QBF_{k,∃}} is odd ([74], see proof of Lemma 4.5). A number of Δ_{2}^{P} [O(log n)]-complete problems appear in [73, 43, 37]. Note that Δ_{k}^{P} and Δ_{k}^{P} [O(log n)] are closed under complementation, i.e. a problem Π is in one of these classes iff its complementary problem co-Π is. In particular, Π is complete for such a class iff co-Π is.

2In fact, Quantified Propositional Formula (QPF) rather than QBF would be correct. Note that QPFs are second-order sentences. In abuse of terminology, we do not distinguish between the isomorphic concepts of QPF and QBF.

3ϕ is w.r.t. ⟨x_{1}, …, x_{n_{x}}⟩ lexicographically greater than ψ iff ϕ(x_{j}) = true, ψ(x_{j}) = false for the least j such that ϕ(x_{j}) ≠ ψ(x_{j}).

4QBF_{0,∀} = QBF_{0,∃} is the set of all variable-free true formulas.

3 Previous results

Computational complexity results for abduction have been derived previously. It appears that more work has been done on non-logical abduction approaches than on logical abduction, which on the other hand has been analyzed mainly for fragments of propositional logic. Bylander and his coworkers extensively investigated the complexity of abduction, based upon a “functional” abduction model [1, 36, 5, 6, 4]. Their work mainly aimed at characterizing the complexity of computing any (in our terms) ⪯-solution or all ⪯-solutions of an abduction problem, where ⪯ is an irredundant preference (in fact, even partial) order based on a plausibility relation. The underlying assumptions of Bylander’s work allows one to model certain parts of propositional logic [4], and is thus somewhat related to our work (see below). In the context of Bayesian belief networks [56], Cooper showed the intractability of calculating the probability that a certain hypothesis is present in some explanation, ignoring other hypotheses [16]. For the logical approach, a number of very interesting complexity results for abduction on Horn theories have been derived by Selman and Levesque [69], Friedrich et al. [28], and by Bylander [4]. Selman and Levesque show that, in our terms, finding a ⊆-solution as well as finding any solution to a Horn PAP P is NP-hard, and that the same holds if the solution must contain a certain hypothesis h.^{5} These results are shown by a reduction from an NP-complete problem on graphs; we give new proofs. Eshghi has shown in [24], where the notion of solution slightly stricter than in this paper, that finding a ⊆-minimal solution is tractable if T is acyclic Horn and its pseudo-completion is unit-refutable. Friedrich et al. studied complexity issues for definite Horn PAPs [28]. They showed that under this restriction, deciding necessity, relevance, and ⊆-necessity of a hypothesis is polynomial, and that deciding ⊆-relevance of a hypothesis is NP-complete. Bylander [4] demonstrates a polynomial transformation of a certain subclass of the functional abduction model [6], the independent abduction problems, into definite Horn PAPs. Thus, by previous results [6], the tractability of finding some ⊆-solution (and hence also of finding any solution) is established.

5We should note that not all these results are explicitly stated, but follow immediately from proofs in that paper.

Results somewhat less related to ours are also shown by Rutenburg [68] and Provan [65] in the context of truth maintenance systems (TMS) [20]. The role of TMSs for abductive problem solving has already been pointed out in [45], and the relationship between TMS and abduction was further investigated in [31]. Rutenburg [68] analyzed the complexity of various alternatives of a TMS, and presented several NP-completeness results and a Σ_{2}^{P} -completeness result for decision problems associated to finding TMS-explanations (“nogoods”) of certain size. His analysis also covers de Kleer’s popular assumption-based TMS (ATMS) [18], for which Provan derived similar results [65].

4 Complexity results: the general case

In this section, we present complexity results for deciding ⪯-relevance and ⪯-dispensability for a full propositional PAP under several preference criteria, among them ⊆-preference, ≤-preference, and prioritized abduction. We also cover the case of an arbitrary efficiently decidable preference order, and we address the complexity of deciding whether a PAP has any solution at all. All results derived in this section render the respective problems complete for classes at the second or third level of the PH. We note the following easy proposition.

Proposition 4.1 Let P = ⟨V, H, M, T ⟩ be a PAP. Deciding if S ⊆ H fulfills S ∈ Sol(P) is in Δ_{2}^{P}.

Proof. Since S ∈ Sol(P) iff S ⊆ H, T ∪ S is consistent, and T ∪ S ⊧ M, this is clear. □

Remark: Deciding S ∈ Sol(P) is easily shown to be D^{P} -complete (see [35] for D^{P}).

Deciding Sol(P) ≠ ∅

First, we show that deciding if a PAP P has any solution is a Σ_{2}^{P} -complete problem. More strictly, we show that this result may be strengthened to the case where H ∪ M = V and T is in clausal form. Roughly, deciding Sol(P) ≠ ∅ is Σ_{2}^{P} -complete because one needs to find a subset of hypotheses (corresponding to existentially quantified Boolean variables) which entails the manifestations (corresponding to universally quantified variables).

Theorem 4.2 To decide if Sol(P) ≠ ∅ for a given PAP P = ⟨V, H, M, T ⟩ is Σ_{2}^{P} -complete. Σ_{2}^{P} -hardness holds even if H ∪ M = V and T is in clausal form.

Proof. By Proposition 4.1, verifying a guess for S ∈ Sol(P) is in Δ_{2}^{P}, hence membership in Σ_{2}^{P} follows.

Σ_{2}^{P} -hardness of this problem is shown by a transformation from deciding Φ ∈ QBF_{2,∃}. Let without loss of generality Φ be a QBF ∃x_{1} ⋯ ∃x_{n}∀y_{1} ⋯ ∀y_{m}E. Let X = {x_{1}, …, x_{n}}, Y = {y_{1}, …, y_{m}}, X′ = {x′_{1}, …, x′_{n}}, and let further s be a new variable. Define a PAP P = ⟨V, H, M, T ⟩ as follows.

V = X ∪ Y ∪ X′ ∪ {s}
H = X ∪ X′
M = Y ∪ {s}
T = {x_{i} ↔ ¬x′_{i} : 1 ≤ i ≤ n} ∪ {E → s ∧ y_{1} ∧ ⋯ ∧ y_{m}} ∪
{s → y_{1} ∧ ⋯ ∧ y_{m}}

Note that T is consistent and that P is constructible in polynomial time. We show that Φ ∈ QBF_{2,∃} holds if and only if Sol(P) ≠ ∅. Assume Φ ∈ QBF_{2,∃} holds. Hence, there exists a truth assignment ϕ(X) such that ∀y_{1} ⋯ ∀y_{m}E_{ϕ(X)} ∈ QBF_{1,∀} holds. Define

S = {x_{i} : ϕ(x_{i}) = true, 1 ≤ i ≤ n} ∪ {x′_{i} : ϕ(x_{i}) = false, 1 ≤ i ≤ n}.

Clearly, S ⊆ H and T ∪ S is consistent. Since T ∪ S logically implies x_{i} ≡ ϕ(x_{i}), 1 ≤ i ≤ n, it follows that T ∪ S ⊧ E_{ϕ(X)}. Since T ∪ S ⊧ E → s ∧ y_{1} ∧ ⋯ ∧ y_{m}, clearly T ∪ S ⊧ s ∧ y_{1} ∧ ⋯ ∧ y_{m} holds. Thus, S ∈ Sol(P). Conversely, assume that there exists S ∈ Sol(P). Note that {x_{i}, x′_{i}} ⊈ S, 1 ≤ i ≤ n. It holds that T ∪ S ⊧ E. To show this, assume that T ∪ S |̸= E, i.e., T ∪ S ∪ {¬E} is consistent. It is easily seen that in this case, T ∪ S ∪ {¬E, ¬s} is consistent, too. Consequently, T ∪ S |̸= s, which is a contradiction since S ∈ Sol(P) and s ∈ M. It follows that T ∪ S ⊧ E. Define a truth assignment ϕ(X) by ϕ(x_{i}) = true if x_{i} ∈ S and ϕ(x_{i}) = false if x_{i} ∉ S, 1 ≤ i ≤ n. Since T ∪ S ∪ {x′_{i} : x_{i} ∉ S} is consistent and logically implies x_{i} ≡ ϕ(x_{i}), for 1 ≤ i ≤ n, and since T ∪ S ∪ {x′_{i} : x_{i} ∉ S} ⊧ E_{ϕ(X)}, E_{ϕ(X)} is a tautology. Thus Φ = ∃x_{1} ⋯ ∃x_{n}∀y_{1} ⋯ ∀y_{m}E ∈ QBF_{2,∃} holds. It remains to show that deciding Sol(P) ≠ ∅ is Σ_{2}^{P} -hard even if H ∪ M = V and T is in clausal form. Note that H ∪ M = V already holds. By the results in [72], checking Φ ∈ QBF_{2,∃} remains Σ_{2}^{P} -hard even if E is in DNF. Hence a CNF formula \overline{E}(x_{1}, …, x_{n}, y_{1}, …, y_{m}) = C_{1} ∧ C_{2} ∧ ⋯ ∧ C_{r} with \overline{E} ≡ ¬E can efficiently be constructed. It is easy to see that {E → s ∧ y_{1} ∧ ⋯ ∧ y_{m}, s → y_{1} ∧ ⋯ ∧ y_{m}} is logically equivalent to the clausal theory

C = {C_{i} ∪ {s} : 1 ≤ i ≤ r} ∪ {C_{i} ∪ {y_{j}} : 1 ≤ i ≤ r, 1 ≤ j ≤ m} ∪ {{¬s, y_{i}} : 1 ≤ i ≤ m}

Clearly, C can be constructed in polynomial time from E as well as the clausal theory T′ = C ∪ {¬x_{i} ∨ ¬x′_{i}, x_{i} ∨ x′_{i} : 1 ≤ i ≤ n}. Since T′ is clearly logically equivalent to T, checking Sol(P) ≠ ∅ is ≤_{m}^{p}-reducible to the subcase where H ∪ V = M and T is in clausal form. Whence the theorem is proved. □

We remark that deciding Sol(P) ≠ ∅ becomes “easier” if H is consistent with T. In this case, the problem is in NP (and clearly NP-complete). Thus unless hypotheses are incompatible, abduction is, in a sense, no harder than deduction.

Relevance and dispensability

Checking whether a hypothesis is relevant for a PAP is of the same complexity as checking if a PAP has a solution.

Theorem 4.3 Deciding if a given hypothesis is relevant for a PAP P is Σ_{2}^{P} -complete, as well as deciding if a given hypothesis is dispensable for P. Σ_{2}^{P} -hardness holds even if H ∪ M = V and T is in clausal form.

Proof. By Proposition 4.1, verifying a guess for S ∈ Sol(P) such that h ∈ S (resp. h ∉ S) is in Δ_{2}^{P}, hence membership of the problems in Σ_{2}^{P} is clear. Σ_{2}^{P} -hardness is shown by the following reduction. Let P = ⟨V, H, M, T ⟩, and let h, h′, m′ ∉ V be new variables. Define a PAP P′ = ⟨V ∪ {h, h′, m′}, H ∪ {h, h′}, M ∪ {m′}, T′⟩ where

T′ = {¬h ∨ F : F ∈ T } ∪ {h′ → m : m ∈ M} ∪ {¬h ∨ ¬h′, h → m′, h′ → m′}.

Clearly, T′ is consistent and constructible in polynomial time. It is straightforward to verify that Sol(P′) = {S ∪ {h} : S ∈ Sol(P)} ∪ {{h′} ∪ A : A ⊆ H}. Therefore, deciding if h′ is dispensable (resp. h is relevant) for P′ is Σ_{2}^{P} -hard by Theorem 4.2, by which also the sharpening of this result to the indicated subcase follows. □ As a consequence of Theorem 4.3, if an algorithm is designed that tries to remove hypotheses from H subsequently in order to construct a solution for a PAP P, it is most likely that this algorithm will backtrack and will have exponential run-time, even if it has access to an NP oracle.

⊆-preference

At first glance surprising is that relevance and dispensability checking under ⊆-preference is of the same complexity as under no preference. The ⊆-minimality criterion imposed on solutions is not an additional source of complexity, however, since deciding whether a solution is a ⊆-solution is by monotony of classical inference ⊧ possible in polynomial time with an NP oracle.

Theorem 4.4 Deciding if a given hypothesis is ⊆-relevant for a PAP P is Σ_{2}^{P} -complete, as well as deciding if a given hypothesis is ⊆-dispensable for P. Σ_{2}^{P} -hardness holds even if H ∪ M = V and T is in clausal form.

Proof. Let P = ⟨V, H, M, T ⟩ and let h ∈ H. By Propositions 2.1 and 4.1 verifying a guess for S ∈ Sol_{⊆}(P) such that h ∈ S (resp. h ∉ S) is clearly in Δ_{2}^{P}. Hence membership of those problems in Σ_{2}^{P} follows. Σ_{2}^{P} -hardness of ⊆-relevance and ⊆-dispensability checking, even under the stated restriction, follows immediately from the construction of P′ in the proof of Theorem 4.3, since {h′} ∈ Sol_{⊆}(P′) and hence h is relevant iff it is ⊆-relevant for P, and h′ is dispensable for P′ iff it is ⊆-dispensable for P′. Whence the theorem is proved. □

Note that the restriction of the acceptable solutions to inclusion-minimal solutions makes the relevance and dispensability test not harder.

≤-preference

Under ≤-preference, deciding relevance and dispensability seemingly becomes more complex. Thus while restricting the acceptable solutions to ⊆-solutions does not change the complexity of the problems, ≤-preference presumably requires additional computational power. This for the reason that already checking if S ∈ Sol_{≤}(P) for a given S ∈ Sol(P) is Π_{2}^{P} -hard, and hence most likely not possible in polynomial time with an NP oracle. Nevertheless, relevance and dispensability checking under ≤-preference is only “mildly” harder than under ⊆-preference. Roughly, deciding ≤-relevance and ≤-dispensability is harder than deciding ⊆-relevance and ⊆-dispensability since verifying whether a solution S is a ≤-solution is apparently more complex. An intuitive explanation is that in order to decide this problem, knowing the “global” minimum solution size s is essential, while for ⊆-minimality this problem requires no “global” knowledge and depends only “locally” on S. Computing s is Σ_{2}^{P} - and Π_{2}^{P} -hard, but possible in polynomial time with a Σ_{2}^{P} oracle. By using standard search techniques, a logarithmic upper bound on the number of oracle calls can be established. We refer in the proof of the next result to the following lemma.

Lemma 4.5 Let Φ_{1}, Φ_{2}, …, Φ_{m} be QBFs such that Φ_{i} = ∃x_{1}^{i} ⋯ ∃x_{n_{x}}^{i}∀y_{1}^{i} ⋯ ∀y_{n_{y}}^{i}E_{i}, E_{i} is in DNF, 1 ≤ i ≤ m, and that Φ_{i} ∉ QBF_{2,∃} implies Φ_{i+1} ∉ QBF_{2,∃}, 1 ≤ i < m. Let ν(Φ_{1}, …, Φ_{m}) = max{i : Φ_{i} ∈ QBF_{2,∃}, 1 ≤ i ≤ m}.^{6} Deciding whether ν(Φ_{1}, …, Φ_{m}) is odd is Δ_{3}^{P} [O(log n)]-complete.

Proof. Since deciding Φ_{i} ∈ QBF_{2,∃} is Σ_{2}^{P} -complete [72], 1 ≤ i ≤ m, this follows immediately from [74, Theorem 8.1], which states that for k ≥ 1, in terms of languages, A ∈ Δ_{k+1}^{P}[O(log n)] iff A ∈ Σ_{k}^{P} (P ol), i.e. there exists B ∈ Σ_{k}^{P} and a polynomial p such that c_{B}(x, i + 1) ≤ c_{B}(x, i), for all 1 ≤ i ≤ p(|x|) and c_{A}(x) = max{i : 1 ≤ i ≤ p(|x|), (x, i) ∈ B} mod 2, and the fact that new x^{i} and y^{i} variables that do not occur in E_{i} can be easily added to the quantifier prefix of Φ_{i} such that the validity/invalidity of the formula Φ_{i} is preserved. □

6Here max ∅ = 0.

Theorem 4.6 Given a PAP P = ⟨V, H, M, T ⟩ and a hypothesis h ∈ H, deciding if h is ≤-dispensable (resp. ≤-relevant) for P is Δ_{3}^{P} [O(log n)]-complete. Δ_{3}^{P} [O(log n)]-hardness holds even if H ∪ M = V and T is in clausal form.

Proof. Membership in Δ_{3}^{P} [O(log n)] is shown for both problems as follows: compute the minimum solution size s = min{|S| : S ∈ Sol(P)} by binary search, querying the Σ_{2}^{P} oracle whether there exists S ∈ Sol(P) such that |S| ≤ k, where k is in the input. Then, query the oracle whether there exists S ∈ Sol(P) such that |S| = s and h ∉ S (resp. h ∈ S). The oracle answers yes if and only if h is ≤-dispensable (resp. h is ≤-relevant). Note that this procedure works correctly also if Sol(P) = ∅ (s can be any value). Δ_{3}^{P} [O(log n)]-hardness for both problems is shown by a ≤_{m}^{p}-reduction of the problem in Lemma 4.5 as follows. Consider Φ_{i} = ∃x_{1}^{i} ⋯ ∃x_{n_{x}}^{i}∀y_{1}^{i} ⋯ ∀y_{n_{y}}^{i}E_{i}. Construct a PAP P_{i} = ⟨V_{i}, H_{i}, M_{i}, T_{i}⟩ where V_{i} = {x_{1}^{i}, …, x_{n_{x}}^{i}} ∪ {x_{1}^{′i}, …, x_{n_{x}}^{′i}} ∪{y_{1}^{i}, …, y_{n_{y}}^{i}} ∪ {s^{i}} analogous to the PAP P in the proof of Theorem 4.2 such that Sol(P_{i}) ≠ ∅ iff Φ_{i} ∈ QBF_{2,∃}. Then, apply a transformation to P_{i} similar to the one described in the proof of Theorem 4.3 as follows. Let h_{1}^{i}, h_{2}^{i}, a_{1}^{i}, …, a_{r}^{i}, m^{i} be new variables, where r = |H_{i}| + 1, and construct P^{i} = ⟨V^{i}, H^{i}, M^{i}, T^{i}⟩ where

V^{i} = V_{i} ∪ {h_{1}^{i}, h_{2}^{i}, a_{1}^{i}, …, a_{r}^{i}, m^{i}}
H^{i} = H_{i} ∪ {h_{1}^{i}, h_{2}^{i}, a_{1}^{i}, …, a_{r}^{i}}
M^{i} = M_{i} ∪ {m^{i}}
T^{i} = {¬h_{1}^{i} ∨ F : F ∈ T_{i}} ∪ {h_{2}^{i} → m : m ∈ M_{i}} ∪
{¬h_{1}^{i} ∨ ¬h_{2}^{i}, h_{1}^{i} → m^{i}, h_{2}^{i} ∧ a_{1}^{i} ∧ ⋯ ∧ a_{r}^{i} → m^{i}}.

Clearly, T^{i} is consistent and can be constructed in polynomial time. Note that the only substantial difference between this transformation and the one employed in the proof of Theorem 4.3 is that h_{2}^{i} ∧ a_{1}^{i} ∧ ⋯ ∧ a_{r}^{i} → m^{i} replaces h_{2}^{i} → m^{i}. It is straightforward to verify that

Sol(P^{i}) = {S ∪ {h_{1}^{i}} ∪ A : S ∈ Sol(P_{i}), A ⊆ {a_{1}^{i}, …, a_{r}^{i}}} ∪
{ {h_{2}^{i}, a_{1}^{i}, …, a_{r}^{i}} ∪ H′ : H′ ⊆ H_{i}}

and that either for some S ∈ Sol(P^{i}), it holds that T^{i} ∪ S ⊧ h_{1}^{i} ∧ ¬h_{2}^{i} (in this case, Φ_{i} ∈ QBF_{2,∃}) or for all S ∈ Sol(P^{i}), it holds that T^{i} ∪ S ⊧ ¬h_{1}^{i} ∧ h_{2}^{i} (resp. Φ_{i} ∉ QBF_{2,∃}). Since for all S ∈ Sol(P_{i}), |S| < r, we thus get Φ_{i} ∈ QBF_{2,∃} iff for all S ∈ Sol_{≤}(P^{i}), h_{1}^{i} ∈ S, and Φ_{i} ∉ QBF_{2,∃} iff for all S ∈ Sol_{≤}(P^{i}), h_{2}^{i} ∈ S. Let P^{1}, …, P^{m} be the PAPs constructed that way. Then, define P = ⟨H, V, M, T ⟩, where V = ⋃_{i} V^{i}, H = ⋃_{i} H^{i}, M = ⋃_{i} M^{i}, and T = ⋃_{i} T^{i}. Since V^{i} ∩ V^{j} = ∅ for 1 ≤ i < j ≤ m, we obtain by Lemma 2.2 that Sol_{⪯}(P) = {S_{1} ∪ ⋯ ∪ S_{m} : S_{i} ∈ Sol_{⪯}(P^{i}), 1 ≤ i ≤ m} if ⪯ is equality or ≤. Since T^{i} ⊆ T, we thus have the following:

1. for all S ∈ Sol(P), either T ∪ S ⊧ h_{1}^{i} ∧ ¬h_{2}^{i} or T ∪ S ⊧ ¬h_{1}^{i} ∧ h_{2}^{i},

2. Φ_{i} ∈ QBF_{2,∃} iff for all S ∈ Sol_{≤}(P), h_{1}^{i} ∈ S,

3. Φ_{i} ∉ QBF_{2,∃} iff for all S ∈ Sol_{≤}(P), h_{2}^{i} ∈ S.

Now let o, e, h_{o}, h_{e} be new variables. Define

ODD_{m} = {h_{1}^{1} ∧ ⋯ ∧ h_{1}^{2k+1} ∧ h_{2}^{2k+2} ∧ ⋯ ∧ h_{2}^{m} → o : 0 ≤ k < m/2},
EVEN_{m} = {h_{1}^{1} ∧ ⋯ ∧ h_{1}^{2k} ∧ h_{2}^{2k+1} ∧ ⋯ ∧ h_{2}^{m} → e : 0 ≤ k ≤ m/2}.

Note that the theories ODD_{m}, EVEN_{m} can be constructed in polynomial time. Let S ∈ Sol(P). From 1.) it follows that if {α → β, γ → δ} ⊆ ODD_{m} ∪ EVEN_{m} and T ∪ S ⊧ α ∧ β, then α = β, γ = δ; hence, T ∪ S |̸= o ∧ e. Furthermore, since we have that Φ_{i} ∉ QBF_{2,∃} implies Φ_{i+1} ∉ QBF_{2,∃}, 1 ≤ i < m, it holds that for all S ∈ Sol_{≤}(P), T ∪ODD_{m} ∪EVEN_{m} ∪S ⊧ o iff ν = ν(Φ_{1}, …, Φ_{m}) is odd and T ∪ODD_{m} ∪EVEN_{m} ∪S ⊧ e iff ν is even. Now construct the PAP P′ = ⟨V′, H′, M′, T′⟩, where

V′ = V ∪ {o, e, h_{o}, h_{e}},
H′ = H ∪ {h_{o}, h_{e}}, M′ = M ∪ {o, e},
T′ = T ∪ ODD_{m} ∪ EVEN_{m} ∪ {h_{e} → o, h_{o} → e}.

Since for each S ∈ Sol(P), T′ ∪ S |̸= o ∧ e and h_{o}, h_{e} ∉ V, we have that S ∈ Sol(P′) fulfills S − {h_{o}, h_{e}} ∈ Sol(P) and S ∩ {h_{o}, h_{e}} ≠ ∅. Consequently, Sol_{≤}(P′) = {S ∪ {h_{o}} : S ∈ Sol_{≤}(P)} if ν is odd and Sol_{≤}(P′) = {S ∪ {h_{e}} : S ∈ Sol_{≤}(P)} if ν is even. Therefore, h_{o} is ≤-relevant (and h_{e} is ≤-dispensable) for P′ iff ν is odd. Since P′ can be constructed in polynomial time from Φ_{1}, …, Φ_{m} and since H′ ∪M′ = V′ already holds, it remains to show that T′ can be transformed efficiently into clausal form. Since E_{i} is in DNF, 1 ≤ i ≤ n, however, each T_{i} in the first step of the transformation can efficiently be transformed into clausal form (see the proof of Theorem 4.2); hence, it is clear that T′ can be efficiently transformed into clausal form. Whence the theorem is proved. □

Prioritization

Note that the complexity of ⪯-relevance and ⪯-dispensability checking slightly increases by restricting the acceptable solutions from arbitrary to ≤-solutions. A substantial increase happens if we introduce priorities among the hypotheses. This can be accomplished by introducing priority levels, in the same way as in [25] and [30] in the context of theory update, in prioritized circumscription [46], and in the preferred subtheories approach for default reasoning [3]. The general idea is to divide the hypotheses into levels of priority P_{1}, …, P_{k} and to eliminate, starting from P_{1}, level by level, those solutions that are not most preferable on the current priority level.

Definition 4.1 Let H be a finite set and ⪯ be a preorder defined on 2^{H}, and let P = ⟨P_{1}, …, P_{k}⟩, k ≥ 1, such that H = P_{1} ∪ ⋯ ∪ P_{k}, , where P_{i} ∩ P_{j} = ∅, 1 ≤ i < j ≤ k. Then, define the relation ⪯_{P} on 2^{H} by A ⪯_{P} B iff A = B or there exists i ∈ {1, …, k} such that A ∩ P_{j} ⪯ B ∩ P_{j}, B ∩ P_{j} ⪯ A ∩ P_{j}, for all 1 ≤ j < i, and A ∩ P_{i} ⪯ B ∩ P_{i}, B ∩ P_{i} ⪯̸ A ∩ P_{i}.

Intuitively, A ⪯_{P} B iff A and B are of equal preference on P_{1}, …, P_{i−1} and A is preferred over B on P_{i}. Notice that e.g. in case of ≤_{P}, this is equivalent with |A ∩ P_{j}| = |B ∩ P_{j}| for 1 ≤ j < i and |A ∩ P_{i}| < |B ∩ P_{i}|. To give a concrete example, consider the motor vehicle example from the introduction again. Let the prioritization P = ⟨P_{1}, P_{2}⟩ on the hypotheses H = {rich mixture, lean mixture, low oil, low water} be defined by P_{1} = {low oil, rich mixture} and P_{2} = {low water, lean mixture}. Then,

{rich mixture, low water} ≤_{P} {rich mixture, low oil},

and

{rich mixture, low water} ≤_{P} {rich mixture, low water, low oil}.

Clearly, ⪯_{P} collapses to ⪯ if P = ⟨P_{1}⟩, that is no priorities between hypotheses exist. It is not difficult to verify that ⪯_{P} defines a preorder on 2^{H}. Furthermore, ⪯_{P} is irredundant if ⪯ is irredundant, and ⪯_{P} is polynomial-time decidable if ⪯ is. We consider ⊆_{P} and ≤_{P}, that is the method of priorities applied to irredundant and minimum sized solutions. In both cases, the complexity of relevance and dispensability checking increases. For ≤_{P}, however, the problems remain at the second level of PH, while for ⊆_{P} they migrate to the third level. In particular, ⊆_{P} is among the computationally hardest preference orders with respect to relevance and dispensability checking, provided that deciding solution preference is polynomial. An upper bound for this general case is the following.

Lemma 4.7 Let P = ⟨V, H, M, T ⟩ be a PAP and assume deciding ⪯ is polynomial. Then, deciding whether a given hypothesis h is ⪯-relevant (resp. ⪯-dispensable) for P is in Σ_{3}^{P}.

Proof. Since ⪯ is polynomial and deciding S ∈ Sol(P) is in Δ_{2}^{P} (Proposition 4.1), deciding whether S ⊆ H satisfies S ∈ Sol_{⪯}(P) is thus in Π_{2}^{P}. Consequently, verifying a guess for S ∈ Sol_{⪯}(P) such that h ∈ S (resp. h ∉ S) is in Δ_{3}^{P}, from which membership of the problems in Σ_{3}^{P} follows. □

Note that this result still holds if deciding ⪯ is allowed to be in Δ_{2}^{P} instead of P = Δ_{1}^{P}. Nevertheless, already preference orders in P may lead to Σ_{3}^{P} -hardness.

In particular, this holds for ⊆_{P}, which is polynomial-time decidable and therefore not a source of intractability. For P = ⟨P_{1}⟩, we have from the results on ⊆-preference that ⊆_{P} -relevance and ⊆_{P} -dispensability checking are in this case Σ_{2}^{P} -complete. An additional priority level suffices to unchain the worst case complexity of these problems, which is Σ_{3}^{P} -completeness. This complexity increase may be intuitively explained by the loss of the computationally benign property of ⊆-solutions in Proposition 2.1, which implied with Proposition 4.1 a polynomial test for deciding whether a solution S is a ⊆-solution using an NP oracle. In case of at least two priority groups, deciding whether S is a ⊆_{P} -solution is Π_{2}^{P} -complete and thus more complex.

Theorem 4.8 Deciding ⊆_{P} -relevance and ⊆_{P} -dispensability of a given hypothesis h for a P = ⟨V, H, M, T ⟩ is Σ_{3}^{P} -complete. Σ_{3}^{P} -hardness holds even if P = ⟨P_{1}, P_{2}⟩. The same holds if T is in clausal form.

Proof. By Lemma 4.7, it remains to show Σ_{3}^{P} -hardness. We show this by a ≤_{m}^{p}- reduction of deciding Φ ∈ QBF_{3,∃} for a QBF Φ. Let without loss of generality Φ = ∃x_{1} ⋯ ∃x_{n_{x}}∀y_{1} ⋯ ∀y_{n_{y}}∃z_{1} ⋯ ∃z_{n_{z}}E. We define a PAP P = ⟨V, H, M, T ⟩ as follows. Let H_{x} = {x_{1}, x′_{1}, …, x_{n_{x}}, x′_{n_{x}}}, H_{y} = {y_{1}, y′_{1}, …, y_{n_{y}}, y′_{n_{y}}}, H_{z} = {z_{1}, …, z_{n_{z}}}, M_{x} = {r_{1}, …, r_{n_{x}}}, M_{y} = {w_{1}, …, w_{n_{y}}}, and let p, s, t be new variables. Define

V = H_{x} ∪ H_{y} ∪ H_{z} ∪ M_{x} ∪ M_{y} ∪ {p, s, t}
H = H_{x} ∪ H_{y} ∪ {p, s}
M = M_{x} ∪ M_{y} ∪ {t}
T = {¬x_{i} ∨ ¬x′_{i}, x_{i} → r_{i}, x′_{i} → r_{i} : 1 ≤ i ≤ n_{x}} ∪
{y_{i} ∧ y′_{i} ↔ ¬s, y_{i} ∧ y′_{i} → w_{i}, s → w_{i} : 1 ≤ i ≤ n_{y}} ∪
{¬s ∧ p → t, ¬E ∧ s → t}.

Note that T is consistent and constructible in polynomial time. In what follows, let X = {x_{1}, …, x_{n_{x}}}, Y = {y_{1}, …, y_{n_{y}}}. We first observe that for each S ∈ Sol(P), either x_{i} ∈ S or x′_{i} ∈ S must hold, for 1 ≤ i ≤ n_{x}, since otherwise T ∪ S |̸= r_{i}; consequently, either T ∪ S ⊧ x_{i} or T ∪ S ⊧ ¬x_{i}. Let ϕ_{S}(X) denote the truth assignment defined this way. On the other hand, let ψ(X) be any truth assignment and define

S_{ψ} = {x_{i} : ψ(x_{i}) = true, 1 ≤ i ≤ n_{x}} ∪ {x′_{i} : ψ(x_{i}) = false, 1 ≤ i ≤ n_{x}} ∪ H_{y} ∪ {p}.

It is straightforward to verify that S_{ψ} ∈ Sol(P) holds for every ψ(X). Moreover, S_{ψ} ∈ Sol_{⊆}(P) holds. Indeed, T ∪ (S_{ψ} − {p}) is consistent with ¬t, both T ∪ (S_{ψ} − {x_{i}}) and T ∪ (S_{ψ} − {x′_{i}}) are consistent with ¬r_{i}, for all x_{i}, x′_{i} ∈ S_{ψ}, and both T ∪ (S_{ψ} − {y_{i}}), T ∪ (S_{ψ} − {y′_{i}}) are consistent with ¬w_{i}, for all y_{i}, y′_{i} ∈ S_{ψ}.

Now define two priority levels P = ⟨P_{1}, P_{2}⟩, where P_{1} = H − {s} and P_{2} = {s}. Then, each S_{ψ} is a maximal solution under ⊆_{P}, that is, no S ∈ Sol(P), S ≠ S_{ψ}, satisfies S_{ψ} ⊆_{P} S. On the other hand, each S ∈ Sol(P) must satisfy S ⊆_{P} S_{ϕ_{S}}, since if S ≠ S_{ϕ_{S}}, then S ∩ P_{1} ⊂ S_{ϕ_{S}} ∩ P_{1} holds. Note that since S_{ϕ_{S}} ∈ Sol_{⊆}(P), we have that for each S ∈ Sol(P), s ∈ S holds iff S ≠ S_{ϕ_{S}}. We claim that for every ψ(X), S_{ψ} ∈ Sol_{⊆_{P}} (P) iff Φ_{ψ} = ∀y_{1} ⋯ ∀y_{n_{y}}∃z_{1} ⋯ ∃z_{n_{x}}E_{ψ(X)} ∈ QBF_{2,∀} holds. Assume that Φ_{ψ} ∉ QBF_{2,∀}. Then, a μ(Y) exists such that ∀z_{1} ⋯ ∀z_{n_{z}}(¬E_{ψ(X)})_{μ(Y)} ∈ QBF_{1,∀}. Define a set S_{ψ,μ} as follows:

S_{ψ,μ} = {x_{i} : ψ(x_{i}) = true, 1 ≤ i ≤ n_{x}} ∪ {x′_{i} : ψ(x_{i}) = false, 1 ≤ i ≤ n_{x}} ∪
{y_{i} : μ(y_{i}) = true, 1 ≤ i ≤ n_{y}} ∪ {y′_{i} : μ(y_{i}) = false, 1 ≤ i ≤ n_{y}} ∪ {s}.

Then, S_{ψ,μ} ∈ Sol(P) holds. Indeed, T ∪ S_{ψ,μ} is consistent, and T ∪ S_{ψ,μ} logically implies y_{i} ≡ μ(y_{i}), 1 ≤ i ≤ n_{y}, and x_{i} ≡ ψ(x_{i}), 1 ≤ i ≤ n_{x}; consequently, T ∪S_{ψ,μ} ⊧ ¬E ∧s. Thus it is clear that T ∪S_{ψ,μ} ⊧ M. Note that S_{ψ,μ} ≠ S_{ψ} and S_{ψ,μ} ⊆_{P} S_{ψ}; hence, S_{ψ} ∉ Sol_{⊆_{P}} (P). Conversely, assume S_{ψ} ∉ Sol_{⊆_{P}} (P) holds for ψ(X). Let S ∈ Sol(P) such that S ≠ S_{ψ}, S ⊆_{P} S_{ψ} holds. Then clearly, ϕ_{S}(X) is identical to ψ(X); from above, we know s ∈ S. Hence, {y_{i}, y′_{i}} ⊈ S holds, for 1 ≤ i ≤ n_{y}. Let R = {y_{i} : y_{i} ∈ S, 1 ≤ i ≤ n_{y}}∪ {¬y_{i} : y_{i} ∉ S, 1 ≤ i ≤ n_{y}}. Then, T ∪ S ∪ R is consistent, and since s ∈ S, T ∪ S ⊧ t, we have T ∪ S ∪ R ⊧ ¬E. Let μ(Y) be defined by μ(y_{i}) = true, y_{i} ∈ R, and μ(y_{i}) = false, y_{i} ∉ R, 1 ≤ i ≤ n_{y}. Then, we have that (¬E_{ϕ_{S}(X)})_{μ(Y)}, that is (¬E_{ψ(X)})_{μ(Y)} is a tautology, hence ∀z_{1} ⋯ ∀z_{n_{z}}(¬E_{ψ(X)})_{μ(Y)} ∈ QBF_{1,∀}. This means, however, that Φ_{ψ} ∉ QBF_{2,∀} holds, and the claim is proved. From the claim and S_{ψ} ∈ Sol_{⊆}(P), it follows that p is ⊆_{P} -relevant iff Φ ∈ QBF_{3,∃} holds. Hence Σ_{3}^{P} -hardness of deciding ⊆_{P} -relevance is proved. It is straightforward to verify that for each S ∈ Sol_{⊆_{P}} (P), s ∈ S iff p ∉ S. Hence, p is ⊆_{P} -relevant for P iff s is ⊆_{P} -dispensable for P, which proves Σ_{3}^{P} -hardness of ⊆_{P} -dispensability checking. Since we may without loss of generality assume that E is in CNF [72], it is clear that T can be efficiently rewritten in clausal form. Thus we have the theorem. □

The results from above suggest that this result could be strengthened to the case H∪M = V; a more involved proof would be necessary, however. Now let us consider the effect of the method of priorities on ≤. It appears that the complexity of relevance and dispensability checking increases to Δ_{3}^{P} [O(log n)]-completeness. An intuitive explanation for this increase is that checking whether a solution S is a ≤_{P} - solution requires to compute for each priority group P_{i} the cardinality of S on this group, which can be efficiently done using a Σ_{2}^{P} oracle. Since the cardinality of S on P_{i} depends on the cardinality of S on all P_{j} with j < i, computing the cardinality of a ≤_{P} -solution on all priority groups requires in the worst case at least linearly many oracle calls, which contrasts with the logarithmically many oracle calls for computing the size of a ≤-solution.

Theorem 4.9 Let P be a PAP and let P = ⟨P_{1}, …, P_{k}⟩ be a prioritization. Deciding ≤_{P} -relevance as well as ≤_{P} -dispensability of a hypothesis h for P is Δ_{3}^{P} -complete. Δ_{3}^{P} - hardness holds even if H ∪ M = V and T is in clausal form.

Proof. Note that for S, S′ ∈ Sol(P), S ≤_{P} S′ iff S = S′ or for the least i such that |S ∩ P_{i}| ≠ |S′ ∩ P_{i}|, |S ∩ P_{i}| < |S′ ∩ P_{i}| holds. Membership in Δ_{3}^{P} is shown as follows. For all S, S′ ∈ Sol_{≤_{P}} (P) we have |S ∩ P_{i}| = |S′ ∩ P_{i}|, 1 ≤ i ≤ k. Let s_{i} = |S ∩ P_{i}| for such an S, 1 ≤ i ≤ k. First, s_{1}, …, s_{i}, …, s_{k} are determined in that order, where s_{i} is computed by queries to the Σ_{2}^{P} oracle (e.g. in a binary search) whether there exists S ∈ Sol(P) such that |S ∩ P_{j}| = s_{j}, for 1 ≤ j < i, and |S ∩ P_{i}| ≤ r. This can be done with polynomially many Σ_{2}^{P} oracle calls. Then, the Σ_{2}^{P} oracle is queried whether there exists S ∈ Sol(P) such that |S ∩ P_{i}| = s_{i}, 1 ≤ i ≤ k and h ∈ S (resp. h ∉ S). Note that this procedure also works correctly if Sol(P) = ∅ (s_{1}, …, s_{k} can be arbitrary). Let ⟨x_{1}, …, x_{n_{x}}⟩ be in lexicographical order. Then, Δ_{3}^{P} -hardness is shown by a reduction from deciding whether the with respect to ⟨x_{1}, …, x_{n_{x}}⟩ lexicographically maximum truth assignment ϕ(X), X = {x_{1}, …, x_{n_{x}}}, such that Φ_{ϕ} = ∀y_{1} ⋯ ∀y_{n_{y}}E_{ϕ(X)} ∈ QBF_{1,∀} satisfies ϕ(x_{n_{x}}) = true (where such a ϕ(X) is known to exist). Define a PAP P = ⟨V, H, M, T ⟩ as follows. Let X = {x_{1}, …, x_{n_{x}}}, X′ = {x′_{1}, …, x′_{n_{x}}}, Y = {y_{1}, …, y_{n_{y}}}, U = {u_{1}, …, u_{n_{x}}}, and let s be an additional variable. Define

V = X ∪ X′ ∪ Y ∪ U ∪ {s}
H = X ∪ X′
M = U ∪ Y ∪ {s}
T = {¬x_{i} ∨ ¬x′_{i}, x_{i} → u_{i}, x′_{i} → u_{i} : 1 ≤ i ≤ n_{x}} ∪
{E → s ∧ y_{1} ∧ ⋯ ∧ y_{n_{y}}, s → y_{1} ∧ ⋯ y_{n_{y}}}

Note that P is close to the PAP in the proof of Theorem 4.2. Let for every truth assignment ϕ(X),

S_{ϕ} = {x_{i} : ϕ(x_{i}) = true, 1 ≤ i ≤ n_{x}} ∪ {x′_{i} : ϕ(x_{i}) = false, 1 ≤ i ≤ n_{x}}.

Then, Sol(P) = {S_{ϕ} : ∀y_{1} ⋯ ∀y_{n_{y}}E_{ϕ(X)} ∈ QBF_{1,∀}}. This can be shown easily along the line of the proof of Theorem 4.2. Define a prioritization P = ⟨P_{1}, …, P_{2n_{x}}⟩ as follows: P_{2i−1} = {x′_{i}}, P_{2i} = {x_{i}}, for 1 ≤ i ≤ n_{x}. P prefers every S_{ϕ} with x_{1} ∈ S_{ϕ} (i.e. ϕ(x_{1}) = true) over every S_{ψ} with x_{1} ∉ S_{ψ} (ψ(x_{1}) = false) etc. Therefore, Sol_{≤_{P}} (P) = {S_{ϕ_{m}}}, where ϕ_{m}(X) is with respect to ⟨x_{1}, …, x_{n_{x}}⟩ the lexicographically maximum ϕ(X) such that ∀y_{1} ⋯ ∀y_{n_{y}}E_{ϕ(X)} ∈ QBF_{1,∀}. Therefore, x_{n_{x}} is ≤_{P} -relevant (and x′_{n_{x}} is ≤_{P} -dispensable) for P iff ϕ_{m}(x_{n_{x}}) = true. Since we may assume without loss of generality that E is in DNF [44], T can be rewritten in clausal form in polynomial time (to rewrite {E → s ∧ y_{1} ⋯ ∧ y_{n_{y}}, s → y_{1} ∧ ⋯ ∧ y_{n_{y}}}, see proof of Theorem 4.2). Since P, P are polynomial-time constructible and H ∪ M = V, we thus have the theorem. □

Penalization

Yet another variant of solution preference, but not completely unrelated to the methods from above, is minimization of solution penalty. The method of penalties works as follows. Each hypothesis h has attached a penalty p(h) (a positive integer), and the penalty p(S) of a solution S ∈ Sol(P) is defined as p(S) = ∑_{h∈S} p(S), the sum of the penalties of its hypotheses. The solutions S with smallest penalty, i.e. for which p(S) is a minimum, are accepted. Thus, solution preference by penalties defines a kind of weighted abduction, cf. [34]. Definition 4.2 Let P = ⟨V, H, M, T ⟩ be a PAP, and let p : H → {1, 2 …} be a penalty attachment, which is extended to 2^{H} by p(H′) = ∑_{h∈H′} p(h), for all H′ ⊆ H. The preference relation ⊑_{p} on Sol(P) is defined by S ⊑_{p} S′ iff p(S) ≤ p(S′). Clearly, ⊑_{p} is a preorder and hence admissible as solution preference criterion. It appears that ⊑_{p}-preference is a generalization of the smallest cardinality preference ≤. Indeed, ≤ is obtained if p(h) = p(h′), for all h, h′ ∈ H. It turns out that ⊑_{p}-preference also covers the method of priorities applied to ≤-preference. To see this, let P = ⟨V, H, M, T ⟩ and assume a prioritization P = ⟨P_{1}, …, P_{k}⟩. An equivalent penalty attachment p^{P} can be defined as follows. Let d = 1 + max{|P_{i}| : 1 ≤ i ≤ k}, and let p^{P} (h) = d^{k−i}, where h ∈ P_{i}, for each h ∈ H. Then,

Proposition 4.10 Sol_{⊑_{p^{P}}} (P) = Sol_{≤_{P}} (P).

Proof. For 1 ≤ i ≤ k, it holds that p^{P} (P_{i} ∪⋯∪P_{k}) ≤ (d−1) ∑_{j=i}^{k} d^{k−j} = d^{k−i+1} −1 < p^{P} (h), for each h ∈ P_{1} ∪ ⋯ ∪ P_{i−1}. Hence if s_{i} denotes |P_{i} ∩ S|, 1 ≤ i ≤ k, for some S ∈ Sol_{≤_{P}} (P), then it is straightforward to show that for each S ∈ Sol_{⊑_{p^{P}}} (P), and 1 ≤ i ≤ k, |P_{i} ∩ S| = s_{i} holds, from which the proposition follows immediately. □ If numbers are represented in binary, we get thus the following result.

Theorem 4.11 Let P = ⟨V, H, M, T ⟩ be a PAP and p be a penalty attachment to H, which is part of the input. Deciding whether h is ⊑_{p}-relevant (resp. ⊑_{p}-dispensable) is Δ_{3}^{P} -complete. Δ_{3}^{P} -hardness holds even if H ∪ M = V and T is in clausal form.

Proof. The minimum solution penalty s = min{p(S) : S ∈ Sol(P)} is computable by binary search in O(n) steps with a Σ_{2}^{P} oracle, where n is the input size. Then, a single query to the Σ_{2}^{P} oracle whether there exists S ∈ Sol(P), such that |S| = s and h ∈ S (resp. h ∉ S) decides the problem. Again, this procedure works correctly if Sol(P) = ∅. Hence the problem is in Δ_{3}^{P}. Hardness for Δ_{3}^{P} under the indicated restrictions follows from Theorem 4.9 and, if numbers are represented in binary, the polynomial time computability of p^{P} from a prioritization P. □ Note that if numbers are required to be in unary (tally) notation, then O(log n) oracle calls suffice to determine the minimum solution penalty s. In that case, the problems fall back to Δ_{3}^{P} [O(log n)] and are complete for this class.

5 Horn abduction

So far, we have considered abduction in the full propositional case, that is, the theory T may contain arbitrary propositional formulas. In many cases, however, the possible formulas in T may be restricted to a certain formula class. One of the most important restriction on formulas is the Horn property, that is the formula is a clause with at most one positive literal. It is well-known that the co-NP-complete implication problem T_{1} ⊧ T_{2} for arbitrary propositional theories becomes polynomial if T_{1} and T_{2} are Horn theories, i.e. contain only Horn clauses. As a further restriction, it is sometimes postulated that Horn clauses are definite, that is each clause has exactly one positive literal. Note that this restriction is of particular interest for modeling abduction problems, since formulas of type c_{1} ∧ ⋯ ∧ c_{n} → e are often adequate to describe interrelationships between causes and effects.

Definition 5.1 A PAP P = ⟨V, H, M, T ⟩ is Horn (resp. definite Horn) iff T is a set of Horn clauses (resp. definite Horn clauses).

This section is devoted to the complexity of PAPs in the Horn case and the definite Horn case. We consider the effect of these restrictions to ⪯-relevance and ⪯-dispensability checking under the various preference orders ⪯ considered in the previous section. Generally spoken, it turns out that the complexity of those problems is lowered at least by one level of PH. This is due to the elimination of one source of intractability.

Proposition 5.1 If P = ⟨V, H, M, T ⟩ is a Horn PAP, checking S ∈ Sol(P) for S ⊆ H is polynomial.

Proof. Indeed, e.g. by the results in [19], deciding whether T ∪ S is consistent and T ∪ H ⊧ M holds is polynomial. □

The benign properties of definite Horn theories allow additional complexity reduction to tractability in some cases, while in the remaining cases the complexity compared to the general Horn case is not affected. Some of the intractability results of this section appear in other contexts [6, 69, 4] with different proofs.

Deciding Sol(P) ≠ ∅

Theorem 5.2 [69] Let P = ⟨V, H, M, T ⟩ be a Horn PAP. Deciding Sol(P) ≠ ∅ is NPcomplete. NP-hardness holds even if H ∪ M = V.

Proof. (Sketch) Membership of this problem in NP is clear since a guess for S ∈ Sol(P) is verifiable in polynomial time. We show NP-hardness by a transformation from the well-known satisfiability problem (SAT), cf. [29]. Let C = {C_{1}, …, C_{m}} be a set of propositional clauses on X = {x_{1}, …, x_{n}}.

Let X′ = {x′_{1}, …, x′_{n}}, G = {g_{1}, …, g_{m}}, Z = {z_{1}, …, z_{n}} be sets of new variables. Then, the PAP P = ⟨V, H, M, T ⟩, where

V = X ∪ X′ ∪ G ∪ Z, H = X ∪ X′, M = G ∪ Z,
T = {¬x_{i} ∨ ¬x′_{i}, x_{i} → z_{i}, x′_{i} → z_{i} : 1 ≤ i ≤ n} ∪

⋃_{i=1}^{m}({x_{j} → g_{i} : x_{j} ∈ C_{i}} ∪ {x′_{j} → g_{i} : ¬x_{j} ∈ C_{i}}),

has a solution iff C is satisfiable. Note that H ∪ M = V; since P is polynomial time constructible, we have the result. □

It is well-known that deciding Sol(P) ≠ ∅ for a definite Horn PAP P is possible in polynomial time, which follows immediately from the following property.

Proposition 5.3 [28, 6] Let P = ⟨V, N, M, T ⟩ be a definite Horn PAP. Then, S ∈ Sol(P) implies S′ ∈ Sol(P), for all S ⊆ S′ ⊆ H.

Corollary 5.4 If P = ⟨V, H, M, T ⟩ is a definite Horn PAP, then Sol(P) ≠ ∅ iff H ∈ Sol(P); hence by Proposition 5.1 deciding Sol(P) ≠ ∅ is polynomial.

Relevance, dispensability, and ⊆-preference

Theorem 5.5 Deciding if h is relevant (resp. dispensable) for a Horn PAP P is NPcomplete, and the same holds in case of ⊆-preference. In all cases, this may be strengthened to the case where H ∪ M = V.

Proof. Membership in NP is clear since verifying S ∈ Sol(P) and S ∈ Sol_{⊆}(P) is possible in polynomial time (Propositions 2.1 and 5.1). NP-hardness under the restriction is immediate by the construction of the PAP P′ from P in the proof of Theorem 4.3. If P is a Horn PAP, then P′ is easily transformed into a Horn PAP. Recall that h is relevant for P′ iff h′ is dispensable for P′ iff Sol(P) ≠ ∅; this carries over to ⊆-relevance of h and ⊆-dispensability of h′ for P′ (see proof of Theorem 4.4); whence the theorem. □

In case of a definite Horn PAP, the following holds.

Proposition 5.6 [28, 6] Let P = ⟨V, H, M, T ⟩ be a definite Horn PAP. Then, deciding whether a hypothesis h is relevant (resp. dispensable, ⊆-dispensable) for P is possible in polynomial time.

Proof. Indeed, by Proposition 5.3, h is in this case relevant iff H ∈ Sol(P), and h is dispensable as well as ⊆-dispensable iff H − {h} ∈ Sol(P). Thus by Proposition 5.1 the proposition follows. □

Testing whether h is ⊆-relevant is intractable even for definite Horn PAPs, however.

Theorem 5.7 [28] Deciding if h is ⊆-relevant for a definite Horn PAP P is NP-complete. NP-hardness holds even if H ∪ M = V.

Proof. (Sketch) The problem is clearly in NP. NP-hardness is shown in [28] by a straightforward ≤_{m}^{p}-reduction of the problem PRIME ATTRIBUTE NAME [29, p. 233]. We sketch here a simple ≤_{m}^{p}-reduction from SAT. Let C = {C_{1}, …, C_{r}} be a set of propositional clauses on variables x_{1}, …, x_{n}. Let literals correspond to hypotheses (x_{i} and ¬x_{i} to h_{i} and h′_{i}, respectively) and clauses C_{j} to manifestations m_{j}. Include an additional hypothesis h^{∗} and an additional manifestation m^{∗}, i.e. H = {h_{1}, h′_{1}, …, h_{n}, h′_{n}, h^{∗}} and M = {m_{1}, …, m_{r}, m^{∗}}. Let T consist of the following clauses:

• h_{i} ∧ h′_{i} → m, for each i, 1 ≤ i ≤ n, and m ∈ M;

• h_{i} → m_{j} (resp. h′_{i} → m_{j}) for each i and j, 1 ≤ i ≤ n, 1 ≤ j ≤ r, such that x_{i} (resp. ¬x_{i}) appears in C_{j};

• h^{∗} → m^{∗}.

Now h^{∗} is in a ⊆-minimal solution of the PAP P = ⟨H ∪ M, H, M, T ⟩ if and only if C is satisfiable. Otherwise, only {h_{i}, h′_{i}} for each i with 1 ≤ i ≤ n are ⊆-minimal solutions. Hence the result follows. □

≤-preference

The smallest cardinality criterion makes both checking for dispensability and relevance become more complex, even for definite Horn PAPs. In the proof of the next result, we refer to the following lemma, which is proved in the appendix.

Lemma 5.8 Let C = {C_{1}, …, C_{m}} be a clause set on variables X and let k ∈ {1, …, m}. Call a truth assignment ϕ(X) csat-maximum for C iff ϕ(X) satisfies a maximum number of clauses in C. Then, deciding if every csat-maximum ϕ(X) for C fulfills V_{ϕ}(C_{k}) = true is Δ_{2}^{P} [O(log n)]-complete.

Theorem 5.9 Let P = ⟨V, H, M, T ⟩ be a Horn PAP. Deciding if h is ≤-dispensable (resp. ≤-relevant) for P is Δ_{2}^{P} [O(log n)]-complete. Δ_{2}^{P} [O(log n)]-hardness holds even if P is definite Horn and H ∪ M = V.

Proof. Membership in Δ_{2}^{P} [O(log n)] is shown for both problems analogous to the full propositional case (see proof of Theorem 4.6); since by Proposition 5.1 checking S ∈ Sol(P) is polynomial, an NP oracle replaces the Σ_{2}^{P} oracle. We show hardness for Δ_{2}^{P} [O(log n)] under the restriction to definite Horn PAPs by a ≤_{m}^{p}-reduction from the problem in Lemma 5.8. Let C = {C_{1}, …, C_{m}}, X = {x_{1}, …, x_{n}}, and k ∈ {1, …, m}. We define a definite Horn PAP P = ⟨V, H, M, T ⟩ as follows. Let X^{i} = {x_{1}^{i}, …, x_{m}^{i}}, X^{′i} = {x_{1}^{′i}, …, x_{m}^{′i}}, 1 ≤ i ≤ n, W = {w_{1}, …, w_{n}}, G = {g_{1}, …, g_{m+1}}, F = {f_{1}, …, f_{m+1}} be sets of new variables. Define

V = X^{1} ∪ X^{′1} ⋯ ∪ X^{n} ∪ X^{′n} ∪ W ∪ G ∪ F
H = X^{1} ∪ X^{′1} ⋯ ∪ X^{n} ∪ X^{′n} ∪ F
M = W ∪ G
T = {x_{1}^{i} ∧ ⋯ ∧ x_{m}^{i} → w_{i}, x_{1}^{′i} ∧ ⋯ ∧ x_{m}^{′i} → w_{i} : 1 ≤ i ≤ n} ∪

{f_{i} → g_{i} : 1 ≤ i ≤ m + 1} ∪ {f_{k} → g_{m+1}}

⋃_{j=1}^{m}{x_{1}^{i} ∧ ⋯ ∧ x_{m}^{i} → g_{j} : x_{i} ∈ C_{j}, 1 ≤ i ≤ n} ∪

⋃_{j=1}^{m}{x_{1}^{′i} ∧ ⋯ ∧ x_{m}^{′i} → g_{j} : ¬x_{i} ∈ C_{j}, 1 ≤ i ≤ n}.

For every truth assignment ϕ(X), let

S_{ϕ} = {x_{1}^{i}, …, x_{m}^{i} : ϕ(x_{i}) = true, 1 ≤ i ≤ n} ∪ {x_{1}^{′i}, …, x_{m}^{′i} : ϕ(x_{i}) = false, 1 ≤ i ≤ n} ∪
{f_{i} : V_{ϕ}(C_{i}) = false, 1 ≤ i ≤ m}.

Note that S_{ϕ} ∪ {f_{m+1}} ∈ Sol(P), and, if V_{ϕ}(C_{k}) = false, S_{ϕ} ∈ Sol(P). Furthermore, if s denotes the minimum solution size, then nm + 1 ≤ s ≤ n(m + 1) holds. Indeed, for each S ∈ Sol(P) and 1 ≤ i ≤ n, X^{i} ⊆ S or X^{′i} ⊆ S must hold, and since f_{k} ∈ S or f_{m+1} ∈ S, s ≥ nm + 1 follows. On the other hand, S_{ϕ} ∪ {f_{1}, …, f_{m}} ∈ Sol(P) for each ϕ(X), hence s ≤ n(m + 1). Consequently, each S ∈ Sol_{≤}(P) fulfills S ∩ (X^{i} ∪ X^{′i}) = X^{i} or S ∩ (X^{i} ∪ X^{′i}) = X^{′i}, for 1 ≤ i ≤ n (if X^{i} ∪ X^{′i} ⊆ S, then |S| ≥ n(m + 1) + 1); let for S the truth assignment ϕ_{S}(X) be defined by ϕ_{S}(x_{i}) = true if X^{i} ⊆ S and ϕ_{S}(x_{i}) = false if X^{′i} ⊆ S, 1 ≤ i ≤ n. Clearly, A ⊇ S_{ϕ_{A}} holds for each A ∈ Sol_{≤}(P). It holds that f_{m+1} is ≤-relevant for P if and only if each csat-maximum ϕ(X) for C fulfills V_{ϕ}(C_{k}) = true. Assume f_{m+1} is ≤-irrelevant for P, that is, each S ∈ Sol_{≤}(P) satisfies f_{m+1} ∉ S. Now ϕ_{S}(X) must be csat-maximum for C: If ψ(X) satisfies more clauses in C than ϕ_{S}(X), then |S_{ψ} ∪ {f_{m} + 1}| ≤ |S| and consequently S_{ψ} ∪ {f_{m} + 1} ∈ Sol_{≤}(P) holds, which contradicts to the ≤-irrelevance of f_{m+1}. Thus ϕ_{S}(X) is csat-maximum for C, and since f_{k} ∈ S, we obtain V_{ϕ_{S}}(C_{k}) = false. Conversely, assume some ψ(X) such that V_{ψ}(C_{k}) = false is csat-maximum for C. Then, S_{ψ} ∈ Sol_{≤}(P) holds, since S_{ψ} ∈ Sol(P) and |S_{ϕ}| ≥ |S_{ψ}| for all truth assignments ϕ(X) and A ⊇ S_{ϕ_{A}} for each A ∈ Sol_{≤}(P). Now assume that there exists S ∈ Sol_{≤}(P) such that f_{m+1} ∈ S; then, |S| = |S_{ψ}| entails that |S ∩ {f_{1}, …, f_{m}}| < |S_{ψ} ∩ {f_{1}, …, f_{m}}|, which means ϕ_{S}(X) satisfies more clauses in C than ψ(X), which contradicts to the csat-maximality of ψ(X). Consequently, f_{m+1} is ≤-irrelevant for P.

It is easily verified that f_{m+1} is ≤-relevant for P iff f_{k} is ≤-dispensable for P. Since P is constructible in polynomial time and H ∪ M = V, we have the theorem. □

Prioritization

Now let us consider the effect of priority groups. Not much surprisingly, the method of priorities makes ⊆ and ≤ harder also in the full Horn case, such that the problems reside in PH one level below the general propositional case. The same holds in case of definite Horn PAPs, except for ⊆-relevance checking, which is not affected by the method of priorities. The upper bound for ⪯-dispensability and ⪯-relevance checking for general preference orders ⪯ is one level below that general propositional case.

Lemma 5.10 Let P = ⟨V, H, M, T ⟩ be a Horn PAP and ⪯ be a polynomial-time decidable preference order. Then, deciding ⪯-relevance and ⪯-dispensability is in Σ_{2}^{P}.

Proof. The proof is essentially the same as for Lemma 4.7. Since checking S ∈ Sol(P) and ⪯ are polynomial, verifying a guess for S ∈ Sol_{⪯}(P) such that h ∈ S (resp. h ∉ S) is in Δ_{2}^{P}. Hence membership in Σ_{2}^{P} follows. □

Priority groups on ⊆-preference lift the problems for Horn PAPs from the first up to the second level of PH.

Theorem 5.11 Let P be a Horn PAP and P = ⟨P_{1}, …, P_{k}⟩ be a prioritization. Deciding whether h is ⊆_{P} -relevant (resp. ⊆_{P} -dispensable) for P is Σ_{2}^{P} -complete. Σ_{2}^{P} -hardness holds even if k = 2 and H ∪ M = V.

Proof. Since ⊆_{P} is polynomial, by Lemma 5.10 it remains to show the hardness part. We show Σ_{2}^{P} -hardness by a ≤_{m}^{p}-reduction of deciding Φ ∈ QBF_{2,∀} for a QBF Φ = ∀x_{1} ⋯ ∀x_{n} ∃x_{n+1} ⋯ ∃x_{m}E, 1 ≤ n < m, to deciding ⊆_{P} -irrelevance (resp. ⊆_{P} -necessity) of a hypothesis for a Horn PAP P = ⟨V, H, M, T ⟩. We may assume that E = C_{1} ∧ ⋯ ∧ C_{l} is a conjunction of clauses C_{i}, cf. [72]. Now let X = {x_{1}, …, x_{m}}, X′ = {x′_{1}, …, x′_{m}}, R = {r_{1}, …, r_{m}}, G = {g_{1}, …, g_{m}}, and let h, h′, t be additional variables. Define

V = X ∪ X′ ∪ R ∪ G ∪ {h, h′, t}
H = X ∪ X′ ∪ {h, h′}
M = R ∪ G ∪ {t}
T = {¬x_{i} ∨ ¬x′_{i}, x_{i} → r_{i}, x′_{i} → r_{i} : 1 ≤ i ≤ m} ∪

⋃_{j=1}^{l}({x_{i} → g_{j} : x_{i} ∈ C_{j}, 1 ≤ i ≤ n} ∪ {x′_{i} → g_{j} : ¬x_{i} ∈ C_{j}, 1 ≤ i ≤ n})

∪{h → g_{i} : 1 ≤ i ≤ m} ∪ {¬h ∨ ¬h′, h → t, h′ → t}, and let P = ⟨P_{1}, P_{2}⟩, P_{1} = {x_{1}, x′_{1}, …, x_{n}, x′_{n}, h}, P_{2} = H − P_{1}. We first observe that each solution S ∈ Sol(P) must satisfy either x_{i} ∈ S, T ∪ S ⊧ x_{i} or x′_{i} ∈ S, T ∪ S ⊧ ¬x_{i}, for all 1 ≤ i ≤ m; denote by ϕ_{S}(X) the corresponding truth assignment to X. Moreover, either h or h′ must be in S. Let for every truth assignment ϕ(X),

S_{ϕ} = {x_{i} : ϕ(x_{i}) = true, 1 ≤ i ≤ m} ∪ {x′_{i} : ϕ(x_{i}) = false, 1 ≤ i ≤ m}.

Then,

Sol(P) = {S_{ϕ} ∪ {h} : ϕ = ϕ(X)} ∪ {S_{ϕ} ∪ {h′} : E_{ϕ(X)} is true }.

Let X_{n} = {x_{1}, …, x_{n}}. Then, S, S′ ∈ Sol(P′) satisfy S ⊆_{P} S′ or S′ ⊆_{P} S only if ϕ_{S}(X) and ϕ_{S′}(X) are identical over X_{n}. Since eliminating h has higher priority than eliminating h′, it is straightforward to verify that for every truth assignment ψ(X_{n}), all S ∈ Sol_{⊆_{P}} (P) such that ϕ_{S}(X) is on X_{n} identical to ψ(X_{n}) satisfy h ∉ S (and hence E_{ϕ_{S}(X)} is true, h′ ∈ S) iff ∃x_{n+1} ⋯ ∃x_{m}E_{ψ(X_{n})} ∈ QBF_{1,∃} holds. Consequently, h is ⊆_{P} -irrelevant for P iff Φ = ∀x_{1} ⋯ ∀x_{n}∃x_{n+1} ⋯ ∃x_{m}E ∈ QBF_{2,∀} holds. Furthermore, it is clear that h is ⊆_{P} -irrelevant for P iff h′ occurs in every ⊆_{P} -solution of P, i.e. h′ is ⊆_{P} -necessary for P. Clearly, P, P can be constructed in polynomial time. Since H ∪ M = V, we thus have the theorem. □

In case of definite Horn PAPs, we have the following results.

Theorem 5.12 Let P = ⟨V, H, M, T ⟩ be a PAP and let P = ⟨P_{1}, …, P_{k}⟩ be a prioritization on V. Deciding whether a hypothesis is ⊆_{P} -relevant is NP-complete. NP-hardness holds even if H ∪ M = V.

Proof. As checking whether S ⊆ H satisfies S ∈ Sol_{⊆_{P}} (P) is possible in polynomial time, membership in NP follows. Indeed, S ∈ Sol(P) fulfills S ∈ Sol_{⊆_{P}} (P) iff for each h ∈ S ∩ P_{i}, it holds that S ∪ P_{i+1} ∪ ⋯ ∪ P_{k} − {h} ∉ Sol(P), for 1 ≤ i ≤ k. NP-hardness under the restriction follows by Theorem 5.7. □

Theorem 5.13 Let P = ⟨V, H, M, T ⟩ be a definite Horn PAP and P = ⟨P_{1}, …, P_{k}⟩ be a prioritization. Deciding if h is ⊆_{P} -dispensable is NP-complete. NP-hardness holds even if k = 2 and H ∪ M = V.

Proof. A guess for S ∈ Sol_{⊆_{P}} (P) such that h ∉ S can be verified in polynomial time (cf. proof of Theorem 5.12), hence the problem is in NP. We show NP-hardness by a ≤_{m}^{p}-reduction of deciding whether h is ⊆_{P} -relevant for a definite Horn PAP P = ⟨V, H, M, T ⟩ to this problem. Let h′, m ∉ V be additional variables. Define P′ = ⟨V′, H′, M′, T′⟩ where V′ = V ∪ {h′, m}, H′ = H ∪ {h′}, M′ = M ∪ {m}, and T′ = T ∪ {h → m, h′ → m}. We observe that each S ∈ Sol(P) must contain h or h′. It is easily verified that for each S ∈ Sol_{⊆}(P) such that h ∈ S, it holds that S ∈ Sol_{⊆}(P′) and S − {h} ∪ {h′} ∉ Sol_{⊆}(P′); if h is ⊆-irrelevant for P, then Sol_{⊆}(P′) = {S ∪ {h}, S ∪ {h′} : S ∈ Sol_{⊆}(P)}. Now define a prioritization P = ⟨V′ − {h′}, {h′}⟩. Note that ⊆_{P} prefers those solutions that do not contain h (and hence contain h′). Thus it is not hard to see that h′ is ⊆_{P} - dispensable for P′ iff h is ⊆-relevant for P. Since by Theorem 5.12 we may assume that H ∪ M = V, we get H′ ∪ M′ = V′, and hence the theorem follows. □

Since in the definite Horn case priority groups on ⊆-preference do not affect the complexity of the problems, it remains to consider whether there is some polynomial time decidable preference ⪯ such that checking ⪯-relevance and ⪯-dispensability is at the second level of PH. It is not hard to find such a order, however.

Theorem 5.14 Let P be a definite Horn PAP and ⪯ be an arbitrary polynomial-time decidable solution preference. Deciding whether h is ⪯-relevant (resp. ⪯-dispensable) is Σ_{2}^{P} -complete.

Proof. By Lemma 5.10 it remains to show Σ_{2}^{P} -hardness. Let P = ⟨V, H, M, T ⟩ be a Horn PAP and P = ⟨P_{1}, …, P_{k}⟩ be a prioritization of H. Let T_{d} ⊆ T be the definite Horn clauses in T, and let v ∉ V be a distinguished variable. Define P′ = ⟨V′, H, M, T′⟩, where V′ = V ∪ {v}, T′ = T_{d} ∪ {C ∪ {v} : C ∈ T − T_{d}} ∪ {{¬v}}. Clearly, Sol(P) = Sol(P′). Define the definite Horn PAP P′′ = ⟨V′, H, M, T′ − {{¬v}}⟩, and let ⪯ on 2^{H} be defined by

A ⪯ B iff B ∉ Sol(P′) ∨ (A, B ∈ Sol(P′) ∧ A ⊆_{P} B).

Clearly, ⪯ is a polynomial time decidable preorder. Then, Sol_{⪯}(P′′) = Sol_{⊆_{P}} (P′) = Sol_{⊆_{P}} (P) holds if Sol(P) ≠ ∅, and in this case h is ⪯-relevant (resp. ⪯-dispensable) for P′′ iff h is ⊆_{P} -relevant (resp. ⊆_{P} -dispensable) for P, for each h ∈ H. Since the latter problems are Σ_{2}^{P} -hard if Sol(P) ≠ ∅ (see proof of Theorem 5.11), we have the theorem. □

Theorem 5.15 Let P = ⟨V, H, M, T ⟩ be a Horn PAP, and let P = ⟨P_{1}, …, P_{k}⟩ be a prioritization. Deciding whether h is ≤_{P} -relevant (resp. ≤_{P} -dispensable) for P is Δ_{2}^{P} - complete. Δ_{2}^{P} -hardness holds even if P is definite Horn and H ∪ M = V.

Proof. Membership in Δ_{2}^{P} can be shown analogous to membership of the problems in the full propositional case in Δ_{3}^{P} (proof of Theorem 4.9), where a NP oracle replaces the Σ_{2}^{P} oracle. We show this by a ≤_{m}^{p}-reduction of the following Δ_{2}^{P} -complete problem [37, 43]: Given a satisfiable clause set C = {C_{1}, …, C_{m}} on X = {x_{1}, …, x_{n}}, decide whether the with respect to ⟨x_{1}, …, x_{n}⟩ lexicographically maximum ϕ(X) satisfying C, which we denote by ϕ_{m}(X), fulfills ϕ_{m}(x_{n}) = true.

Let X′ = {x′_{1}, …, x′_{n}}, X′′ = {x′′_{1}, …, x′′_{n}}, R = {r_{1}, …, r_{2n}}, G = {g_{1}, …, g_{m}}, and define a definite Horn PAP P = ⟨V, H, M, T ⟩ by

V = X ∪ X′ ∪ X′′ ∪ R ∪ G
H = X ∪ X′ ∪ X′′
M = R ∪ G
T = {x_{i} → r_{i}, x_{i} → r_{n+i} : 1 ≤ i ≤ n} ∪ {x′_{i} → r_{i}, x′′_{i} → r_{n+i} : 1 ≤ i ≤ n} ∪

⋃_{j=1}^{m}({x_{i} → g_{j} : x_{i} ∈ C_{j}} ∪ {x′_{i} → g_{j} : ¬x_{i} ∈ C_{j}}),

and define a prioritization P = ⟨P_{1}, …, P_{n+1}⟩ by P_{1} = X∪X′, and P_{i+1} = {x′′_{i}}, 1 ≤ i ≤ n. Let for any truth assignment ϕ(X) be

H_{ϕ} = {x_{i} : ϕ(x_{i}) = true, 1 ≤ i ≤ n} ∪ {x′_{i}, x′′_{i} : ϕ(x_{i}) = false, 1 ≤ i ≤ n}.

Then, H_{ϕ} ∈ Sol(P) holds if and only if ϕ(X) satisfies C. Now verify that each S ∈ Sol(P) must contain x_{i} or x′_{i}, x′′_{i}, for 1 ≤ i ≤ n; otherwise T ∪ S |̸= r_{i} or T ∪ S |̸= r_{n+i} would hold. Consequently, since C is satisfiable, S ∈ Sol_{≤_{P}} (P) holds only if S = S_{ϕ} for some ϕ(X). Since P prefers solutions that do not contain x′′_{1} (and hence contain x_{1}) over solutions that contain x′′_{1} etc, it is clear that for distinct truth assignments ϕ(X), ψ(X) satisfying C, we have H_{ϕ} ≤_{P} H_{ψ} iff ϕ(X) is with respect to ⟨x_{1}, …, x_{n}⟩ lexicographically greater than ψ(X). Consequently, Sol_{≤_{P}} (P) = {H_{ϕ_{m}}} must hold. Hence, x_{n} is ≤_{P} -relevant (resp. x′_{n} is ≤_{P} -dispensable) for P iff ϕ_{m}(x_{n}) = true holds. Since P, P can be constructed in polynomial time and H ∪ M = V, the theorem follows. □

Penalization

For solution preference based on penalties, the problems reside for the Horn and the definite Horn case, as is expected, in PH one level below the full propositional case.

Theorem 5.16 Let P = ⟨V, H, M, T ⟩ be a Horn PAP and let p be a penalty attachment to H, which is part of the input. Deciding if h is ⊑_{p}-relevant (resp. ⊑_{p}-dispensable) for P is Δ_{2}^{P} -complete. Δ_{2}^{P} -hardness holds even if P is definite Horn and H ∪ M = V.

Proof. Membership in Δ_{2}^{P} is shown analogous to the full propositional case (proof of Theorem 4.11), where a NP oracle replaces the Σ_{2}^{P} oracle. Δ_{2}^{P} -hardness under the restrictions follows immediately by Theorem 5.15 and the ≤_{m}^{p}-reduction from ≤_{P} to ⊑_{p} applied in the proof of Theorem 4.11. □

Recall the convention that numbers are binary. With unary notation, ⊑_{p}-relevance and ⊑_{p}-dispensability are Δ_{2}^{P} [O(log n)]-complete in the Horn and definite Horn case.

6 Computation of solutions

In this section, we briefly address the problem of computing an acceptable solution. The complexity of this task is important if the solutions are computed incrementally one by one, and also for credulous reasoning. By this method, an arbitrary solution S ∈ Sol_{⪯}(P) is computed and considered as the only solution of the problem; all other solutions are neglected. Besides finding a solution to a PAP, we consider the case of ⊆- and ≤-solutions. Computing a solution is a search problem (see [35]); notice that functions are search problems with a unique solution. It can be seen that computing a solution to a PAP P = ⟨V, H, M, T ⟩ is, under a suitably generalized notion of polynomial-time Turing reducibility (cf. [26]) complete for the class of multivalued search problems solvable by nondeterministic Turing machines with NP oracle access in polynomial time (this class is termed NPMV^{NP} in [26]). The same holds for computing a ⊆-solution, since a guessed ⊆-solution may be verified in polynomial time with an NP oracle. In the Horn case, we get analogous completeness results for nondeterministic Turing machines without oracle access. And, recall that finding any as well as any ⊆-solution for a definite Horn PAP is polynomial. In case of ≤-preference, a simple completeness result for any well-known complexity class lacks at present. In the general case, the problem is solvable with O(|H|) queries to a Σ_{2}^{P} oracle. It is unclear, however, whether this bound can be substantially improved (e.g. to logarithmically many oracle calls in the input size). In the Horn case, we get an analogous result where an NP oracle replaces the Σ_{2}^{P} oracle. Computing a ≤-solution for a definite Horn PAP is, although this is easily shown NPhard, especially interesting since finding any solution is polynomial. The computational cost of this problem can be characterized e.g. in terms of the recently introduced class NPOP (NP optimization problems) [12], which is concerned with actually computing optimal solutions rather than with determining the optimal solution cost (cf. the class OptP in [43]). Since the problem can easily be shown to be in NPOP, it follows by results of Chen and Toda in [12] that a polynomial-time randomized algorithm using one free evaluation of parallel queries to NP sets can be described that finds a ≤-solution to any Horn PAP P with probability ≥ 1 − 2^{−e(n)}, where n is the instance size of P and e(n) is any given polynomial. Notice that this result is relevant for parallel computation of a ≤-solution. On the other hand, computing a ≤-solution for a definite Horn PAP can be readily shown to be a hard NPOP problem, which suggests that the problem is not solvable in polynomial time with one free evaluation of a sublinear number of parallel queries to NP oracle sets.

7 Conclusion

We have studied the complexity of logic-based abduction in the propositional context. To summarize, we first adopted a model of propositional abduction and solution preference, and then we considered the three main decision problems of abductive reasoning: does an abduction problem have a solution; does a hypothesis contribute to an acceptable solution (relevance), and; does a hypothesis occur in all acceptable solutions (necessity). Our study has included several preference orders and has paid attention to syntactical restrictions on the underlying theory; the main results, together with previously known results, are compactly presented in Tables 1-3. Note that we dealt with deciding ⪯- dispensability rather than with deciding ⪯-necessity, which is the complementary problem. Notice that all classes of the polynomial hierarchy PH, refined by adopting Δ_{k}^{P} [O(log n)] classes, from P up to Σ_{3}^{P} and Π_{3}^{P} are covered by our results, and that except for one case, deciding ⪯-necessity is as complex as the complement of deciding ⪯-relevance. The results of main interest are Σ_{2}^{P} -completeness of deciding whether a propositional abduction problem has any solution and that deciding ⪯-relevance or ⪯-necessity of a hypothesis is complete for any class at the second level of PH in case of no preference (=), in case of preference of irredundant solutions (⊆), and in case of preference of minimum-sized solutions (≤). The method of priorities (⊆_{P} , ≤_{P}) leads to a complexity increase except for ⊆_{P} -relevance in the case of definite Horn theories. For ⊆_{P} the increase reaches the upper complexity bound for polynomial decidable preference orders, which is at the third level of PH (⪯ in P). Under ≤_{P} -preference, which is “easier” than ⊆_{P} -preference, the problems are still at the second level, and are as hard as under preference by penalty attachments (⊑_{p}). If the underlying theory is Horn, then the complexity of the problems is always lowered by one level of PH. A further restriction to definite Horn theories only affects the complexity of the set-inclusion based preference methods (⊆, ⊆_{P}), and lowers the complexity of the problems, except for one case, by another level of PH. We have finally addressed in brief the issue of computing a solution for a propositional abduction problem. Unless PH collapses – what we assumed to be false – abduction is much harder than classical consequence ⊧, which is co-NP-complete, and cannot be solved in deterministic polynomial time even if an oracle for ⊧ is available. Besides ⊧, the number of candidates S ⊆ H for a solution S is a second source of complexity that lifts abduction to the second level of PH. The ⊆-minimality measure is not a source of additional complexity, as testing both whether S is a solution or a ⊆-solution is in Δ_{2}^{P}. In contrast to ⊆-minimality, the minimum cardinality measure is a source of additional complexity, which may be explained by the fact that testing whether S is a ≤-solution is Π_{2}^{P} -hard and Σ_{2}^{P} -hard (this follows from Theorem 4.6) and hence most likely not in Σ_{2}^{P} or Π_{2}^{P}. However, this source of complexity is “weaker” in a sense, since abduction with the minimum cardinality measure

P = ⟨V, H, M, T ⟩ general case T in clausal form T is Horn T is definite Horn
Deciding Sol(P) ≠ ∅  Σ_{2}^{P}  Σ_{2}^{P}  NP^{[69]}  in P^{[4]}

Table 1: Complexity results for propositional abduction (≤_{m}^{p}-completeness)

Propositional Abduction  Deciding whether h ∈ H is ⪯-relevant for P
P = ⟨V, H, M, T ⟩  =  ⊆  ≤  ⊆_{P} ≤_{P} ⊑_{p} ⪯ in P
general case  Σ_{2}^{P}  Σ_{2}^{P} Δ_{3}^{P}[O(log n)] Σ_{3}^{P} Δ_{3}^{P} Δ_{3}^{P}  Σ_{3}^{P}
T is in clausal form  Σ_{2}^{P}  Σ_{2}^{P} Δ_{3}^{P}[O(log n)] Σ_{3}^{P} Δ_{3}^{P} Δ_{3}^{P}  Σ_{3}^{P}
T is Horn  NP^{[69]} NP^{[69]} Δ_{2}^{P}[O(log n)] Σ_{2}^{P} Δ_{2}^{P} Δ_{2}^{P}  Σ_{2}^{P}
T is definite Horn  in P^{[28, 4]} NP^{[28]} Δ_{2}^{P}[O(log n)] NP Δ_{2}^{P} Δ_{2}^{P}  Σ_{2}^{P}

Table 2: Complexity results for propositional abduction, contd.

Propositional Abduction  Deciding whether h ∈ H is ⪯-necessary for P
P = ⟨V, H, M, T ⟩  =  ⊆  ≤  ⊆_{P} ≤_{P} ⊑_{p} ⪯ in P
general case  Π_{2}^{P}  Π_{2}^{P}  Δ_{3}^{P}[O(log n)] Π_{3}^{P} Δ_{3}^{P} Δ_{3}^{P}  Π_{3}^{P}
T is in clausal form  Π_{2}^{P}  Π_{2}^{P}  Δ_{3}^{P}[O(log n)] Π_{3}^{P} Δ_{3}^{P} Δ_{3}^{P}  Π_{3}^{P}
T is Horn  co-NP  co-NP Δ_{2}^{P}[O(log n)] Π_{2}^{P} Δ_{2}^{P} Δ_{2}^{P}  Π_{2}^{P}
T is definite Horn  in P^{[28, 4]} in P^{[28, 4]} Δ_{2}^{P}[O(log n)] co-NP Δ_{2}^{P} Δ_{2}^{P}  Π_{2}^{P}

Table 3: Complexity results for propositional abduction, contd. is still at the second level of PH. The method of priorities is another source of complexity for both the ⊆-minimal measure and the minimum cardinality measure. For a ⊆-solution S, which is a potential candidate for a ⊆_{P} -solution, exponentially many other candidates S′ such that S′ ⊆_{P} S may exist. Unless PH collapses, ⊆-minimality combined with the method of priorities is not polynomial even if an oracle for ⊆-minimal abduction is available. In the case of minimum cardinality solutions, the method of priorities moves abduction from Δ_{3}^{P} [O(log n)] to the class of Δ_{3}^{P} -complete problems, which are considered to be more difficult than the problems in Δ_{3}^{P} [O(log n)]. Penalization is in this case a “weaker” source of complexity, however, since it does not scale abduction up to the third level of PH. An intuitive explanation for the complexity increase is that computing the size of a ≤_{P} - solution on the priority groups, which seems to be an implicit task in solving the problem, needs probably about as many Σ_{2}^{P} oracle calls as H contains hypotheses in the worst case, while computing the size of a minimum cardinality solution is possible with a logarithmic number of oracle calls. The method of penalties is a “weak” source of complexity since it does not increase the complexity of abduction by another level of PH. The computational effect of this method is equivalent to the combined effect of the minimum cardinality measure and the method of priorities, and the complexity increase has the similar intuitive explanation by the Σ_{2}^{P} oracle calls made in computing the minimum penalty value for a solution. In the case of Horn theories, classical inference is polynomial and hence eliminated as a source of complexity. As the different preference orders have the same effect as in the general propositional case, this explains the decrease of the complexity of abduction by one level of PH in the Horn case. Under the further restriction to definite Horn theories, the structure of the set of solutions (S ⊆ H ∈ Sol(P) implies S′ ∈ Sol(P), for S ⊂ S′ ⊆ H) reduces the search space such that in some cases polynomial time algorithms are known.

Related results

We note that, more recently, similar complexity results have been derived for other forms of non-classical reasoning (see [7] for a survey of the field): Nonmonotonic Logics. Gottlob [32] has shown that several reasoning tasks in a number of nonmonotonic propositional logics are complete for a certain class of the second level of PH. In particular, he showed that in Reiter’s default logic [66], in McDermott and Doyle’s nonmonotonic logic [49, 48], in Moore’s autoepistemic logic [51], and in Marek and Truszczyński’s nonmonotonic logic N [47] (which all have a fixed point semantics), deciding whether a fixed point exists is Σ_{2}^{P} -complete; deciding whether a formula belongs to some fixed point is Σ_{2}^{P} -complete; and deciding whether a formula belongs to all fixed points is Π_{2}^{P} -complete. Stillman [71] and Papadimitriou and Sideri [55] found the same results independently for default logic.

Knowledge Base Update and Counterfactuals. A number of methods for revising or updating knowledge bases (theories) have been proposed in the literature which handle inconsistent update knowledge appropriately. This makes those methods applicable for evaluating counterfactuals, which are conditional statements of the form “if F, then G”, where F is assumed to be false in the current knowledge base [30]. Nebel [53] and Eiter and Gottlob [22] have shown that for almost all update operators ∘, deciding whether a knowledge base T updated, according to ∘, with formula F implies the formula G is Π_{2}^{P} -complete or “mildly” harder. Closed World Reasoning and Circumscription. Eiter and Gottlob [21] have shown that inferencing from a propositional theory under various forms of the closed world assumption and under circumscription is at the second level of PH. In particular, deciding whether the circumscription CIRC (F), i.e. the minimal models of a propositional formula F imply a formula G, is shown to be Π_{2}^{P} -complete. TMS. Rutenburg [68] has shown that for a certain variant of truth maintenance system (TMS), deciding whether a “nogood” of certain size exists is Σ_{2}^{P} -complete. This list may be extented by results for yet different forms of nonmonotonic reasoning, e.g. inheritance networks. All these results document that most of the popular forms of non-classical propositional logic are most likely much harder than classical propositional logic. Unless the polynomial hierarchy collapses, there is no polynomial algorithm for any of those Σ_{2}^{P} -hard or Π_{2}^{P} -hard problems, even if an NP oracle is provided; that is, deciding classical inferences is, modulo polynomiality, for free. On the other hand, most of the logics are roughly of the same computational complexity. As an important side result, completeness of problems in two logics for the same class entails that the problems are polynomial time transformable into each other. For example, a number of problems in non-classical logics can be polynomially transformed into testing necessity of a hypothesis for a propositional abduction problem. Conversely, the necessity test can be polynomially transformed into a circumscriptive inference problem, for instance.

Discussion and future work

Let us conclude this paper by a number of comments which also hint at further issues to study in the context of logic-based abduction. Our results clearly show that the major variants of logic-based abduction are very hard — in most cases even harder than classical propositional reasoning. Hence, there is no hope for complete and efficient algorithms that solve these problems. Similar observations on the other formalizations of abduction were made in [6], where an interesting discussion on the consequences these rather discouraging results is given. We fully agree with the conclusions drawn in [6]. Based on the ideas in [6] and our own work and experience, we can identify four possible directions to follow both to handle concrete abduction and to do further research on logic-based abduction. Use tractable restrictions of the abduction problems. We already stated in Section 1 that in several cases less complicated approaches such as the set-covering approach are more appropriate than logic-based abduction. Several reasoning tasks are solvable in polynomial with such models. If one has to build an abductive reasoner in a certain domain, one should always first look if a simple approach is sufficient for the particular purpose. Even for logic-based abduction several tractable subclasses have been identified, cf. [28, 4, 24]. We believe that it is worthwhile to explore additional and as large as possible tractable subclasses. However, we feel that further work in this direction should take into account the specific characteristics of particular application domains. For instance in the field of databases, one has to face large quantities of factual data and only few rules. Nevertheless, for several applications, it will just be impossible to find a suitably restricted version of abduction in order to gain tractability. Give up minimality or completeness of solutions. If it is impossible to efficiently compute minimal solutions that explain all manifestations, one may choose to cope with explanations of lower quality. In a first step, one may renounce to minimality of solutions. Unfortunately, this is beneficial only in the case of a definite Horn theory T (see Tables 2 and 3), where the complexity is lowered from NP to P due to monotonicity. In all other cases, the complexity remains unaffected. A more profitable idea may be to give up on solution completeness and accept approximate solutions, i.e., explanations that do not explain all manifestations, but only relevant parts of the present manifestations. This idea is fostered in [6] where also other relevant references on this issue are provided. It is a challenge for future theoretical research to see whether there exist polynomial algorithms generating approximate solutions to abduction problems for a suitable notion of approximation. Note that some NP-complete problems can be approximately solved in polyonmial time while others can not (for an overview, see [39]). Similar results for problems at higher levels of the polynomial hierarchy are currently not known. Note also that polynomial algorithms for inductive concept learning have been presented [2] which produce approximate solutions (concepts) under a statistical notion of approximation. Since inductive learning can be conceived as a form of abduction (set examples = manifestations, concepts = hypotheses), it would be interesting to see whether this form of approximate reasoning can be adapted to abduction problems. Other relevant methods of approximative reasoning that may be fruitfully applied to abduction have been introduced by Cadoli and Schaerf [8]. Note that partial or approximate explanations are often sufficient in order to cure a malfunction or to repair a faulty system. To give a simple example, a minimal diagnosis for the symptom high blood pressure is {excessive salt consumption, genetic predisposition}. A therapy in this case would usually consist in prescribing the patient a diet in order to invalidate the single hypothesis excessive salt consumption, thus making the symptom disappear. A more formal definition of therapy as opposed to diagnosis and a polynomial algorithm for computing therapies can be found in [28]. Use heuristic knowledge to control and simplify the search process. Our results suggest that the general formulation of a logic-based abduction problem does not encode knowledge that makes search efficient. In domain-specific abductive expert systems, such knowledge may be represented and used at a higher level. For an excellent discussion of this point, the reader is referred to [6, Section 7]. Give up on correctness and completeness of the search algorithm. One may use polynomial algorithms that are not guaranteed to be complete or correct, but which are known to compute the correct result with very high probability. Such algorithms for solving NP-complete problems have been studied in the recent literature [70, 41]. It remains to see if algorithms of this type also exist for problems that are complete for classes at higher levels of the polynomial hierarchy.

Acknowledgments. The authors would like to thank L. Console, D. Theseider Dupré, H. Blair, E. Köhler, and the anonymous referees for their valuable comments on a draft of this paper. The motor vehicle example has been suggested by L. Console and D. Theseider Dupré, and the reduction in the proof of Theorem 5.7 has been proposed by one of the referees. The authors are further grateful to K.W. Wagner for sending papers.

A Appendix

Lemma 5.8 Let C = {C_{1}, …, C_{m}} be a set of clauses on variables X and let k ∈ {1, …, m}. Call a truth assignment ϕ(X) csat-maximum for C iff ϕ(X) satisfies a maximum number of clauses in C. Then, deciding if every csat-maximum ϕ(X) for C fulfills V_{ϕ}(C_{k}) = true is Δ_{2}^{P} [O(log n)]-complete.

Proof. Membership of the problem in Δ_{2}^{P} [O(log n)] is clear since the maximum number s of simultaneously satisfiable clauses in C can be computed in O(log m) steps with an NP oracle, and then one query to an NP oracle finds the answer. We show hardness for Δ_{2}^{P} [O(log n)] by a ≤_{m}^{p}-reduction from the Δ_{2}^{P} [O(log n)]-complete problem UOCSAT [37]: Given a set C = {C_{1}, …, C_{m}} of clauses on variables X = {x_{1}, …, x_{n}}, decide if the maximum simultaneously satisfiable set of clauses in C is unique. Our transformation is as follows. In what follows, let for every clause set C denote msc(C) the maximum number of simultaneously satisfiable clauses in C. Let X^{1}, …, X^{m}, X^{i} = {x_{1}^{i}, …, x_{n+1}^{i}}, 1 ≤ i ≤ m be disjoint variable sets, and define clause sets C^{1}, …, C^{m} by C^{i} = C^{i,1} ∪ C^{i,2}, 1 ≤ i ≤ m, where C^{i,1} = {C_{1}^{i}, …, C_{n}^{i}} is a copy of C in which x_{j}^{i} is substituted for x_{j}, 1 ≤ j ≤ n, and

C^{i,2} = {C_{i}^{i} ∪ {¬x_{n+1}^{i}}} ∪ {{x_{n+1}^{i}, ¬x_{j}^{i}} : x_{j}^{i} ∈ C_{i}^{i}} ∪ {{x_{n+1}^{i}, x_{j}^{i}} : ¬x_{j}^{i} ∈ C_{i}^{i}}.

C^{i,2} is satisfiable, and each truth assignment ϕ(X^{i}) such that V_{ϕ}(C^{i,2}) = true fulfills ϕ(x_{n+1}^{i}) = V_{ϕ}(C_{i}^{i}). It is easily verified that a truth assignment ϕ(X^{i}) is csat-maximum for C^{i} iff V_{ϕ}(C^{i,2}) = true and ϕ(X^{i}) restricted to X^{i} − {x_{n+1}^{i}} is csat-maximum for C^{i,1}. Now let C^{m+1}, …, C^{2m} be copies of C^{1}, …, C^{m}, respectively, on sets of new variables Y^{1}, …, Y^{m} similar to the X^{1}, …, X^{n}, where in C^{i}, m < i ≤ 2m, the variable y_{j}^{i} is substituted for x_{j}^{i}, for all j. Let a_{1}, …, a_{m} be additional new variables, and define clause sets D^{i} on V^{i} = X^{i} ∪ Y^{i} ∪ {a_{i}}, 1 ≤ i ≤ m, by

D^{i} = C^{i} ∪ C^{m+i} ∪ {{x_{n+1}^{i}, y_{n+1}^{i}, ¬a_{i}}, {¬x_{n+1}^{i}, ¬y_{n+1}^{i}, ¬a_{i}}, {a_{i}}}.

The following is not hard to show: ϕ(a_{i}) = true for every csat-maximum ϕ(V^{i}) for D^{i} iff there exist csat-maximum truth assignments ψ(X), μ(X) for C such that V_{ψ}(C_{i}) ≠ V_{μ}(C_{i}). Let E = D^{1} ∪ ⋯ ∪ D^{m}, V = V^{1} ∪ ⋯ ∪ V^{m}. From the properties of the D^{i}’s, the following is easily obtained: There exists i ∈ {1, …, m} such that ϕ(a_{i}) = true for every csat-maximum ϕ(V) for E iff there exist csat-maximum truth assignments ψ(X), μ(X) for C such that V_{ψ}(C_{i}) ≠ V_{μ}(C_{i}). Now let b be a new variable and define

F = E ∪ {{¬a_{i}, ¬b} : 1 ≤ i ≤ m} ∪ {{b}}, W = V ∪ {b}.

Then, msc(E) + m ≤ msc(F) ≤ msc(E) + m + 1 holds. Now consider msc(F) = msc(E) + m + 1. This is clearly the case if and only if there is some csat-maximum ϕ(W) for E such that ϕ(a_{i}) = false, for 1 ≤ i ≤ m. By the properties of E, it follows that msc(F) = msc(E)+m+1 if and only if every csat-maximum ϕ(X), ψ(X) for C fulfill V_{ϕ}(C_{i}) = V_{ψ}(C_{i}), for 1 ≤ i ≤ m, i.e. the maximum simultaneously satisfiable subset of C is unique. It is obvious that msc(F) = msc(E)+m+1 iff each csatmaximum truth assignment ϕ(W) for F satisfies ϕ(b) = true. Therefore, the maximum simultaneously satisfiable subset of C is unique iff for every ϕ(W) that is csat-maximum for F, ϕ({b}) = true holds. Since F is polynomial-time constructible from C, the lemma follows. □

References

[1] D. Allemang, M.C.Tanner, T. Bylander, and J. Josephson. Computational Complexity of Hypothesis Assembly. In Proceedings IJCAI-87, pages 112–117, 1987.

[2] A. Blumer, A. Ehrenfeucht, D. Haussler, and M. Warmuth. Occam’s Razor. Information Processing Letters, 24:377–380, 1987.

[3] G. Brewka. Nonmonotonic Reasoning: Logical Foundations of Commonsense. Cambridge University Press, 1991.

[4] T. Bylander. The Monotonic Abduction Problem: A Functional Characterization on the Edge of Tractability. In Proceedings KR-91, pages 70–77, 1991.

[5] T. Bylander, D. Allemang, M. Tanner, and J. Josephson. Some Results Concerning the Computational Complexity of Abduction. In Proceedings KR-89, pages 44–54, 1989.

[6] T. Bylander, D. Allemang, M. Tanner, and J. Josephson. The computational complexity of abduction. Artificial Intelligence, 49:25–60, 1991.

[7] M. Cadoli and M. Schaerf. A Survey on Complexity Results for Non-monotonic Logics. Technical report, Dipartimento di Informatica e Sistemistica, Università di Roma “La Sapienza”, 1992. To appear in Journal of Logic Programming.

[8] M. Cadoli and M. Schaerf. Approximate Inference for Concept Languages. In Proceedings KR-92, 1992.

[9] E. Charniak. A Neat Theory of Marker Passing. In Proceedings AAAI-86, 1986.

[10] E. Charniak. Motivation Analysis, Abductive Unification, and Nonmonotonic Equality. Artificial Intelligence, 34:275–295, 1988.

[11] E. Charniak and P. McDermott. Introduction to Artificial Intelligence. Addison Wesley, Menlo Park, Ca, 1985.

[12] Z.-Z. Chen and S. Toda. On the Complexity of Computing Optimal Solutions. International Journal of Foundations of Computer Science, 2(3):207–220, 1991.

[13] L. Console, D. Theseider Dupré, and P. Torasso. A Theory of Diagnosis for Incomplete Causal Models. In Proceedings IJCAI-89, pages 1311–1317, 1989.

[14] L. Console, D. Theseider Dupré, and P. Torasso. On the Relationship Between Abduction and Deduction. Journal of Logic and Computation, 1(5):661–690, 1991.

[15] L. Console and P. Torasso. A Spectrum of Logical Definitions of Model Based Diagnosis. Computational Intelligence, 7(3):133–141, 1991.

[16] G. Cooper. The computational complexity of probabilistic inference using Bayesian belief networks. Artificial Intelligence, 42:393–405, 1990.

[17] P. Cox and T. Pietrzykowski. General Diagnosis by Abductive Inference. In IEEE Sympos. on Logic Programming, pages 183–189, 1987.

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

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

[20] J. Doyle. A Truth-Maintenance System. Artificial Intelligence, 12:231–272, 1979.

[21] T. Eiter and G. Gottlob. Propositional Circumscription and Extended Closed World Reasoning are Π_{2}^{P} -complete. Theoretical Computer Science 114:231–245, 1993. Addendum 118:315.

[22] T. Eiter and G. Gottlob. On the Complexity of Propositional Knowledge Base Revision, Updates, and Counterfactuals. Artificial Intelligence, 57(2-3):227–270, 1992.

[23] K. Eshghi. Abductive Planning with Event Calculus. In Proc. 5th International Conference and Symposium on Logic Programming, pages 562–579. MIT Press, 1988.

[24] K. Eshghi. A Tractable Class of Abduction Problems. In Proceedings IJCAI-93, pages 3–8, 1993.

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

[26] S. Fenner, S. Homer, M. Ogiwara, and A. Selman. On Using Oracles That Compute Values. Technical Report 93-05, CS Department of the University of New York at Buffalo, February 1993. Extended abstract in: Proceedings STACS-93, pp. 398-407, Springer LNCS 665, 1993.

[27] J. Finger. Exploiting Constraints in Design Synthesis. PhD thesis, Dept. Comput. Sc. Stanford University, 1987.

[28] G. Friedrich, G. Gottlob, and W. Nejdl. Hypothesis Classification, Abductive Diagnosis, and Therapy. In Proceedings International Workshop on Expert Systems in Engineering, Vienna, September 1990, number 462 in Lecture notes in AI, pages 69–78, 1990.

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

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

[31] L. Giordano and A. Martelli. An Abductive Characterization of the TMS. In Proceedings of ECAI-90, pages 308–313, 1990.

[32] G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2(3):397–425, June 1992.

[33] C. Hartshorne et al., editors. The Collected Papers of Charles Sanders Peirce. Cambridge Press, 1931–1958, Vol. II, pages 272–607.

[34] J. R. Hobbs, M. E. Stickel, P. Martin, and D. Edwards. Interpretation as Abduction. In Proceedings of the 26th Annual Meeting of the Association for Computational Linguistics, pages 95–103, 1988.

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

[36] J. Josephson, B. Chandrasekaran, J. J. W. Smith, and M. Tanner. A Mechanism for Forming Composite Explanatory Hypotheses. IEEE Transactions on Systems, Man, and Cybernetics, SMC-17:445–454, 1987.

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

[38] A. Kakas and P. Mancarella. Database Updates Through Abduction. In Proceedings VLDB-90, pages 650–661, 1990.

[39] Viggo Kann. On the Approximability of NP-complete Optimization Problems. PhD thesis, Department of Numerical Analysis and Computing Science, Royal Institute of Technology, Stockholm, Sweden, May 1992.

[40] K. Konolige. Abduction versus closure in causal theories. Artificial Intelligence, 53:255–272, 1992.

[41] E. Koutsoupias and C. Papadimitriou. On the Greedy Algorithm for Satisfiability. Information Processing Letters, 43:53–55, 1992.

[42] R. Kowalski. Logic Programs in Artificial Intelligence. In Proceedings IJCAI-91, pages 596–601, 1991.

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

[44] M. Krentel. Generalizations of OptP to the Polynomial Hierarchy. Theoretical Computer Science, 97(2):183–198, 1992.

[45] H. Levesque. A knowledge-level account for abduction. In Proceedings IJCAI-89, pages 1061–1067, 1989.

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

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

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

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

[50] A. Meyer and L. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential time. In Proceedings 13^{th} Ann. Symp. on Switching and Automata Theory, pages 125–129. IEEE Computer Society, 1972.

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

[52] C. G. Morgan. Hypothesis Generation by Machine. Artificial Intelligence, 2:179–187, 1971.

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

[54] P. Norvig. Inference in Text Understanding. In Proceedings AAAI-87, 1987.

[55] C. Papadimitriou and M. Sideri. On Finding Extensions of Default Theories. In Proceedings 4th Intl. Conference on Database Theory (ICDT 92), October 1992.

[56] J. Pearl. Fusion, propagation, and structuring in belief networks. Artificial Intelligence, 29:241–288, 1986.

[57] J. Pearl. Probabilistic Reasoning in Intelligent Systems. Morgan Kaufmann, San Mateo, CA, 1988.

[58] C. S. Peirce. Abduction and induction. In J. Buchler, editor, Philosophical Writings of Peirce, chapter 11. Dover, New York, 1955.

[59] Y. Peng and J. Reggia. Abductive Inference Models for Diagnostic Problem Solving. Springer, 1990.

[60] D. Poole. A Logical Framework for Default Reasoning. Artificial Intelligence, 36:27–47, 1988.

[61] D. Poole. A Methodology for Using a Default and Abductive Reasoning System. International Journal of Intelligent Systems, 5(5):521–548, 1989.

[62] D. Poole. Explanation and Prediction: An Architecture for Default and Abductive Reasoning . Computational Intelligence, 5(1):97–110, 1989.

[63] D. Poole. Normality and Faults in Logic Based Diagnosis. In Proceedings IJCAI-89, pages 1304–1310, 1989.

[64] H. Pople. On the Mechanization of Abductive Logic. In Proceedings IJCAI-73, pages 147–152, 1973.

[65] G. Provan. The computational complexity of multiple-context truth maintenance systems. In Proceedings ECAI-90, pages 522–527, August 1990.

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

[67] R. Reiter. A Theory of Diagnosis From First Principles. Artificial Intelligence, 32:57–95, 1987.

[68] V. Rutenburg. Complexity Classification in Truth Maintenance Systems. In Proceedings STACS-91, pages 373–383, 1991.

[69] B. Selman and H. J. Levesque. Abductive and Default Reasoning: A Computational Core. In Proceedings AAAI-90, pages 343–348, July 1990.

[70] B. Selman, H. J. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proceedings AAAI-92, pages 440–446, July 1992.

[71] J. Stillman. The Complexity of Propositional Default Logic. In Proceedings AAAI-92, pages 794–799, 1992.

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

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

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