Gustav Nordh
email: nordh@lix.polytechnique.fr

Bruno Zanuttini

What makes propositional abduction tractable

Keywords: Abduction, Propositional logic, Computational complexity

Abduction is a fundamental form of nonmonotonic reasoning that aims at finding explanations for observed manifestations. This process underlies many applications, from car configuration to medical diagnosis. We study here the computational complexity of deciding whether an explanation exists in the case when the application domain is described by a propositional knowledge base. Building on previous results, we classify the complexity for local restrictions on the knowledge base and under various restrictions on hypotheses and manifestations. In comparison to the many previous studies on the complexity of abduction we are able to give a much more detailed picture for the complexity of the basic problem of deciding the existence of an explanation. It turns out that depending on the restrictions, the problem in this framework is always polynomial-time solvable, NP-complete, coNP-complete, or Σ P 2 -complete. Based on these results, we give an a posteriori justification of what makes propositional abduction hard even for some classes of knowledge bases which allow for efficient satisfiability testing and deduction. This justification is very simple and intuitive, but it reveals that no nontrivial class of abduction problems is tractable. Indeed, tractability essentially requires that the language for knowledge bases is unable to express both causal links and conflicts between hypotheses. This generalizes a similar observation by Bylander et al. for set-covering abduction.

Introduction

Abduction is the fundamental reasoning process which consists of explaining observations by plausible causes taken from a given set of hypotheses. For instance, it is an abduction problem to try to derive diseases from observed symptoms, according to known rules relating both. This process was extensively studied by Peirce [START_REF]Philosophical Writings of Peirce[END_REF], and its importance to Artificial Intelligence was first emphasized by Morgan [START_REF] Morgan | Hypothesis generation by machine[END_REF] and Pople [START_REF] Pople | On the mechanization of abductive logic[END_REF].

From the application point of view, abduction has demonstrated its importance. It has been applied in particular to explanation-based diagnosis (e.g., medical diagnosis [START_REF] Bylander | The computational complexity of abduction[END_REF]), to text interpretation [START_REF] Hobbs | Interpretation as abduction[END_REF], and to planning [START_REF] Herzig | Planning as abduction[END_REF]. It is also the fundamental process underlying ATMSs [START_REF] De Kleer | An assumption-based TMS[END_REF].

The formalization and resolution of abduction problems have been studied in numerous formalisms, among which set-covering [START_REF] Bylander | The computational complexity of abduction[END_REF], default logic [START_REF] Eiter | Semantics and complexity of abduction from default theories[END_REF], logic programming [START_REF] Eiter | Abduction from logic programs: Semantics and complexity[END_REF][START_REF] Lin | Abduction in logic programming: A new definition and an abductive procedure based on rewriting[END_REF]. We are interested here in its resolution in classical propositional logic.

We adopt a complexity-theoretic point of view. More precisely, we are interested in the complexity of deciding whether an abduction problem has a solution when the underlying knowledge base is propositional. Thus our study follows Selman and Levesque's [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF] and Eiter and Gottlob's [START_REF] Eiter | The complexity of logic-based abduction[END_REF] seminal papers. We also build on two classifications previously obtained in our framework [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF][START_REF] Nordh | Propositional abduction is almost always hard[END_REF].

Even in the simple setting of propositional logic, deciding whether an abduction problem has a solution is in general Σ P 2 -complete. Consequently, like for most hard computational problems, several approaches have been studied for solving it efficiently: Exhibiting tractable classes obtained by restrictions over the knowledge base [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF][START_REF] Del Val | On some tractable classes in deduction and abduction[END_REF][START_REF] Eiter | The complexity of logic-based abduction[END_REF][START_REF] Eshghi | A tractable class of abduction problems[END_REF][START_REF] Zanuttini | New polynomial classes for logic-based abduction[END_REF]; heuristic approaches, in particular through computation of prime implicates [START_REF] Del Val | A new method for consequence finding and compilation for restricted languages[END_REF][START_REF] Del Val | The complexity of restricted consequence finding and abduction[END_REF][START_REF] Marquis | Consequence finding algorithms[END_REF][START_REF] Simon | Efficient consequence finding[END_REF] and through reducing the problem to QBF and using generic QBF solvers [START_REF] Egly | Solving advanced reasoning tasks using quantified boolean formulas[END_REF]; compilation [START_REF] Cadoli | Preprocessing of intractable problems[END_REF][START_REF] Liberatore | Compilability of propositional abduction[END_REF]; and approximation [START_REF] Kautz | Horn approximations of empirical data[END_REF][START_REF] Zanuttini | Approximation of relations by propositional formulas: complexity and semantics[END_REF].

In this paper we adopt the approach consisting of trying to find tractable restrictions over the knowledge base. Our contribution is twofold.

First, we identify the complexity of abduction, with varying restrictions over the representations of manifestations and hypotheses, for every constraint lan-guage and every clausal or equational language restricting the (propositional) knowledge base, under reasonable assumptions on the representation of the constraints. Concerning manifestations, we study the restrictions where they are expressed as a positive, negative, or unrestricted literal, clause, term, or CNF. Concerning hypotheses, we study the restrictions where they are expressed by a set of literals which is positive, negative, closed under complement, or unrestricted. To that aim, we use the now well-known Schaefer's framework [START_REF] Schaefer | The complexity of satisfiability problems[END_REF] and Post's lattice [START_REF] Post | The two-valued iterative systems of mathematical logic[END_REF]. Precisely, we proceed as follows.

• We first prove a relatively small number of tractability and hardness results

for particular constraint languages. • Using Post's classification and these results, we then derive the complexity of abduction for any constraint language. • In a similar manner, and at the same time, we obtain the complexity of abduction for any clausal or equational language.

We exhibit new polynomial and new hard restrictions. We also discover that abduction is always either in P, NP-complete, coNP-complete, or Σ P 2 -complete, depending on the restrictions. Such a result could not be taken for granted, due to Ladner's result stating that if P = NP, then there exist problems in NP that are neither in P nor NP-complete [START_REF] Ladner | On the structure of polynomial time reducibility[END_REF]. Moreover, the fact that some restrictions yield NP-complete, and others coNP-complete problems is surprising at first sight. It reveals in particular that abduction is a very rich problem in terms of completeness results in different complexity classes. Thus our results can be used as starting points for establishing complexity results for other problems, in particular in nonmonotonic reasoning.

From the application point of view, our tables of complexity allow the designers of knowledge-based agents or expert systems to choose the appropriate knowledge representation language, according to the tradeoff between the expressiveness required and the constraints on resolution of abduction problems. Moreover, when a representation language that is hard for abduction must be used, the precise complexity of the corresponding problem allows to choose heuristic approaches for solving it. For instance, with an appropriate reduction an NP-complete problem can be solved by a satisfiability solver, while a Σ P 2 -complete one cannot; a more generic QBF solver (or a specialized QBF ∃,2solver) must be used.

Our second contribution is to identify a simple set of minimal conditions yielding NP-completeness for languages which allow for efficient deduction (and are thus good candidates for knowledge representation). For instance, when terms have to be explained, we discover that abduction is NP-hard exactly when the language for knowledge bases can both express causal links from hypotheses to individual manifestations and forbid some combinations of hypotheses. This generalizes similar observations by Bylander et al. [START_REF] Bylander | The computational complexity of abduction[END_REF] about set-covering abduction.

From this condition it follows that tractability can occur only in very restricted cases, i.e., when there can be no causal dependency at all or when causes can all be assumed together. For instance, in medical diagnosis this means that diseases must not rule each other out for the task to be tractable. We also argue that these conditions give intuitions about results beyond Schaefer's framework of constraint languages, and we revisit some previously known results in that manner. In this spirit, our observations allow to adopt a unified point of view on the results exhibited with many different restrictions in the literature.

The use of Post's lattice and Schaefer's framework for studying the complexity of reasoning problems is sometimes considered to be overlimitating. For instance, it does not encompass the class of all Horn formulas; this is because Horn clauses can be arbitrarily long. In this study, we adopt these powerful tools coming from complexity-theory and show how to overcome some of these limitations. Indeed, we use them to show results about infinite constraint languages as well as about finite ones, and we formulate the former in terms of classes of CNF formulas. These extensions are directly motivated by AIapplications where it is common to model the knowledge base using an infinite constraint language represented in terms of classes of CNF formulas.

To put our results in context, we briefly discuss the results from the literature on the complexity of abduction that are most relevant to our present study. Our starting point is Selman and Levesque's [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF], and Eiter and Gottlob's [START_REF] Eiter | The complexity of logic-based abduction[END_REF] classical results. Selman and Levesque [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF] proved that deciding whether an abduction problem over a Horn knowledge base has an explanation is NPcomplete, even when the hypotheses are given as a set of positive literals and the manifestation is a single positive literal. Similarly, Eiter and Gottlob [START_REF] Eiter | The complexity of logic-based abduction[END_REF] proved that when the knowledge base is given by a general propositional formula, the problem becomes Σ P 2 -complete. Moreover they note that when the knowledge base is given by a definite Horn formula, the hypotheses are positive literals, and the manifestations are given by a positive term, then the problem is in P.

From these results it is clear that the complexity of the abduction problem depends heavily on the representation language of the knowledge base. This have led researchers to investigate the complexity of abduction for various restrictions on the representation language of the knowledge base. This line of research culminated with the two recent complexity classifications given in [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF][START_REF] Nordh | Propositional abduction is almost always hard[END_REF]. In these papers the complexity of deciding if there exists an explanation is classified for a very general class of restrictions on the representation language of the knowledge base, that include many restrictions that have been studied before in the literature. Although the restrictions on the representa-tion language of the knowledge base studied in these papers are identical, the papers differ on the representation of hypotheses and manifestations. In [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF] the hypotheses are given by a set of literals that are closed under complement and the manifestation is given by a single literal, while in [START_REF] Nordh | Propositional abduction is almost always hard[END_REF] the hypotheses are allowed to be any set of literals and the manifestations are given by a term.

When comparing the results of [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF] and [START_REF] Nordh | Propositional abduction is almost always hard[END_REF] it becomes clear that even small variations on the representation of hypotheses and manifestations can have a strong impact on the complexity of the abduction problem. Hence, to understand the complexity of abduction one must also understand how restrictions on the representation of hypotheses and manifestations influence the complexity. This is partially the motivation for the present study where we systematically analyse the complexity of abduction under simultaneous restrictions on the representation of hypotheses, manifestations, and the knowledge base.

The paper is organized as follows. We first give some preliminaries about propositional logic, Schaefer's framework and complexity classes (Section 2) and the definition of the abduction problems we are interested in (Section 3). We then survey previous work and give an overview of our results (Section 4). The technical content of the paper follows: we give several generic reductions between abduction problems (Section 5) and recall several well-known tools for studying abduction (Section 6); we then give the complexity results (Sections 7 to 12) by distinguishing the various families of restrictions over the knowledge base. These results are summarized in Section 13, and some further restrictions on the problems are discussed in Section 14. Finally, we discuss what makes abduction hard in Section 15, and we conclude in Section 16.

Preliminaries

In the paper we consider restrictions over knowledge bases seen either as propositional formulas or as conjunctions of constraints taken from a fixed language. We introduce here the corresponding basic definitions and notations, define the restrictions that we will consider, and briefly recall some complexity notions.

Propositional logic

Boolean variables are usually denoted by x, possibly with subscripts and superscripts. A literal is either a variable (positive literal) or the negation of one (negative literal). Literals are usually denoted by ℓ. The opposite of literal ℓ is written ℓ, i.e., ℓ = x if ℓ = ¬x and vice-versa.

A clause is a finite disjunction of literals, written C = ℓ 1 ∨ ℓ 2 ∨ • • • ∨ ℓ n . A formula in Conjunctive Normal Form (a CNF for short) is a finite conjunction of clauses, written

KB = C 1 ∧ C 2 ∧ • • • ∧ C k .
A term is a finite conjunction of literals, written T = ℓ 1 ∧ ℓ 2 ∧ • • • ∧ ℓ n . Variables, literals, clauses and terms are considered special cases of formulas. A (linear) equation is an equation of the form (x 1 ⊕ x 2 ⊕ • • • ⊕ x n = a) with a ∈ {0, 1} (⊕ denotes addition modulo 2). An affine formula is a finite conjunction of linear equations. Observe that affine formulas are not CNFs.

If ϕ is a formula, Vars(ϕ) denotes the set of all variables that occur in ϕ. Given a set of variables V , Lits(V ) denotes the set of all literals formed upon the variables in V , i.e., Lits(V

) = V ∪ {¬x | x ∈ V }. If L is a set of literals,
L denotes their conjunction, and N (L) denotes the set of opposite literals {ℓ | ℓ ∈ L}. A clause, term, or CNF is said to be positive (resp. negative) if all the literals which occur in it are positive (resp. negative), and a clause or term is said to be unit if it contains exactly one literal. The empty clause is written ⊥. Observe that Vars(⊥) = ∅ and that ⊥ is always false. Similarly, (0 = 1) denotes the always false linear equation with no variable.

An assignment µ to a set of variables V is a mapping from V to {0, 1}. When the order of the variables is clear, we write assignments as words, e.g., µ = 011 if µ(x 1 ) = 0 and µ(x 2 ) = µ(x 3 ) = 1. If KB is a formula, an assignment µ to Vars(KB ) or to a superset of Vars(KB ) is said to satisfy KB , or to be a model of KB , if it makes KB evaluate to 1 with the usual rules for the connectives. We write µ |= KB .

A formula KB is said to be satisfiable if it has at least one model. It is said to entail a formula KB ′ if every assignment to Vars(KB ) ∪ Vars(KB ′ ) which satisfies KB also satisfies KB ′ , written KB |= KB ′ . If moreover KB ′ |= KB , then KB and KB ′ are said to be (logically) equivalent, written KB ≡ KB ′ .

Example 1

The formula:

KB = (x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 3 ∨ ¬x 4 ) ∧ (¬x 1 ∨ x 2 ∨ ¬x 3 ) ∧ (¬x 1 ∨ ¬x 2 )
is a CNF containing 4 clauses. We have Vars(KB ) = {x 1 , x 2 , x 3 , x 4 }, and thus Lits(Vars(KB )) = {x 1 , ¬x 1 , . . . , x 4 , ¬x 4 }. The assignment µ to Vars(KB ) defined by µ(x 1 ) = 0, µ(x 2 ) = 1, µ(x 3 ) = 0, and µ(x 4 ) = 0 (µ = 0100 for short) is a model of KB , while 0000 is not. The formula KB ′ = (x 1 ⊕ x 2 = 1) ∧ (x 2 ⊕ x 3 ) = 0 is an affine formula. Its set of models is {011, 100}, and it can be seen that KB ′ |= KB , while KB |= KB ′ and thus, KB ≡ KB ′ .

Classes of clauses and equations

We will first impose restrictions on the knowledge bases of abduction problems in the form of classes of clauses and linear equations. These classes are reported in Table 1 (page 11, second and third columns) and described below.

The class of all clauses is denoted by C CNF . A clause C is said to be 1-valid if it is satisfied by assigning 1 to all variables in it. Equivalently, a clause is 1-valid if it contains at least one positive literal. The class of all 1-valid clauses is denoted by C 1v . Dually, C 0v is the class of all 0-valid clauses.

A clause is Horn if it contains at most one positive literal. The class of all Horn clauses is denoted by C Horn . A clause is 1-valid Horn (also called definite Horn) if it contains exactly one positive literal. The class of all 1-valid Horn clauses is denoted by C 1v -Horn . Analogously, a clause C is said to be dual-Horn (0-valid dual-Horn) if it contains at most one (exactly one) negative literal, and the class of all dual-Horn clauses (0-valid dual-Horn clauses) is denoted by C dHorn (C 0v -dHorn ). Moreover, the class of all 1-valid dual-Horn clauses is denoted by C 1v -dHorn .

A clause is said to be bijunctive if it contains at most two literals, and implicative if it contains zero (empty clause) or one literal, or is of the form (¬x 1 ∨x 2 ). The classes of all bijunctive and of all implicative clauses are denoted by C bij and C impl , respectively. A clause is said to be IHS-B-if it is implicative or negative, and the class of all IHS-B-clauses is denoted by C IHSB-. Similarly, a clause is said to be IHS-B+ if it is implicative or positive, and the class of all IHS-B+ clauses is denoted by C IHSB+ . Moreover, a clause is said to be of width k if it contains at most k literals. The classes of all IHS-B-and IHS-B+ clauses of width k are denoted C IHSB -/k and C IHSB +/k , respectively.

A clause is said to be essentially negative if it is negative or unit positive. The class C neg,= contains all essentially negative clauses, as well as the equality relations (x 1 = x 2 ). Observe that such equality relations are not clauses, thus we slightly abuse language. The reason why we allow the equality relation is that it makes the class C neg,= equivalent in expressiveness to a relational clone, and thus, in particular, stable with respect to the complexity of abduction (see Section 2.3). Nevertheless, we also discuss the case when this relation is not allowed in the paper. Dually to C neg,= , the class C pos,= contains all essentially positive clauses and the equality relations.

Recall that a linear equation is an equation of the form (

x 1 ⊕ • • • ⊕ x n = a), a ∈ {0, 1}.
The class of all linear equations is denoted by E aff . Similarly to the case of clauses we say that a linear equation is 1-valid (resp. 0-valid) if it is satisfied by assigning 1 (resp. 0) to all variables in it. The classes of all 1-valid and all 0-valid linear equations are denoted by E 1v -aff and E 0v -aff , respectively.

A linear equation is of width 2 if it contains at most two variables. The class of all linear equations of width 2 is denoted by E aff /2 . Finally, the class C unit,= contains all unit clauses and equality relations (the same remark as for C neg,= applies). The class C 1v -unit,= contains the unit positive clauses and the equality relations, and the class C 0v -unit,= contains the unit negative clauses and the equality relations.

Constraint languages and Post's lattice

In this section we introduce the notions of constraint languages and relational clones. We also describe Post's classification of all Boolean relational clones, usually referred to as Post's lattice. A more detailed introduction to Post's lattice can be found in the survey articles [START_REF] Böhler | Playing with Boolean blocks, part I: Post's lattice with applications to complexity theory[END_REF][START_REF] Böhler | Playing with Boolean blocks, part II: Constraint satisfaction problems[END_REF].

Constraints generalize the notions of clauses and linear equations, and constraint languages generalize the notion of classes of clauses and equations. The set of all n-tuples of elements from {0, 1} is denoted by {0, 1} n . Such tuples are denoted as sequences or as words, e.g., (0, 1, 1) or 011. Any subset of {0, 1} n is called an n-ary relation on {0, 1}. A (finite) constraint language over {0, 1} is an arbitrary (finite) set of (finitary) relations over {0, 1}.

If Γ is a constraint language, then a constraint over Γ is an application of an n-ary relation R ∈ Γ to an n-tuple of variables, written R(x 1 , . . . , x n ) (possibly with repeated variables). A formula over Γ (or Γ-formula) is a finite conjunction of constraints over Γ, written KB = R 1 (x 11 , . . . , x 1n 1 ) ∧ • • • ∧ R k (x k1 , . . . , x kn k ). A constraint over Γ is considered a special case of Γ-formula. Like for propositional formulas, we write Vars(KB ) for the set of all variables occurring in KB .

If C = R(x 1 , . . . , x n ) is a constraint, an assignment µ to {x 1 , . . . , x n } or to a superset of {x 1 , . . . , x n } is said to satisfy C, or to be a model of C, if the n-tuple (µ(x 1 ), µ(x 2 ), . . . , µ(x n )) is in R. If KB is a Γ-formula, then µ is said to satisfy KB if it
satisfies all its constraints. The notions of satisfiability, entailment and equivalence are defined like for propositional formulas, and similarly for entailment and equivalence between a propositional formula and a Γ-formula.

Example 2 (continued) The set R = {0100, 0110, 0111, 1000, 1001} is a 4ary relation, and R ′ = {01, 10} and R ′′ = {00, 11} are binary relations. Thus Thus, slightly abusing notation, we will identify a clause (or equation) C on variables x 1 , . . . , x k with the k-ary relation consisting of its set of satisfying assignments. In particular, we will often identify the literal x (resp. ¬x) and the unary constraint T(x) (resp. F(x)), so that if KB is a Γ-formula and L is a set of literals, then KB ∧ L is considered a Γ ∪ {T, F}-formula.

Γ = {R, R ′ , R ′′ } is a constraint language. Then R(x 1 , x 2 , x 3 , x 4 ) ∧ R ′′ (x 3 , x 4 ) is a Γ-formula. It can be seen that this formula entails KB of Example 1. Now C = R(x 1 , x 2 , x 3 , x 3 ) is a Γ-constraint (
We also say that a relation is Horn if it can be represented by a Horn CNF. A constraint language Γ is said to be Horn if every relation in Γ is Horn. Thus, slightly abusing notation, we write C Horn both for the class of all Horn clauses and for the (infinite) constraint language containing all the relations represented by Horn clauses. We use the same shorthands for the other classes of clauses and equations.

Example 4 (continued) Relation R in Example 2 is represented by formula KB in Example 1. Relation R ′ = {01, 10} is represented by the formula (x 1 ∨ x 2 ) ∧ (¬x 1 ∨ ¬x 2 )
, and thus it is bijunctive. Observe that it is also represented by the formula x 1 ⊕ x 2 = 1, and thus it is affine (of width 2).

Central to our approach is the notion of a relational clone. Intuitively, the relations in the relational clone Γ are those which can be simulated by existentially quantified conjunctions of constraints over Γ ∪ {R = }. We will show (in Section 5.2) that the complexity of abduction is stable under such simulations, from which it follows that the complexity for all (finite) constraint languages is determined by the complexity for one (finite) language in each relational clone.

Definition 5 Let Γ be a constraint language. The relational clone of Γ, written Γ , is the set of all relations R such that R(x 1 , . . . , x n ) is logically equivalent to ∃V KB (where n is the arity of R) for some set of variables V disjoint from {x 1 , . . . , x n } and some Γ ∪ {R = }-formula KB with Vars(KB ) = {x 1 , . . . , x n } ∪ V .

Example 6 Let R be the 4-ary relation represented by the CNF (x 1 ∨x 2 ∨x 3 ∨ x 4 ) ∧ (¬x 1 ∨ ¬x 2 ∨ ¬x 3 ∨ ¬x 4 ), and recall that F is the unary relation {0}. Let R ′ be the ternary relation represented by the formula

(x 1 ∨ x 2 ) ∧ (x 2 ⊕ x 3 = 0). It is easily seen that R ′ (x 1 , x 2 , x 3 ) ≡ ∃x 4 R(x 1 , x 1 , x 2 , x 4 ) ∧ F(x 4 ) ∧ R = (x 2 , x 3 ), and thus R ′ ∈ {R, F} . Definition 7 A constraint language Γ is said to be a relational clone if Γ = Γ .
Emil Post gave a remarkable classification of all classes of Boolean functions which are closed under composition and projection [START_REF] Post | The two-valued iterative systems of mathematical logic[END_REF]. Such classes of functions are referred to as clones and, as a result of Post's classification, the inclusion structure (under set inclusion) among Boolean clones is completely known. Later it was shown that there is a bijection between clones and relational clones [START_REF] Geiger | Closed systems of functions and predicates[END_REF][START_REF] Pschel | Funktionen-und Relationenalgebren[END_REF] and that the inclusion structure (under set inclusion) among the relational clones follows from the inclusion structure among the clones. The classification of Boolean clones/relational clones is called Post's lattice and is presented in Figure 1 in terms of relational clones. The lines in the lattice represent set inclusion, i.e., a line from a relational clone ICl 1 to a relational clone ICl 2 lying above ICl 1 in the lattice, means that ICl 1 ⊆ ICl 2 . The dotted lines represent infinite chains of relational clones (e.g., IS 2 0 , IS 3 0 , . . . , IS n 0 , . . . for the rightmost line).

We give a definition of each relational clone that is relevant to our study in Table 1, taken from [START_REF] Creignou | Preferred representations of Boolean relations[END_REF]. The other relational clones are not relevant in the sense that their complexity for abduction is always the same as one of its super-clones and one of its sub-clones.

As it turns out from the results in [START_REF] Creignou | Preferred representations of Boolean relations[END_REF], most relational clones Γ correspond to a class C of clauses or equations, in the sense that every relation in Γ can be represented by a conjunction of clauses (equations) from C, and every clause (equation) from C, viewed as a relation, is in Γ. In particular, Γ = C .

Thus we define relational clones in the following manner. For each entry in the table, the relational clone named in the first column is the set of all relations which can be represented by a conjunction of clauses or equations as in the third column. For instance, the class BR is the relational clone of all relations which can be represented by a conjunction of clauses (that is, the class of all relations); IE 2 is the relational clone containing all Horn relations; IL 0 is the class of all relations which can be represented by a conjunction of linear equations all with 0 as their right member, and so on. When there is a standard name for the relational clone or class of formulas, it is given in the fourth column.

Only two relational clones cannot be defined in this manner. A relation is said to be complementive if for every tuple (µ 1 , . . . , µ n ) in it, the tuple (µ 1 ⊕ 1, . . . , µ n ⊕ 1) is also in it. Then IN 2 denotes the relational clone containing all complementive relations, and IN denotes that containing all complementive and 0-valid (and thus also 1-valid) relations.

Given a relational clone Γ it is easy to locate Γ ∪ {F} and Γ ∪ {T} in Post's lattice. This will be useful several times, so we state this easy fact for

IE 0 - (¬x 1 ∨ • • • ∨ ¬xn), n ≥ 1, (x 1 ∨ ¬x 2 ∨ • • • ∨ ¬xn), n ≥ 2 - IE - (x 1 ∨ ¬x 2 ∨ • • • ∨ ¬xn), n ≥ 2 - IV 2
C dHorn clauses with at most one negative literal dual Horn

IV 1 C 1v -dHorn (¬x 1 ∨ x 2 ∨ • • • ∨ xn), n ≥ 2, (x 1 ∨ • • • ∨ xn), n ≥ 1 - IV 0 C 0v -dHorn
clauses with exactly one negative literal definite dual Horn

IV - (¬x 1 ∨ x 2 ∨ • • • ∨ xn), n ≥ 2 -
Bijunctive and IHS-B

ID 2 C bij clauses containing at most 2 literals bijunctive IM 2 C impl (¬x 1 ∨ x 2 ), (x 1 ), (¬x 1 ), ⊥ implicative IM - (¬x 1 ∨ x 2 ) - IS 10 C IHSB- (x 1 ), (¬x 1 ∨ x 2 ), (¬x 1 ∨ • • • ∨ ¬xn), n ≥ 0 IHS-B- IS k 10 C IHSB-/k (x 1 ), (¬x 1 ∨ x 2 ), (¬x 1 ∨ • • • ∨ ¬xn), k ≥ n ≥ 0 IHS-B-of width k IS 12 Cneg,= (x 1 ), (¬x 1 ∨ • • • ∨ ¬xn), n ≥ 0, (x 1 = x 2 )
essentially negative

IS 11 - (¬x 1 ∨ x 2 ), (¬x 1 ∨ • • • ∨ ¬xn), n ≥ 0 - IS k 11 - (¬x 1 ∨ x 2 ), (¬x 1 ∨ • • • ∨ ¬xn), k ≥ n ≥ 0 - IS k 1 - (x 1 = x 2 ), (¬x 1 ∨ • • • ∨ ¬xn), n ≤ k - IS 00 C IHSB+ (¬x 1 ), (¬x 1 ∨ x 2 ), (x 1 ∨ • • • ∨ xn), n ≥ 0 IHS-B+ IS k 00 C IHSB+/k (¬x 1 ), (¬x 1 ∨ x 2 ), (x 1 ∨ • • • ∨ xn), k ≥ n ≥ 0 IHS-B+ of width k IS 02 Cpos,= (¬x 1 ), (x 1 ∨ • • • ∨ xn), n ≥ 0, (x 1 = x 2 ) essentially positive IS 01 - (¬x 1 ∨ x 2 ), (x 1 ∨ • • • ∨ xn), n ≥ 0 - IS k 01 - (¬x 1 ∨ x 2 ), (x 1 ∨ • • • ∨ xn), k ≥ n ≥ 0 - IS k 0 - (x 1 = x 2 ), (x 1 ∨ • • • ∨ xn), n ≤ k - Affine IL 2 E aff all linear equations affine IL 0 E 0v -aff (x 1 ⊕ • • • ⊕ xn = 0), n ≥ 0 - IL 1 E 1v -aff (x 1 ⊕ • • • ⊕ xn = a), n ≥ 0, a = n (mod 2) - IL 3 - (x 1 ⊕ • • • ⊕ xn = a), n even, a ∈ {0, 1} - IL - (x 1 ⊕ • • • ⊕ xn = 0), n even - ID 1 E aff /2 (0 = 1), (x 1 = a), (x 1 ⊕ x 2 = a), a ∈ {0, 1} affine of width 2 ID - (0 = 1), (x 1 ⊕ x 2 = a), a ∈ {0, 1} - Unit IR 2 C unit,= (x), (¬x), (x 1 = x 2 ) - IR 1 C 1v -unit,= (x), (x 1 = x 2 ) - IR 0 C 0v -unit,= (¬x), (x 1 = x 2 ) - IBF - (x 1 = x 2 ) -
Table 1 Classes of clauses and equations future reference.

The abduction problem

We define here the various abduction problems which we study. In order to clarify the presentation, we first define the general abduction problem, without any restriction on hypotheses and manifestations, and then its restrictions.

General abduction problem

The abduction problem with restrictions on the knowledge base only is defined as follows. Recall that classes of clauses or equations are identified to constraint languages, so that the following definition encompasses them.

Problem 9 (Abd(Γ)) Let Γ be a constraint language. An instance P of the abduction problem Abd(Γ) is a tuple (V, H, M, KB ), where

• V is a set of variables, • H ⊆ Lits(V ) is the set of hypotheses,
• M is a propositional formula (the manifestation), with Vars(M ) ⊆ V , and

• KB is a Γ-formula, with Vars(KB ) ⊆ V .
The question is whether there exists an explanation for P , i.e., a set E ⊆ H such that KB ∧ E is satisfiable and KB ∧ E entails M .

We need to make assumptions on how the relations in the Γ-formula for the KB are represented. When the constraint language Γ is not specified by giving a class of equations or clauses, then we naturally assume that all the relations in all constraints in the Γ-formula are given in extension. That is, by listing all the tuples belonging to each relation explicitly. When Γ is specified by giving a class of equations or clauses, then we choose to let the Γ-formula be represented by a system of equations or CNF-formula, respectively. For complexity matters, the size of P = (V, H, M, KB ) is defined to be the total number of occurrences of variables in it, and additionally in the case where the Γ-formula is given in extension, the number of tuples in the relations in the Γ-formula.

As an illustration, consider, e.g., the language Γ = {R = , R = }, that is, the language containing the binary equality and difference relations. Then an instance of Abd(Γ) is a tuple (V, H, M, KB ), where KB is a conjunction of equality and difference constraints over V , H is a set of literals over V , and M is a propositional formula over V . Similarly, an instance of Abd(C Horn ) is a tuple (V, H, M, KB ), where KB is a Horn CNF and H and M are as before.

Observe that we can assume without loss of generality that KB is satisfiable in an instance. Indeed, if KB is unsatisfiable, then KB ∧ E cannot be satisfiable (for any E), and thus there can be no explanation. Nevertheless, we do not enforce this assumption since satisfiable KB s cannot be distinguished from unsatisfiable ones efficiently in general.

The notion of explanation is illustrated in the following example.

Example 10 (continued) Consider again KB = (

x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 3 ∨ ¬x 4 ) ∧ (¬x 1 ∨ x 2 ∨ ¬x 3 ) ∧ (¬x 1 ∨ ¬x 2 ) of Example 1. The tuple P = (V = {x 1 , x 2 , x 3 , x 4 }, H = {x 3 , ¬x 4 , x 4 }, M = x 2 , KB )
is an instance of Abd(C CNF ). It has exactly three explanations, namely

E 1 = {x 3 , ¬x 4 }, E 2 = {x 3 , x 4 }, and E 3 = {x 3 }.
On the contrary, {x 1 } is not an explanation, because it is not a subset of H, {x 4 } is not because it does not entail M together with KB , and finally {x 1 , x 3 } is not because it is not consistent with KB (and it is not a subset of H).

In the literature it is common to impose a preference relation on the different explanations in order to concentrate on the most interesting/preferred explanations. One common preference criterion is subset minimality, i.e., an explanation E is said to be subset minimal (⊂-minimal) if there is no other explanation E ′ such that E ′ ⊂ E. We want to emphasize that in this paper we do not impose any preference relation on explanations. Note that in the example above E 3 ⊂ E 1 , E 2 , which does not matter in our setting but would make E 3 the only preferred explanation with respect to the subset minimality criterion.

Abduction under restrictions

We now define the abduction problem under restrictions on manifestations and hypotheses. We will use the following notation for restrictions on manifestations:

• PosLits denotes the class of all positive literals,

• NegLits denotes the class of all negative literals, and Problem 11 (abduction under restrictions) Let Γ be a constraint language, and let M be a class of propositional formulas. An instance P of one of the decision problems P-Abd(Γ,M), N-Abd(Γ,M), V-Abd(Γ,M), or L-Abd(Γ,M) is an instance (V, H, M, KB ) of the problem Abd(Γ) such that M ∈ M holds and

• H ⊆ V , that is, every h ∈ H is positive, for P-Abd, • H ⊆ N (V ) (every h ∈ H is negative) for N-Abd, • H = V H ∪ N (V H ) for some V H ⊆ V (H is closed under complement) for V-Abd, • H ⊆ Lits(V ) (H is unrestricted) for L-Abd.
For all four problems, the question is whether there is an explanation for P .

Our motivation for studying various restrictions on the hypotheses and manifestations is to understand how these restrictions affect the complexity of the problem. We note that as far as no restriction is imposed to the knowledge base, generic polynomial-time reductions exist between all these restrictions. For instance, moving from a term M to a (fresh) variable m as the manifestation can be done up to adding M ↔ m, or even M → m, to the knowledge base. Similarly, a negative hypothesis of the form ¬h ∈ H can be removed by replacing ¬h with a fresh variable h ′ in H, and adding ¬h ↔ h ′ to KB . This is the motivation for studying only restricted cases, such as positive hypotheses and single-variable manifestations, in generic heuristic approaches to solving abduction problems (see, e.g., Marquis' survey [START_REF] Marquis | Consequence finding algorithms[END_REF]). However, when the knowledge base is restricted to a particular language, as is the case here, such reductions in general fail to preserve the language. This is why we study various restrictions on H and M , and investigate their impact on the complexity of the problem. Note that in the particular case of Horn knowledge bases and single-literal manifestations, Eiter and Makino were similarly interested in the impact of the polarity imposed to the manifestation [START_REF] Eiter | On computing all abductive explanations from a propositional Horn theory[END_REF]. In our terms, among other results they compared the complexity of L-Abd(C Horn ,PosLits) to that of L-Abd(C Horn ,NegLits).

Further restrictions on the problem, such as assuming that the manifestation is satisfiable or that every hypothesis occurs in the knowledge base, are of interest for practical purposes. Nevertheless, apart from very restricted cases they do not affect the complexity of the problem, so we only discuss them briefly in Section 14.

To conclude this section, observe that we do not consider DNF manifestations, that is, disjunctions of terms as manifestations. The reason for that is that already deciding KB |= M , where M is a DNF formula, is coNP-complete even if KB is empty (tautological), since then it is equivalent to deciding whether M is tautological. Consequently, there is no hope in finding interesting (tractable) classes of knowledge bases for abduction with such manifestations.

Related work and overview of results

In this section we first survey relevant literature on the complexity of abduction, and then give an overview of our results. We finally discuss how our results may be used in several contexts.

Related work

The earliest work about assumption-based propositional abduction is Reiter and de Kleer's, in the ATMS framework [START_REF] Reiter | Foundations of assumption-based truth maintenance systems: preliminary report[END_REF]. As far as this paper is concerned, the main result there is a characterization of explanations by means of prime implicates, reported in Section 6.2.

Subsequently, in the early nineties, several results were given concerning the computational complexity of abduction. Among them, Bylander et al. [START_REF] Bylander | The computational complexity of abduction[END_REF] consider set-covering abduction. That is, they assume that each hypothesis comes with the set of atomic manifestations which it can explain, and the question is to find a set of hypotheses which explains all manifestations. Under various assumptions on the interaction between hypotheses (incompatibility, independence, etc.), the authors investigate the frontier between tractable and intractable such problems. Since this objective is similar to ours, we give a detailed comparison of our work with theirs in Section 15.2. The complexity of abduction has also been studied for other representations of the knowledge base, for example when the knowledge base is represented by ordered binary decision diagrams [START_REF] Horiyama | Reasoning with ordered binary decision diagrams[END_REF].

The first complexity results in the logic-based setting were given by Selman and Levesque [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF] for abduction problems with propositional Horn knowledge bases. Then Eiter and Gottlob performed a more systematic complexity analysis [START_REF] Eiter | The complexity of logic-based abduction[END_REF]. The main results, which we will use for our classification purposes, are the following ones.

Proposition 12 ( [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF]) P-Abd(C Horn ,PosLits) is NP-complete. Hardness holds even if the knowledge base is also restricted to be acyclic Horn.

Proposition 13 ([20])

The general problem Abd(C CNF ) is Σ P 2 -complete. Hardness holds even if all hypotheses are positive and manifestations are restricted to positive terms, that is, P-Abd(C CNF ,PosTerms) is also

Σ P 2 -complete. Proposition 14 ([20]) P-Abd(C 1v -Horn ,PosTerms) is in P.
Due to the intractability results of Propositions 12 and 13, several authors investigated polynomial classes of the abduction problem. Eshghi [START_REF] Eshghi | A tractable class of abduction problems[END_REF] gives a rather technical class based on acyclic Horn formulas (see also del Val's discussion of this result [START_REF] Del Val | On some tractable classes in deduction and abduction[END_REF]); however, this class is not captured by our framework.

Zanuttini [START_REF] Zanuttini | New polynomial classes for logic-based abduction[END_REF] also gives several polynomial classes using the notion of projection, which is presented in Section 6.3. He also gives new proofs for several folklore polynomial classes (discussed by, e.g., Marquis [START_REF] Marquis | Consequence finding algorithms[END_REF]) and for classes of DNF formulas (which are not captured by our framework). The results which are relevant here are the following ones.

Proposition 15 ([51]

) V-Abd(E aff ,Clauses) is in P.

Proposition 16 (see [START_REF] Marquis | Consequence finding algorithms[END_REF][START_REF] Zanuttini | New polynomial classes for logic-based abduction[END_REF]) V-Abd(C pos,= ,Clauses), V-Abd(C neg,= ,Clauses), and V-Abd(C bij ,Clauses) are in P.

Finally, two classification results have recently been given in Schaefer's framework, concerning some restrictions which we study here. We however wish to emphasize that these results were given for finite constraint languages only, whereas we are interested here in both finite constraint languages and infinite (clausal) languages.

Theorem 17 (L-Abd [START_REF] Nordh | Propositional abduction is almost always hard[END_REF]) Let Γ be a finite constraint language. Then L-Abd(Γ,Terms) is in

P if Γ is in ID 1 . Otherwise, it is NP-complete if Γ is in IE 2 , IV 2 , ID 2 , or IL 2 . Otherwise, it is Σ P 2 -complete.
Theorem 18 (V-Abd [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF]) Let Γ be a finite constraint language. Then V-Abd(Γ,PosLits) is in

P if Γ is in IL 2 , ID 2 , IS 10 , IS 02 , IS k 00 (for some k), or IE 1 . Otherwise, it is NP-complete if Γ is in IE 2 or IV 2 . Otherwise, it is Σ P 2 -complete. V-Abd(Γ,Lits) is in P if Γ is in IL 2 , ID 2 , IS 12 , IS 02 , IS k 10 , or IS k 00 (for some k). Otherwise, it is NP-complete if Γ is in IE 2 or IV 2 . Otherwise, it is Σ P 2 - complete.
As concerns Theorem 18, observe in particular that there is no finite language which is in IS 00 or IS 01 but not in IS k 00 or IS k 01 for any k ∈ N. In fact, infinite constraint languages Γ such that Γ = IS 01 yield NP-complete problems (see our Proposition 63).

Overview of results

In this paper, building on the aforementioned results, we perform a systematic study of the computational complexity of propositional abduction. This study allows us to give the complexity of problems P-Abd(Γ,M), N-Abd(Γ,M), V-Abd(Γ,M), and L-Abd(Γ,M) when

• M is any of PosLits, NegLits, Lits, and similarly for clauses, terms, and CNFs instead of literals, • Γ is any constraint language or any clausal or equational language.

To that aim, we reuse the results given in the literature for specific languages. In particular, we reuse the classifications in [START_REF] Nordh | Propositional abduction is almost always hard[END_REF] and [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF]. Observe in particular that the latter concerns some maximally easy problems for us, in the sense that no other problem which we study can be reduced to them in polynomial time in a generic manner. So it proves very helpful for deriving hardness results. Dually, the former classification proves helpful for deriving membership results, as well as hardness results for CNF manifestations.

Nevertheless, these classifications leave large "gaps". For instance, if Γ is a finite constraint language such that Γ = IL 2 (unrestricted affine constraints), V-Abd(Γ,PosLits) is in P [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF] while L-Abd(Γ,Terms) is NP-complete [START_REF] Nordh | Propositional abduction is almost always hard[END_REF]. Thus these classifications tell nothing about the tractability frontier between both restrictions.

In this paper, for filling several such gaps we strengthen some results given in the literature. Nevertheless, we also give a number of brand new results.

• We study the complexity of P-Abd and N-Abd for 0-valid and 1-valid languages. We exhibit new trivial and new Σ P 2 -hard problems.

• We study the complexity of P-Abd and N-Abd for complementive languages, and identify one minimal coNP-hard and two minimal Σ P 2 -hard problems.

• We complete the literature on abduction with Horn and dual Horn knowledge bases (mainly Selman and Levesque's [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF] and Eiter and Gottlob's [START_REF] Eiter | The complexity of logic-based abduction[END_REF] results). Our main new result is that P-Abd(C dHorn ,CNFs) is in P. • We complete the literature on abduction with bijunctive and IHS-B knowledge bases. Abduction over bijunctive and IHS-B constraint languages are particularly interesting since the borderline between tractability and NPhardness is mainly situated among problems over such constraint languages. We identify two new polynomial problems, namely L-Abd(C impl ,PosCNFs) and L-Abd(C neg,= ,PosCNFs), and many new hardness results with a unified reduction from satisfiability problems. • Similarly, we complete the literature for affine knowledge bases. We give two new tractability results, namely for L-Abd(E aff ,Clauses) and V-Abd(E aff ,Terms), and several new hardness results using original reductions from satisfiability problems.

We also wish to emphasize that as far as we know, CNF manifestations had never been studied before.

These results allow us to complete the picture on the complexity of propositional abduction, and in particular to identify the tractability frontier (between P and NP-hard). This frontier, as we discuss in Section 15, can be characterized by very simple conditions. Moreover, it parallels the frontier identified by Bylander et al. for set-covering abduction [START_REF] Bylander | The computational complexity of abduction[END_REF].

Applications

As already evoked, our results are essentially interesting from a complexitytheoretic and from an AI point of view. On the complexity-theoretic side, we give the complexity of abduction for various, fine-grained restrictions, and it turns out that abduction is always either in P, NP-complete, coNP-complete, or Σ P 2 -complete. This is interesting since Ladner's result states that if P = NP, then there exist problems in NP that are neither in P nor NP-complete [START_REF] Ladner | On the structure of polynomial time reducibility[END_REF]. Such problems are said to be of intermediate complexity.

One way to interpret our results is that the infinite class of abduction problems that we study do not contain such problems of intermediate complexity. For further discussions on the complexity-theoretic topic of finding large subclasses of NP which do not contain problems of intermediate complexity, we refer the reader to Feder and Vardi's seminal paper [START_REF] Feder | The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory[END_REF].

Finally, since the complexity of abduction spans four classes (P, NP, coNP, and Σ P 2 ) and because abduction is a central problem in nonmonotonic reasoning (see, e.g., [START_REF] Brewka | Nonmonotonic reasoning: an overview[END_REF][START_REF] Marquis | Consequence finding algorithms[END_REF]), our results may serve as starting points for deriving complexity results for other problems, by using reductions to or from abduction.

From the AI point of view, our results may help the designers of knowledgebased agents or expert systems to choose the appropriate knowledge representation language. Indeed, depending on the application, and especially on the constraints on resolution of abduction problems, it might be necessary to ensure that such problems will be solved efficiently, or it may be acceptable that they are NP-hard2 . Moreover, depending on the application, the sets of hypotheses and the manifestations may be restricted to particular classes. Then, using our results and the characteristics and requirements of the application, the designer of a knowledge-based system can choose the appropriate knowledge representation language. In particular, she might choose the most expressive one while respecting the tractability constraints.

We acknowledge that our restrictions on knowledge bases cannot capture all possible propositional knowledge representation languages. For instance, they cannot capture the class of Horn-renamable CNF formulas, or that of acyclic Horn formulas, since they impose global restrictions on formulas.

Nevertheless, classes defined by local properties are very important for knowledge representation. Indeed, they are stable under conjunction, that is, if KB 1 and KB 2 are in one of these classes, then so is KB 1 ∧ KB 2 . This makes them suitable for merging mutually consistent theories without losing computational properties of each (simply conjunct both) and is important for knowledge approximation purposes, since such classes define a unique least upper bound [START_REF] Selman | Knowledge compilation and theory approximation[END_REF]. Moreover, they have been given complete pictures of complexity for various reasoning tasks (e.g., inference under circumscription [START_REF] Nordh | A trichotomy in the complexity of propositional circumscription[END_REF] and several tasks in default reasoning [START_REF] Chapdelaine | Complexity of default logic on generalized conjunctive queries[END_REF]), which allows to choose a knowledge representation language under constraints stemming from several tasks. Last but not least, the relational clone generated by any constraint or clausal/equational language can be recognized in polynomial time [START_REF] Creignou | Preferred representations of Boolean relations[END_REF]. Thus an agent may make decisions depending on its current knowledge base. It can, for instance, decide not to try to find an exact solution to a planning problem through abduction because its current knowledge base is not tractable for it, and adopt another strategy, such as approximate planning.

Reductions between abduction problems

We have defined restrictions on the abduction problem along three dimensions: 12 different types of manifestations, 4 different types of hypotheses, and an infinite number of restrictions over knowledge bases. Since our goal is to give a complexity classification of the problem for each combination of restrictions, this section explains how to restrict to a finite and limited number of cases.

Reductions between restrictions on manifestations and hypotheses

The following reductions are obvious.

Lemma 19 Let Γ be a constraint language and let M and M ′ be classes of propositional formulas such that M ⊆ M ′ . Then L-Abd(Γ,M) ≤ P L-Abd(Γ,M ′ ). The same result holds for P-Abd, N-Abd, or V-Abd instead of L-Abd.

Lemma 20 Let Γ be a constraint language, and let M be a class of propositional formulas. Then P-Abd(Γ,M), N-Abd(Γ,M), V-Abd(Γ,M), ≤ P L-Abd(Γ,M).

Reductions between restrictions on knowledge bases

In this section we show how Post's lattice can be used to reduce the number of restrictions on knowledge bases that need to be considered when classifying the complexity of the abduction problem. This approach via Post's lattice is crucial for obtaining our complexity classifications. We conclude this section by demonstrating how the approach can be used to classify the complexity of P-Abd(Γ,Terms) for every constraint language Γ and every clausal or equational language C.

The key for the approach via Post's lattice is Lemma 22, which states that Abd(Γ ′ ) ≤ P Abd(Γ) whenever Γ ′ is a finite and Γ ′ ⊆ Γ (for all restrictions over hypotheses and manifestations considered here). Hence, when studying the complexity of the abduction problem for finite constraint languages Γ, it is enough to consider one generating constraint language per relational clone. In particular, if Γ and Γ ′ are two finite constraint languages and Γ = Γ ′ , then Abd(Γ) and Abd(Γ ′ ) are polynomial-time equivalent to each other.

We first need the following lemma, which allows to get rid of equality relations in knowledge bases.

Lemma 21 Let Γ be a constraint language, and let M be any class of manifestations considered in this paper. Then L-Abd(Γ∪{R = },M) ≤ P L-Abd(Γ,M). The same holds for V-Abd, P-Abd, or N-Abd instead of L-Abd.

PROOF. Let (V, H, M, KB ) be an instance of L-Abd(Γ ∪ {R = },M). Build a knowledge base over Γ from KB in the following manner. For all constraints R = (x i , x j ) in KB replace every occurrence of x j with x i in KB , H, M , remove the constraint from KB , and remove x j from V . Perform this identification iteratively, until KB does not contain any equality constraint any more. Clearly, this transformation can be performed in polynomial time and preserves the existence of an explanation. Finally, it is easily seen that it preserves any restriction on hypotheses and manifestations in the statement. ✷

We can now give the central lemma of our study. The proof checks that additional variables introduced while replacing a constraint in Γ ′ with its equivalent expression over Γ do not affect the existence of a solution.

Lemma 22 Let Γ be a constraint language, and let Γ ′ ⊆ Γ be a finite constraint language (or a finite clausal or equational language). Let M be a class of propositional formulas. Then L-Abd(Γ ′ ,M) ≤ P L-Abd(Γ,M). The same holds for V-Abd, P-Abd, or N-Abd instead of L-Abd, and for a class of clauses or equations C instead of a constraint language Γ.

PROOF. Let P

′ = (V ′ , H ′ , M ′ , KB ′ ) be an instance of L-Abd(Γ ′ ,M). Write KB ′ = i∈I R ′ i (x ′ i,1 , . . . , x ′ i,k i ) and for all i ∈ I, V ′ i = {x ′ i,1 , . . . , x ′ i,k i }.
By the definition of a relational clone we know that for all i ∈ I, the constraint

R ′ i (x ′ i,1 , . . . , x ′ i,k i ) of KB ′ is logically equivalent to some formula ∃V i KB i where V i ∩ V ′ i = ∅ and KB i is a Γ ∪ {R = }-formula over V i ∪ V ′ i .
Importantly, for all i ∈ I we assume V i ∩ V ′ = ∅ and for all i, i ′ ∈ I with i = i ′ , we assume V i ∩ V i ′ = ∅, i.e., all existentially quantified variables are fresh with respect to V ′ and different from each other. This is without loss of generality since the names of these variables are unconstrained.

We define an instance P = (V, H, M, KB ) of Abd(Γ ∪ {R = }) by

• V = V ′ ∪ i∈I V i , • H = H ′ , • M = M ′ , and • KB = i∈I KB i .
In other words, we simply replace every constraint in KB ′ with its expression over Γ ∪ {R = }, and we forget existential quantification. Clearly, this can be performed in linear time since languages are fixed and Γ ′ is finite, and thus all expressions of relations in Γ ′ can be stored in a lookup table once and for all.

We now claim that P and P ′ have exactly the same explanations. First, let E ′ be an explanation for P ′ . Then KB ′ ∧ E ′ is satisfiable, thus the formula i∈I ∃V i KB i ∧ E ′ is satisfiable. Since all existentially quantified variables are fresh with respect to V ′ and different from each other, it follows that KB ∧ E ′ is satisfiable. Now assume that KB ∧ E ′ does not entail M . Then KB ∧ E ′ ∧ ¬M is satisfiable. By the assumption on fresh variables again, it follows that i∈I ∃V i KB i ∧ E ′ ∧ ¬M is satisfiable, i.e., that KB ′ ∧ E ′ ∧ ¬M is satisfiable. Since M = M ′ , this contradicts the fact that E ′ is an explanation for P ′ . Thus every explanation E ′ for P ′ is an explanation for P , and the proof is similar for showing the converse. We conclude by invoking Lemma 21 for getting rid of equality constraints. ✷ It is important to note that the reduction in the proof above preserves all the restrictions on hypotheses and manifestations considered in this paper. For example, if we reduce from a V-Abd(Γ ′ ,PosLits) instance, then the resulting instance will be a V-Abd(Γ,PosLits) instance. Thus, using Lemma 22, we will be able to give the complexity of all the restrictions on the Abd problem for any finite constraint language (Section 13) by considering the complexity of only one language per relational clone.

We now demonstrate the use of Post's lattice for classifying the complexity of Abd(Γ) problems by giving the complete classification of P-Abd(Γ,Terms) for every constraint language Γ and class of clauses/equations C. The reasoning is similar for the other combinations of restrictions on hypotheses and manifestations.

Gathering together results for positive hypotheses and terms as manifestations from subsequent sections in the paper, and applying the (obvious) reductions in Section 5.1, we get the minimal set of results in Table 2. These results are minimal in the sense that they are irredundant with respect to reductions of the form P-Abd(Γ,Terms) ≤ P P-Abd(Γ ′ ,Terms) as soon as Γ ⊆ Γ ′ . In this table, for each clausal language C, we give inside parentheses the corresponding relational clone, i.e., the relational clone ICl such that ICl = C .

The complete picture of complexity can now be obtained as follows.

First, as explained in Section 13.2, a upper bound for the complexity of a clausal or equational language C corresponding to a relational clone ICl carries over to every language Γ such that Γ ⊆ ICl. Now, since all lower bounds are given for finite languages, the results on Figure 2 follow from the results in Table 2, where

• every result reported from the table is given by a bolded circle, and • every other result follows from these together with reductions of the form P-Abd(Γ,Terms) ≤ P P-Abd(Γ ′ ,Terms) as soon as Γ ⊆ Γ ′ (Lemma 22).

Consequently, we have the complexity for every constraint language. For more details, we refer the reader to Section 13.2.

Exploiting the symmetry between 0 and 1

We now show how to exploit the symmetry between 0 and 1 (or positive and negative) in order to reduce the number of cases that need to be considered. We will use the notion of duality. Observe that in the graphical representation of Post's lattice of Boolean relational clones (Figure 1), the dual of a relational clone is simply its mirror image with respect to the vertical line through the center of the lattice [START_REF] Böhler | Bases for Boolean co-clones[END_REF]. Moreover, it is easy to see that if a relation R is represented by a conjunction of clauses (or equations)

Definition 23 (dual) The dual of a clause C = (ℓ 1 ∨ • • • ∨ ℓ k ) is the clause C d = (ℓ 1 ∨ • • • ∨ ℓ k ). The dual of a class of clauses C is the class C d = {C d | C ∈ C}. The dual of an equation Eqn = (x 1 ⊕ • • • ⊕ x n = a) is Eqn d = Eqn if n is even, and Eqn d = (x 1 ⊕ • • • ⊕ x n = a ⊕ 1) otherwise. The dual of an n-ary Boolean relation R is R d = {(µ 1 ⊕ 1, . . . , µ n ⊕ 1) | (µ 1 , . . . , µ n ) ∈ R}. The dual of a constraint language Γ is Γ d = {R d | R ∈ Γ}.
C 1 ∧ • • • ∧ C k , then R d is represented by C d 1 ∧ • • • ∧ C d k .
Example 24 (continued) The dual of clause These definitions allow us to state the following easy equivalences between problems which are in some sense symmetric to each other. The intuition is simply that switching the polarity of all literals in all components of the instance and replacing all relations (clauses/equations) by their duals preserve the existence of explanations.

C = (x 1 ∨ x 2 ∨ ¬x 3 ) is C d = (¬x 1 ∨ ¬x 2 ∨ x 3 ). The dual of equation Eqn = (x 1 ⊕ x 2 = 1) is Eqn itself, and that of Eqn ′ = (x 1 ⊕ x 2 ⊕ x 3 = 0) is (Eqn ′ ) d = (x 1 ⊕ x 2 ⊕ x 3 = 1). The dual of relation R = {000, 010, 111} is R d = {111,
Lemma 25 Let Γ be a constraint language or a class of clauses/equations. Then the following equivalences hold:

• P-Abd(Γ,PosLits) ≡ P N-Abd(Γ d ,NegLits),

• N-Abd(Γ,PosLits) ≡ P P-Abd(Γ d ,NegLits),

• V-Abd(Γ,PosLits) ≡ P V-Abd(Γ d ,NegLits), and • L-Abd(Γ,PosLits) ≡ P L-Abd(Γ d ,NegLits).

They also hold when the manifestations are restricted to positive or negative clauses, terms, or CNFs instead of literals.

Consequently, in the rest of the paper we will only consider positive and unrestricted manifestations. The complexity for negative manifestations can be derived using Lemma 25.

Similarly, the lack of positive/negative polarity for manifestations and/or hypotheses allows to reduce the number of cases to consider. The following lemma is straightforward.

Lemma 26 Let Γ be a constraint language or a class of clauses or equations, and let M be any of Lits, Clauses, Terms, or CNFs. Then,

• N-Abd(Γ,M)

≡ P P-Abd(Γ d ,M), • L-Abd(Γ,M) ≡ P L-Abd(Γ d ,M), and • V-Abd(Γ,M)) ≡ P V-Abd(Γ d ,M).

Other reductions

The following lemma allows to impose polarities to hypotheses and manifestations when the language contains the disequality relation R = = {01, 10}.

Lemma 27 Let Γ be a constraint language such that R = ∈ Γ , and let M be either PosLits or NegLits. Then L-Abd(Γ,Lits) ≤ P P-Abd(Γ,M), N-Abd(Γ,M). The same result holds for clauses, terms, or CNFs instead of literals.

PROOF. Consider an instance (V, H, M, KB ) of L-Abd(Γ,Terms). The desired instance of P-Abd(Γ,PosTerms) is simply obtained by introducing a fresh variable x ′ for any negative literal ¬x in H or M , replacing ¬x with x ′ and adding the constraint R = (x, x ′ ) to KB . Finally, Lemma 22 allows to assume R = ∈ Γ instead of the stronger R = ∈ Γ. The reasoning is similar for the other restrictions. ✷

The two following lemmata concern conjunctive manifestations. The proof of the first one follows firstly from the definition of the abduction problem.

Lemma 28 Let P = (V, H, M, KB ) be an instance of an abduction problem, where

M = (ϕ 1 ∧ • • • ∧ ϕ p
) is a conjunction of formulas, and let E ⊆ H. Then E is an explanation for P if and only if for all i ∈ {1, . . . , p} it is an explanation for (V, H, ϕ i , KB ).

Lemma 29 Let P = (V, H, M, KB ) be an instance of an abduction problem where M is a term. Let ℓ be a literal formed upon a fresh variable m / ∈ V , and write C for the clause (ℓ ∨ ℓ ′ ∈M ℓ ′ ). Then P has an explanation if and only if P ′ = (V ∪ {m}, H, ℓ, KB ∧ C) has one.

PROOF. Assume first that P ′ has an explanation E ′ . We first show that KB ∧ E ′ entails ℓ ′ ∈M ℓ ′ . Assume to the contrary that there is a model µ

of KB ∧ E ′ ∧ ( ℓ ′ ∈M ℓ ′ ). Then since m occurs only in C and ℓ ′ ∈M ℓ ′ ⊂ C, extending µ by µ |= ℓ yields a model of KB ∧ C ∧ E ′ ∧ ℓ, which contradicts the fact that E ′ is an explanation for P ′ . Thus KB ∧ E ′ entails ℓ ′ ∈M ℓ ′ , that is, M . Now since KB ∧ C ∧ E ′ is satisfiable, a fortiori KB ∧ E ′ is satisfiable.
Finally, E ′ is an explanation for P .

Conversely, assume that P has an explanation E. Then by definition of an explanation, there is a model µ of KB ∧ E; thus µ ′ defined to agree with µ over V and to satisfy ℓ is a model of KB ∧ C ∧ E. Now we also have KB ∧ E |= M . It follows that KB ∧ C ∧ E |= ℓ, and finally, E is an explanation for P ′ . ✷

Tools and methods for studying abduction

In this section we present the main generic methods used in the literature for studying abduction problems from a computational point of view.

Complexity of satisfiability and deduction

By definition, solving an abduction problem involves solving a satisfiability and a deduction problem. We therefore recall some definitions and well-known complexity results about these two problems.

Problem 30 (Sat(Γ)) Let Γ be a constraint language. An instance P of Sat(Γ) is a knowledge base KB over Γ, and the question is whether there exists at least one model of KB .

Problem 31 (Deduction(Γ,M)) Let Γ be a constraint language and let M be a class of formulas. An instance P of Deduction(Γ,M) is a tuple (KB , Q), where

• KB is a knowledge base over Γ, and

• Q is a formula in M.
The question is whether KB entails Q.

Schaefer classified the complexity of Sat(Γ) for all possible finite constraint languages Γ [START_REF] Schaefer | The complexity of satisfiability problems[END_REF]. Together with well-known results about the infinite languages studied here (see in particular [START_REF] Dowling | Linear-time algorithms for testing the satisfiability of propositional Horn formulae[END_REF] and [START_REF] Aspvall | A linear-time algorithm for testing the truth of certain quantified Boolean formulas[END_REF]) we have the following theorem.

Theorem 32 (complexity of Sat) Let Γ be a finite constraint language. Then Sat(Γ) is in

P if Γ ⊆ II 0 , Γ ⊆ II 1 , Γ ⊆ IE 2 , Γ ⊆ IV 2 , Γ ⊆ ID 2 , or Γ ⊆ IL 2 . Otherwise, it is NP-complete. Moreover, Sat(C) is in P when C is one of C Horn , C dHorn , C bij , E aff , C 0v , and C 1v .
From the well-known facts that KB entails Q if and only if KB ∧ ¬Q is unsatisfiable, and that KB entails Q 1 ∧ Q 2 if and only if it entails Q 1 and it entails Q 2 , we have the following two corollaries of Theorem 32, which we will use in the paper. if there are a variable x and two clauses of the forms (x ∨ C 1 ) and (¬x ∨ C 2 ) in KB , and removing clauses which are tautological or include others.

Projection

We will also use the notion of projection as a tool for studying the abduction problem. This notion is similar to the well-known notion of elimination of middle terms, or existential abstraction, and its use for abduction has been proposed in [START_REF] Zanuttini | New polynomial classes for logic-based abduction[END_REF]. As for the complexity of computing projection in propositional logic, we refer the reader to [START_REF] Lang | Propositional independenceformula-variable independence and forgetting[END_REF].

Intuitively, projecting onto a set of variables V ′ amounts to existentially quantifying every other variable.

Definition 38 (projection of assignments) Let µ be an assignment to a set of variables V , and let V ′ ⊆ V . The projection of µ onto V ′ , denoted by µ |V ′ , is the assignment to V ′ which agrees with µ.

Definition 39 (projection of formulas) Let KB be a propositional formula or a conjunction of constraints, and let V ′ ⊆ Vars(KB ). A projection of KB onto V ′ is any knowledge base KB ′ with Vars(KB ′ ) ⊆ V ′ and whose set of models over

V ′ is {µ |V ′ | µ |= KB }.
Importantly, the projection of a formula is unique only up to logical equivalence. We will mainly use the following result. Its proof follows from Lemma 37 when the manifestation is a literal or clause, since it is well-known that a projection of a knowledge base KB onto a set of variables preserves the prime implicates of KB over this set [START_REF] Lang | Propositional independenceformula-variable independence and forgetting[END_REF]Proposition 16]. When the manifestation is a term of CNF, the proof follows from the literal or clause case together with Lemma 28.

Lemma 40 Let P = (V, H, M, KB ) be an instance of any abduction problem. Let V ′ be any set of variables with Vars(H) ∪ Vars(M ) ⊆ V ′ ⊆ V , and let KB ′ be a projection of KB onto V ′ . Then the explanations for (V ′ , H, M, KB ′ ) are exactly the explanations for P .

When computable efficiently, projection used as above allows to circumvent the difficulty of what Selman and Levesque call the support selection task [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF]. They argue that this task lies at the core of the computational difficulty of abduction, as witnessed by their study of the Horn case. We come back to this issue in our discussion (Section 15).

One case when a projection of a knowledge base can be computed efficiently is when this knowledge base has a polynomial number of prime implicates, all of which can be enumerated efficiently. This is so, e.g., for bijunctive knowledge bases, which allows us to derive most results in Section 11. However, this is not the only case, as the affine case shows (Section 12).

General case

In this section we only strengthen Eiter and Gottlob's statements [START_REF] Eiter | The complexity of logic-based abduction[END_REF] a little and adapt their proofs to our framework.

Proposition 41 (adapted from [START_REF] Eiter | The complexity of logic-based abduction[END_REF])

L-Abd(C CNF ,CNFs) is in Σ P 2 .
PROOF. Guess an explanation E ⊆ H and check that KB ∧ E is satisfiable. This verification is in NP by Theorem 32. Now, check that KB ∧ E |= M . This verification is in coNP by Theorem 33. Hence, the problem is in NP NP∪coNP = Σ P 2 . ✷ Proposition 42 (adapted from [START_REF] Eiter | The complexity of logic-based abduction[END_REF]) Let Γ be a constraint language satisfying Γ = BR. Then P-Abd(Γ,PosLits) and N-Abd(Γ,PosLits) are Σ P 2 -hard.

PROOF. Eiter and Gottlob [START_REF] Eiter | The complexity of logic-based abduction[END_REF] show that P-Abd(C CNF ,PosLits) is Σ P 2complete. Let Γ 3 be the constraint language containing all ternary relations that are the set of models of exactly one clause. It is well-known that every CNF is logically equivalent to a 3CNF formula with existentially quantified auxiliary variables. Reasoning as for Lemma 22, we get that P-Abd(C CNF ,Pos-Lits) ≡ P P-Abd(Γ 3 ,PosLits), and thus P-Abd(Γ 3 ,PosLits) is Σ P 2 -complete. Now, since Γ 3 = BR, we get that P-Abd(Γ,PosLits) is Σ P 2 -complete.

The claim for N-Abd(Γ,PosLits) follows since any positive hypothesis h can be changed to a negative one ¬h ′ , where h ′ is a fresh variable, up to adding

(h ∨ h ′ ) ∧ (¬h ∨ ¬h ′ ), i.e., h ↔ ¬h ′ , to KB . ✷
Note that, in particular, the hardness result in the preceding proposition holds for any finite constraint language Γ such that Γ = BR. We want to emphasize that, unless explicitly stated otherwise, all the hardness results in the paper for constraint languages Γ hold for any finite constraint language Γ ′ such that Γ ′ = Γ . This is important for us since we can only use Lemma 22 to derive new hardness results if the original (hard) abduction problem is defined over a finite constraint language.

8 0-valid and 1-valid languages

The "easy" abduction problems which we exhibit in this section are of a particular type. Indeed, for them the search space can be reduced to only one candidate explanation. The reasoning is similar to that for the definite Horn case (see, e.g., [START_REF] Eiter | The complexity of logic-based abduction[END_REF]Corollary 5.4]).

Lemma We now give two new results, which give some upper and lower bounds, respectively, for the complexity of P-Abd and N-Abd.

Proposition 45

The problem N-Abd(C 0v ,PosCNFs) is trivial, in the sense that an instance (V, H, M, KB ) has an explanation if and only if M is empty.

PROOF. If M is empty, then it is tautological, thus KB entails M . It follows that there is an explanation if and only if KB is satisfiable, which is necessarily the case since it is 0-valid. Now if M is nonempty, let µ 0 be the assignment of 0 to every variable in V .

Since KB is 0-valid and H is a set of negative literals, we have µ 0 |= KB ∧ E for any E ⊆ H. But since M is positive but not tautological, we also have µ 0 |= M . It follows that for all E ⊆ H we have KB ∧ E |= M and hence, no E ⊆ H can be an explanation. ✷ Proposition 46 Let Γ be a constraint language satisfying Γ = II 0 . Then P-Abd(Γ,PosLits) is Σ P 2 -hard. Similarly, if Γ is a constraint language satisfying Γ = II 1 , then N-Abd(Γ,PosLits) is Σ P 2 -hard.

Horn and dual Horn languages

In this section we build over a number of results given in the literature for Horn knowledge bases, mainly by Selman and Levesque [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF], Eiter, Gottlob, and Makino [START_REF] Eiter | The complexity of logic-based abduction[END_REF][START_REF] Eiter | On computing all abductive explanations from a propositional Horn theory[END_REF], and Khardon and Roth [START_REF] Khardon | Reasoning with models[END_REF].

Lemma 49 (see [START_REF] Khardon | Reasoning with models[END_REF] and [50, Lemma 1]) Let P = (V, H, M, KB ) be an instance of Abd(C Horn ), where M ∈ PosLits ∪ PosClauses ∪ PosTerms ∪ PosCNFs. Then P has an explanation if and only if it has a positive one.

Corollary 50 Let Γ be a Horn language, and let M be PosLits, PosClauses, PosTerms, or PosCNFs. Then L-Abd(Γ,M) ≡ P V-Abd(Γ,M) ≡ P P-Abd(Γ,M).

Proposition 51 (adapted from [20, Corollary 5.4]) L-Abd(C 1v -Horn ,Pos-CNFs) is in P.

PROOF. Let P = (V, H, M, KB ) be an instance. From Lemma 49 it follows that P has an explanation if and only if P ′ = (V, H ∩ V, M, KB ) has one. Now KB is 1-valid, thus KB ∧ (H ∩ V ) is satisfiable. Thus, by Lemma 43 P ′ has an explanation if and only if KB ∧ (H ∩ V ) entails M , which can be decided in polynomial time since KB is Horn (Theorem 33). ✷

The following result is new and gives quite a broad class of tractable abduction problems. Observe that by duality, it also shows that it is tractable to decide whether a CNF has a negative explanation with respect to a Horn knowledge base.

Proposition 52 P-Abd(C dHorn ,CNFs) is in P.

PROOF. Let P = (V, H, M, KB ) be an instance. We assume without loss of generality that KB is satisfiable (see the end of Section 3.1). Let H ′ be the set of all (positive) literals h ∈ H such that KB ∧ h is satisfiable; H ′ can be computed efficiently by testing every h ∈ H since KB is dual Horn. Then P has an explanation if and only if the instance (V, H ′ , M, KB ) has one, since every candidate explanation containing h for some literal h ∈ H \ H ′ would be inconsistent with KB . Now the set of models of a dual Horn knowledge base is closed under componentwise logical or (this is dual to the well-known closure of Horn theories under logical and, see, e.g., [START_REF] Schaefer | The complexity of satisfiability problems[END_REF]). Hence, since KB ∧ h is satisfiable for every h ∈ H ′ , KB ∧ H ′ is satisfiable. We now conclude from Lemma 43 that P has an explanation if and only if KB ∧ H ′ entails M , which can be decided in polynomial time since KB is dual Horn (Theorem 33). ✷

We finally give two hardness results. The proof of the first one follows directly from [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF] (V-Abd case, as reported in Theorem 18) together with Corollary 50.

Proposition 53 Let Γ be a constraint language satisfying Γ = IE 0 . Then P-Abd(Γ,PosLits) is NP-hard.

Proposition 54 Let Γ be a constraint language satisfying Γ = IE 0 . Then P-Abd(Γ,NegLits) and V-Abd(Γ,NegLits) are NP-hard.

PROOF. By Proposition 53, P-Abd(Γ,PosLits) is NP-hard. Now the clause (¬x∨¬y) is in IE 0 , thus Lemma 29 gives a reduction from P-Abd(Γ,PosLits) to P-Abd(Γ,NegLits) with choosing a negative literal for ℓ. The proof is similar for V-Abd, using Theorem 18 for hardness of V-Abd(Γ,PosLits). ✷

Bijunctive and IHS-B languages

Bijunctive and IHS-B restrictions share an important property, summarized in the next lemma.

Lemma 55 Let C be any of C bij , C impl , C IHSB+/k , or C IHSB-/k for some k.

Then every prime implicate of a knowledge base KB over C is in C, and the set of all these prime implicates can be computed in time polynomial in the size of KB. In particular, there are only a polynomial number of them.

PROOF. It is easily seen that all the prime implicates are in C. Indeed, all of them can be generated by resolution, and as is easily seen from the forms of the clauses, resolution preserves each class in the statement. Thus, starting from a formula over C, only clauses in C can be generated.

Clearly, the number of prime implicates of a theory over C bij , C impl , C IHSB+/k , or C IHSB-/k is polynomial in the size of the theory, since the size of clauses over C is bounded by 2 or k in all cases. All can be generated in polynomial time since one can simply generate all clauses of size 2 (resp. k) and for each one, test whether it is entailed by KB and none of its proper subclauses is, in polynomial time in all cases (Theorem 33). ✷

Remark 56

The fact that the language is fixed, and thus that k is fixed for languages C IHSB -/k and C IHSB+/k , is crucial in the proof of Lemma 55. Indeed, the statement does not hold for infinite languages C IHSB-and C IHSB + .

Bijunctive and IHS-B languages: Upper bounds

We first give easy consequences of Lemmata 37 and 55, which generalize folklore results based on prime implicate generation (see in particular Marquis' survey [START_REF] Marquis | Consequence finding algorithms[END_REF]. The algorithm consists of generating the prime implicates of KB over Vars(H) ∪ Vars(M ) until one as in Lemma 37 is found or all have been tested.

Proposition 57 Let C be any of C bij , C neg,= , or C IHSB-/k for some k ∈ N.

Then L-Abd(C,Clauses) is in P.

PROOF. The only case not handled by Lemma 55 is C neg,= , because of the equality relation. We show that if a knowledge base KB over C neg,= contains no equality constraint, then it has a polynomial number of prime implicates, all of which can be generated efficiently. We then conclude with Lemma 21.

Indeed, since clauses in KB are either unit positive or negative, it can be seen that once resolution has been applied to each pair of clauses consisting of a positive and a negative one, it cannot be applied any more. Since there can be at most one positive clause per variable, all prime implicates can be generated in polynomial time. ✷ Proposition 58 L-Abd(C IHSB-,PosClauses) is in P.

PROOF. By a reasoning similar to that in the proof of Lemma 55 we have that every prime implicate of a IHS-B-theory is IHS-B-. Now since the only IHS-B-clauses which contain at least one positive literal are unary and implicative ones, from Lemma 37 we get that the only minimal candidate explanations of an instance of L-Abd(C IHSB -,PosClauses) are the empty one and those restricted to only one (positive) literal, all of which can be tested efficiently. ✷

We now give two new tractability results, for which some more work is needed because of conjunctive manifestations.

Proposition 59 L-Abd(C impl ,PosCNFs) is in P.

PROOF. First observe that since KB is bijunctive, one can decide in polynomial time whether ∅ is an explanation, by deciding whether KB is satisfiable and entails M . Thus we assume hereafter that ∅ is not an explanation.

Let P = (V, H, M, KB ) be an instance of the problem, and assume first that M consists of a single (positive) clause C. In this case, since the only prime implicates of a knowledge base over C impl are in C impl (Lemma 55), we conclude that a set E ⊆ H is an explanation for P if and only if KB ∧ E is satisfiable and there is a literal ℓ ∈ E such that KB ∧ (ℓ) entails C (or, as a subcase, E = ∅ is an explanation); moreover, such an ℓ has to be a positive literal. PROOF. Let (V, H, M, KB ) be an instance. We first invoke Lemma 21 for assuming without loss of generality that KB contains no equality constraint. Now, reasoning as in Lemma 57 we get that the only prime implicates of KB which contain at least one positive literal are unit clauses. Thus, by Lemma 37 there is an explanation for a positive clause C of M if and only if ∅ or {m}, for some m in C, is an explanation. It then follows from Lemma 28 that there is an explanation for M if and only if H contains at least one variable in each clause of M which is not entailed by KB alone, which can be decided efficiently. ✷

Bijunctive and IHS-B languages: Lower bounds

We will mainly use the following lemma, which provides a class of reductions from satisfiability problems to abduction problems. The intuition behind the reduction is that we reduce the test for satisfiability of a set of clauses in a formula to a test for explainability of the satisfaction of these clauses, where satisfaction of a clause is explainable by any of the literals in this clause. The clauses which are not transformed by the reduction serve as constraints over the possible explanations. Importantly, this is exactly the intuition behind our characterization of tractable vs. NP-complete abduction problems, as we shall see in Section 15.

Lemma 61 Let ϕ = i∈I C i be a CNF formula, where for all i, C i = j∈J i ℓ i,j and every ℓ i,j is a literal. Let I ′ ⊆ I be a set of indices. For all i ∈ I ′ let x i be a new variable (x i / ∈ Vars(ϕ)), and let s i be a literal formed upon x i (intuitively, "clause C i is satisfied"). Finally, define

• KB = i∈I\I ′ C i ∧ i∈I ′ j∈J i (ℓ i,j ∨ s i ), • V = Vars(ϕ) ∪ {x i | i ∈ I}, • H = {ℓ i,j | i ∈ I, j ∈ J i } ∪ {ℓ i,j | i ∈ I, j ∈ J i }, and • M = i∈I s i .
Then ϕ is satisfiable if and only if the abduction problem P = (V, H, M, KB ) has an explanation. The same result holds with H = {ℓ i,j | i ∈ I, j ∈ J i }.

PROOF. Assume first that ϕ has a model µ, and define E to be the set of all literals in H which are satisfied by µ. Then since µ satisfies C i for all i ∈ I, it satisfies C i for all i ∈ I \ I ′ ; now define the assignment µ ′ to V to agree with µ over Vars(ϕ) and to satisfy every s i . Then µ ′ satisfies C i for every i ∈ I \ I ′ and (ℓ i,j ∨ s i ) for every i ∈ I, j ∈ J i , thus it satisfies KB . Moreover, clearly µ ′ satisfies E. Finally, KB ∧ E is satisfiable.

We now show that KB ∧ E entails M . Assume to the contrary that KB ∧ E ∧ ( i∈I s i ) is satisfiable. Then there is an i ∈ I such that KB ∧ E ∧ s i is satisfiable. Write µ ′ for one of its models. Then µ ′ satisfies E, thus it agrees with µ over Vars(H); then since µ satisfies ϕ, µ ′ satisfies ℓ i,j for at least one j ∈ J i . Thus µ ′ satisfies ℓ i,j ∧ s i , which contradicts the fact that it satisfies KB . Finally, KB ∧ E entails M , and E is an explanation for P .

Conversely, assume that P has an explanation E. Then there is a model µ of KB ∧ E, and we show that µ |Vars(ϕ) is a model of ϕ. First, for all i ∈ I \ I ′ , µ satisfies C i since C i is in KB . Now assume, towards a contradiction, that there is an i ∈ I ′ such that for all j ∈ J i , µ satisfies ℓ i,j . Define the assignment µ ′ to agree with µ over V \ {x i } and to satisfy s i . Then µ ′ satisfies KB ∧ E but does not satisfy M , which contradicts the fact that E is an explanation for P . It follows that for all i ∈ I ′ , µ satisfies ℓ i,j for at least one j ∈ J i , and thus it satisfies C i . Finally, µ satisfies ϕ, as desired. ✷ Based on this general reduction, we are able to give new hardness results for several abduction problems with bijunctive and IHS-B knowledge bases.

Proposition 62 Let Γ be a constraint language. Then,

• if Γ = IS 2
11 , V-Abd(Γ,PosTerms) and P-Abd(Γ,PosTerms) NPhard; PROOF. We first prove the case Γ = IS 2 11 . From Theorem 32 it follows that Sat({(x 1 ∨x 2 ∨x 3 ), (¬x 1 ∨¬x 2 )}) is NP-complete. Now Lemma 61 gives a reduction from this problem to V-Abd(Γ,PosTerms) or to P-Abd(Γ,Pos-Terms). Indeed, let ϕ = i∈Ip (x i,1 ∨ x i,2 ∨ x i,3 ) ∧ i∈In (¬x i,1 ∨ ¬x i,2 ), where I p , I n are two disjoint sets of indices. Then by Lemma 61 we have the desired reduction by choosing I ′ = I p and for all i ∈ I ′ , s i = x i .

• if Γ = IM , V-Abd(Γ,Terms) is NP-hard; • if Γ = IS 2 0 , V-Abd(Γ,
The proof is similar for cases Γ = IM and Γ = IS 2 0 , up to considering respectively,

• Sat({(x 1 ∨ x 2 ∨ x 3 ), (¬x 1 ∨ ¬x 2 )}), I ′ = I p ∪ I n , for all i ∈ I p , s i = x i , and
for all i ∈ I n , s i = ¬x i , and

• Sat({(x 1 ∨ x 2 ), (¬x 1 ∨ ¬x 2 ∨ ¬x 3 )}), I ′ = I n , and for all i ∈ I ′ , s i = x i . ✷
The next proposition is a special case. Indeed, observe that Γ is necessarily infinite, since any finite language included in IS 11 must have bounded width and thus, be included in IS k 11 for some k ∈ N (yielding Γ ⊆ IS k 11 IS 11 ). This special case is discussed in Section 13.2.

Proposition 63 Let Γ be an (infinite) language satisfying Γ = IS 11 . Then V-Abd(Γ,NegLits) and P-Abd(Γ,NegLits) are NP-hard.

PROOF.

Proposition 62 shows that V-Abd(Γ,PosTerms) is NP-hard if Γ = IS 2 11 . Now Lemma 29 gives a reduction from this problem to V-Abd(Γ ′ ,NegLits), where Γ ′ = IS 11 , by choosing a negative literal for ℓ. The proof is similar for P-Abd(Γ,PosTerms). ✷

Affine languages

The main tool which we will use with affine formulas is projection. This will be done through the following lemma.

Lemma 64 ( [START_REF] Zanuttini | New polynomial classes for logic-based abduction[END_REF]) Let KB be an affine formula, and let V ′ ⊆ Vars(KB ). Then there is a projection of KB onto V ′ which is affine, and such a projection can be computed in polynomial time.

Interestingly, contrary to the case of bijunctive and bounded IHS-B knowledge bases, tractability of projection here is not a consequence of a polynomial number of prime implicates. Indeed, even in the case of a single linear equation of the form (x 1 ⊕ • • • ⊕ x n = 0), an affine formula may have an exponential number of prime implicates (2 n-1 in the example, namely all clauses over exactly x 1 , . . . , x n with an odd number of negative literals).

Affine languages: Upper bounds

We first restate Nordh and Zanuttini's result [START_REF] Nordh | Propositional abduction is almost always hard[END_REF] about affine formulas of width 2. Indeed, they state it for finite languages, but their proof obviously holds for the corresponding infinite language as well.

Proposition 65 (adapted from [START_REF] Nordh | Propositional abduction is almost always hard[END_REF]) L-Abd(E aff /2 ,Terms) is in P.

We now give new tractability results. So as to use projection consistently with its definition, observe that in the affine case we can assume Vars(H) ∪ Vars(M ) ⊆ Vars(KB ) without loss of generality. Indeed, for any variable x ∈ (Vars(H)∪Vars(M ))\Vars(KB ), a fresh variable new x can be introduced and x ⊕ new x = 0 added to KB without changing the set of explanations.

Proposition 66 L-Abd(E aff ,Clauses) is in P.

PROOF. Consider an instance (V, H, M, KB ). Note that since (x = y) ≡ (x⊕y = 1) ∈ E aff we can use Lemma 27 to reduce the instance to an equivalent one (V ′ , H ′ , M ′ , KB ′ ) where M ′ is a positive clause and H ′ is a set of negative literals. Now, in order to eliminate all variables that are neither in H ′ nor in M ′ , project KB ′ onto V ′′ = Vars(H ′ ) ∪ Vars(M ′ ), getting a formula KB ′′ over the set of variables V ′′ . Now since (x = y) ≡ (x ⊕ y = 0) ∈ E aff we can assume Vars(H ′ ) ∩ Vars(M ′ ) = ∅ without loss of generality, since any variable x in the intersection could be duplicated into x H and x M up to adding (x H = x M ) to KB ′′ . We now have an instance P = (V ′′ , H ′ , M ′ , KB ′′ ) where KB ′′ is a set of linear equations, H ′ is the set of negative literals {¬x |x ∈ V ′′ \ Vars(M ′ )}, and M ′ is a positive clause. We can then use exactly the same reduction as in [START_REF] Nordh | Propositional abduction is almost always hard[END_REF]Proposition 11] to show that P has an explanation if and only if the negative term ¬M ′ does not follow from KB ′′ when circumscribing all variables. Since this problem is in P if ¬M ′ is a single literal [START_REF] Durand | The inference problem for propositional circumscription of affine formulas is coNP-complete[END_REF]Theorem 7], and the case of a term is easily seen to be polynomial-time reducible to it, we have the result. ✷

The next proposition will use the notion of a full explanation. Given an instance P = (V, H, M, KB ) of any abduction problem, an explanation E for P is said to be full if Vars(E) = Vars(H). What we will use is the fact that an instance of V-Abd, for any restriction on the manifestation, has an explanation if and only if it has a full one. Indeed, given a nonfull explanation E, since KB ∧ E has at least one model µ, it is easily seen that the set E ′ defined to be the set of all literals over H assigned true by µ is a full explanation for P .

Proposition 67 V-Abd(E aff ,Terms) is in P.

PROOF. Let P = (V, H, M, KB ) be an instance, and write V H for Vars(H). We first consider the case of a positive literal as a manifestation, i.e., M = m for some m ∈ V (the case of a negative literal is dual). Assume m / ∈ H, which is without loss of generality since otherwise P has an explanation if and only if KB ∧ m is satisfiable, which can be decided efficiently. Write KB H∪{m} for an affine projection of KB onto V H ∪ {m}. By Lemma 64 such a knowledge base can be computed in polynomial time. Now define P H∪{m} = (V H ∪ {m}, H, m, KB H∪{m} ). By Lemma 40, P H∪{m} has an explanation if and only if P has one. Moreover, obviously, if m does not occur in KB H∪{m} then P H∪{m} has no explanation. Otherwise, let Eqn m = (m ⊕ X x = a) be an equation of KB H∪{m} containing m. Now let KB H,m=1 be an affine projection of KB H∪{m} ∧ m onto V H . We claim that the full explanations of P H∪{m} are in bijection with the models of KB H,m=1 . Indeed, let E be a full explanation for P H∪{m} . Then by definition of an explanation, there is a model µ of KB H∪{m} ∧ E ∧ m; thus µ |V H satisfies KB H,m=1 ∧ E, and thus KB H,m=1 . Conversely, let µ be a model of KB H,m=1 , and write E for the set of all literals over V H and satisfied by µ; we show that E is a full explanation of P H∪{m} . First, KB H,m=1 ∧ E is satisfiable, thus KB H∪{m} ∧ m ∧ E is satisfiable, and thus KB H∪{m} ∧ E is satisfiable. We are thus left with proving KB H∪{m} ∧ E |= m. Assume towards a contradiction that there is a model µ ′ of KB H∪{m} ∧ E ∧ ¬m. In particular, µ ′ satisfies ¬m and agrees with µ over Vars(E) = V H . Moreover, since µ is a model of KB H,m=1 , it satisfies the equation X x = a ⊕ 1 (i.e., Eqn m with m = 1); it follows that µ ′ satisfies X x = a ⊕ 1; since it also satisfies ¬m, it satisfies m ⊕ X x = a ⊕ 1. Thus it does not satisfy equation Eqn m , which contradicts the fact that it satisfies KB H∪{m} .

We conclude that in the case of a single literal m as the manifestation, the full explanations of P H∪{m} are exactly the models of KB H,m=1 . It follows from Lemma 28 that the full explanations in the case of a manifestation

M = m 1 ∧ • • • ∧ m k are exactly the models of KB H,m 1 =1 ∧ • • • ∧ KB H,m k =1 .
Since every KB H,m i =1 is an affine formula and can be computed in polynomial time, we finally get a polynomial algorithm. ✷

Affine languages: Lower bounds

We finally give hardness proofs for affine languages, all of which are new. To that aim, we use original reductions from satisfiability problems, inspired by the clausal case (Lemma 61).

Proposition 68 Let Γ be a constraint language satisfying Γ = IL. Then L-Abd(Γ,PosTerms) is NP-hard.

PROOF. We give a reduction from Sat({(x 1 ⊕x 2 ⊕x 3 ⊕x 4 = 0), (x 1 ), (¬x 1 ∨ ¬x 2 )}), which is NP-complete by Theorem 32. Let ϕ = ϕ 0 ∧ i∈I (¬x i,1 ∨¬x i 2 )∧ k∈K (x k = 1), where ϕ 0 contains only equations of the form (x 1 ⊕x 2 ⊕x 3 ⊕x 4 = 0). For all i ∈ I let s i / ∈ Vars(ϕ) be a fresh variable (intuitively meaning that clause i is satisfied), and for all i ∈ I let p i,1 , n i,1 , p i,2 , n i,2 / ∈ Vars(ϕ) be four fresh variables ("p" stands for "positive" and "n" for "negative"). Write H p for the set of all p i,j 's and H n for that of all n i,j 's. We define an instance P = (V, H, M, KB ) of L-Abd(Γ,PosTerms) by

• V = Vars(ϕ) ∪ {s i | i ∈ I} ∪ H p ∪ H n , • H = N (Vars(ϕ)) ∪ {x k | k ∈ K} ∪ H p ∪ N (H n ), • M = {s i | i ∈ I} ∪ {x k | k ∈ K}, and • KB = ϕ 0 ∧ i∈I (x i,1 ⊕ p i,1 ⊕ n i,1 ⊕ s i = 0) ∧ i∈I (x i,2 ⊕ p i,2 ⊕ n i,2 ⊕ s i = 0).
The intuition is that the new equations play the role of "implications" ¬x i,1 → s i and ¬x i,2 → s i .

We claim that P has an explanation if and only if ϕ is satisfiable. First, if µ is a model of ϕ, then clearly {¬x | x ∈ Vars(ϕ) and µ(x) = 0} ∪ {x k | k ∈ K} ∪ {p i,j , ¬n i,j | i ∈ I and µ(x i,j ) = 0} is an explanation for P . Conversely, assume E is an explanation for P . Then since for all i ∈ I, s i , p i,1 , p i,2 , n i,1 , n i,2 only occur in equations (x i,j ⊕ p i,j ⊕ n i,j ⊕ s i = 0), E has to contain p i,j or ¬p i,j and n i,j or ¬n i,j for at least one j ∈ {1, 2}. Indeed, otherwise flipping the values of s i and some p i,j 's or n i,j 's in a model of KB ∧ E ∧ M would yield a model of KB ∧ E ∧ ¬s i , contradicting the fact that E is an explanation for P . Thus for all i ∈ I there is a j ∈ {1, 2} such that E contains p i,j and ¬n i,j , since ¬p i,j , n i,j / ∈ H. Now by definition of an explanation, there is a model of KB ∧ E ∧ M , and it follows from the reasoning above that this model satisfies ¬x i,1 or ¬x i,2 for all i ∈ I, since otherwise one of the equations (x i,j ⊕ p i,j ⊕ n i,j ⊕ s i = 0) would not be satisfied. Finally, it satisfies x k for all k ∈ K because these literals are in M . Thus, defining µ to be the projection of this model onto Vars(ϕ), we get that µ is a model of ϕ, as desired. ✷ Proposition 69 Let Γ be a constraint language satisfying Γ = IL 1 . Then N-Abd(Γ,PosTerms) is NP-hard. Similarly, if Γ is a constraint language satisfying Γ = IL 0 , then P-Abd(Γ,PosTerms) is NP-hard.

PROOF. As regards IL 1 , the proof is similar to that of Proposition 68, except that we start from Sat({(x 1 ⊕ x 2 ⊕ x 3 = 1), (¬x 1 ∨ ¬x 2 )}), we introduce only one fresh variable n i,j per occurrence of variable in a negative clause, we build equation (x i,j ⊕ n i,j ⊕ s i = 1) instead of (x i,j ⊕ p i,j ⊕ n i,j ⊕ s i = 0), and we only add ¬n i,j to H.

The proof is dual for IL 0 , starting from Sat({( PROOF. We consider the case of V-Abd. The other cases follow from it using Lemmata 20 and 27.

x 1 ⊕ x 2 ⊕ x 3 = 0), (x 1 ∨ x 2 )}) and building (x i,j ⊕ p i,j ⊕ p ′ i,j ⊕ s i = 0) with p i,j , p ′ i,
We give a reduction from the satisfiability problem for CNF formulas. Let ϕ = i∈I C i be a CNF formula. For every variable x ∈ Vars(ϕ) let p x , n x / ∈ Vars(ϕ) be two fresh variables ("p" stands for "positive" and "n" for "negative"). Let ϕ ′ be the CNF formula obtained from ϕ by replacing every positive occurrence x of a variable in a clause with the positive literal p x , and every negative occurrence ¬x of a variable with the positive literal n x . By construction, ϕ ′ is a positive CNF.

We define an instance P of V-Abd(Γ,PosCNFs) as follows:

• KB = x∈Vars(ϕ) (p x = n x ), • V = {p x | x ∈ Vars(ϕ)} ∪ {n x | x ∈ Vars(ϕ)}, • M = ϕ ′ , and • H = {p x | x ∈ Vars(ϕ)} ∪ {¬p x | x ∈ Vars(ϕ)}.
Then it is easily seen that if ϕ is satisfiable with a model µ, then E defined to be {p x | µ(x) = 1} ∪ {¬p x | µ(x) = 0} is an explanation for P . Conversely, if E is an explanation for P , then it is easily seen that any assignment to Vars(ϕ) satisfying µ(x) = 1 (resp. µ(x) = 0) for all p x ∈ E (resp. ¬p x ∈ E) is a model of ϕ, which concludes the proof. ✷ Proposition 72 Let Γ be a constraint language satisfying Γ = IL. Then V-Abd(Γ,PosCNFs) is NP-hard.

PROOF. We give a reduction from the satisfiability problem for CNF formulas, similar to the one in the proof of Proposition 71. Let ϕ = i∈I C i be a CNF formula. For every variable x ∈ Vars(ϕ) let p x , n x / ∈ Vars(ϕ) be two fresh variables ("p" stands for "positive" and "n" for "negative"). Let ϕ ′ be the CNF formula obtained from ϕ by replacing every positive occurrence x of a variable in a clause with the positive literal p x , and every negative occurrence ¬x of a variable with the positive literal n x . By construction, ϕ ′ is a positive CNF. Moreover, let x 1 , . . . , x 4 / ∈ Vars(ϕ).

We define an instance P of V-Abd(Γ,PosCNFs) as follows:

• KB = (x 1 ⊕ x 2 ⊕ x 3 ⊕ x 4 = 0) ∧ x∈Vars(ϕ) (p x ⊕ n x ⊕ x 3 ⊕ x 4 = 0), • V = {p x | x ∈ Vars(ϕ)} ∪ {n x | x ∈ Vars(ϕ)} ∪ {x 1 , x 2 , x 3 , x 4 }, • M = x 1 ∧ (x 3 ∨ x 4 ) ∧ ϕ ′ , and • H = {p x , ¬p x | x ∈ Vars(ϕ)} ∪ {x 1 , ¬x 1 , x 2 , ¬x 2 }.
The idea is that the manifestations x 1 ∧ (x 3 ∨ x 4 ) together with the equation x 1 ⊕x 2 ⊕x 3 ⊕x 4 = 0 in KB force every model µ of KB ∧ E (for any explanation E) to satisfy µ(x 3 ) = µ(x 4 ). Consequently, the equations (p x ⊕n x ⊕x 3 ⊕x 4 = 0) force µ(p x ) = µ(n x ) for any model µ of KB ∧ E (and any explanation E).

It is easily seen that if ϕ is satisfiable with a model µ, then E defined to be {p

x | µ(x) = 1} ∪ {¬p x | µ(x) = 0} ∪ {x 1 , ¬x 2 } is an explanation for P .
Conversely, if E is an explanation for P , then KB ∧ E is satisfiable and entails x 1 ∧ (x 3 ∨ x 4 ) ∧ ϕ ′ . Now, assume that there is a model µ of KB ∧ E such that µ(x 3 ) = µ(x 4 ) = 1. Note that x 3 and x 4 do not occur in H and that they occur together in every equation in KB . So, it is easy to see that there is also a model µ ′ of KB ∧ E such that µ ′ (x 3 ) = µ ′ (x 4 ) = 0. This is a contradiction with the fact that E is an explanation, since µ ′ does not satisfy (x 3 ∨ x 4 ). Hence, any model µ of KB ∧ E satisfy µ(x 3 ) = µ(x 4 ) and consequently, µ(p x ) = µ(n x ) for all x ∈ Vars(ϕ). Hence, the assignment µ ′ to Vars(ϕ) defined by µ ′ (x) = µ(p x ) for all x ∈ Vars(ϕ) is a model of ϕ. ✷

For the next proposition, observe that even the empty language Γ = ∅ satisfies Γ = IBF .

Proposition 73 Let Γ be a constraint language satisfying Γ = IBF . Then V-Abd(Γ,CNFs) is NP-hard.

PROOF. Recall than IBF only contains the equality relations. We give a reduction from the satisfiability problem for CNFs. Let ϕ be a CNF, we define the following instance P of V-Abd(Γ,CNFs):

• KB is the empty CNF (always satisfied),

• V = Vars(ϕ),

• M = ϕ, and

• H = Lits(Vars(ϕ)).
Then it is easily seen that the (full) explanations of P correspond exactly to the models of ϕ. ✷

Summary and complete classification

We are now in position to give a complete picture of the complexity of propositional abduction for the 48 restrictions over hypotheses and manifestations. By a "complete" picture, we mean that our results give the complexity of abduction for any constraint language and for any class of clauses or equations, as explained in Section 13.2.

Summary of results

The complete complexity picture of abduction in given in Table 3. In this table, for each restriction on hypotheses and manifestations and each complexity class, the minimal and maximal languages in this class (with respect to language inclusion) are listed. More precisely, the languages listed on the first line in each cell are the maximal languages in the complexity class, and the languages on the second line are the minimal languages hard for the class.

As an example, consider the cell for NP-complete L-Abd problems where the manifestations are expressed by PosCNFs. The first row in this cell is C bij , C dHorn , E aff , C Horn , and the second row is IS 2 0 , IS 2 11 , ID, IV , IL. This means that L-Abd(Γ,PosCNFs) is NP-complete for any Γ such that Γ is a subset of one of the languages listed in the first row, and one of the languages on the second row is a subset of Γ . To further exemplify, consider the constraint language Γ = {R}, where R = {001, 010, 100, 111} (i.e., the relation expressed by x 1 ⊕ x 2 ⊕ x 3 = 1). Then, Γ ⊆ E aff and IL ⊆ Γ . Hence, by Proposition 35, L-Abd(Γ,PosCNFs) is in NP, and by Proposition 72 (together with the obvious reduction from V-Abd to L-Abd) L-Abd(Γ,PosCNFs) is NP-hard.

The fact that all the results in Table 3 can be derived from the results reported in the paper (in the manner described above) has been checked by a computer program, which is available from the authors. Also note that the results for negative restrictions on manifestations have been omitted from the table; to recover them, simply use Lemma 25.

Finally, we collapsed the rows concerning (positive) clauses and (positive) literals. Indeed, it turns out that the complexity is always the same for both types of manifestations. Section 15.4 gives an explanation for that fact.

On the completeness of the classification

In this section we motivate our claims that the classifications are complete in the sense that all constraint languages and classes of equations and clauses are covered.

We begin by noting that the upper bounds on the complexity of abduction problems in the paper, which are all given in terms of clausal and equational languages C, also hold for any constraint language Γ such that Γ ⊆ C . If Γ is a finite constraint language, then this is obvious since we can use a simple lookup table to translate a Γ-formula into a CNF or system of equations over C. For infinite constraint languages Γ the situation is slightly more involved. We make use of a result from [START_REF] Creignou | Preferred representations of Boolean relations[END_REF], stating that we can transform (in polynomial time) any Γ-formula where the relations are given in extension into an equivalent CNF-formula/system of equations over any clausal/equational language C from Table 1 such that Γ ⊆ C . Since all the upper bounds on the complexity of abduction in the paper are given for clausal and equational languages C from Table 1, we get that these upper bounds also apply to constraint languages Γ such that Γ ⊆ C . All our hardness results, except for a few special cases discussed below, are proved for finite constraint languages Γ. Obviously, using Lemma 22, these hardness results implies hardness for any constraint language Γ ′ such that Γ ⊆ Γ ′ . The exceptional constraint languages Γ for which we cannot prove hardness by first proving that some finite constraint language Γ ′ ⊆ Γ is hard and then applying Lemma 22, are:

• L-Abd(Γ,M), where Γ ∈ {IS 01 , IS 00 }, M ∈ {(Pos)Lits, (Pos)Clauses}, These cases are exceptional since they are all NP-complete (by Proposition 63 and obvious reductions), but if Γ is replaced by any finite Γ ′ ⊆ Γ, then the problems are in P. This is because these languages include relations described by clauses of arbitrary length, while their finite subsets only allow to express clauses of bounded length. Indeed, they only contain binary clauses and clauses with only one polarity, such as (¬x 1 ∨ • • • ∨ ¬x k ). So the only clauses with can be resolved against each other to infer a new clause are two binary clauses, or a "long" clause and a binary one, so in no case can a clause of length greater than k be inferred.

M P NP-C. coNP-C. Σ P 2 -C. V-Abd PosLits or C IHSB+/k , Cpos,=, C IHSB-, C bij , E aff , C 1v -Horn C dHorn , C Horn C CNF PosClauses IS 01 , IV , IE 0 IN Lits or C IHSB+/k , Cpos,=, C IHSB-/k , Cneg,=, C bij , E aff C dHorn , C Horn C CNF Clauses IS 01 , IS 11 , IV , IE IN PosTerms C impl , Cneg,=, E aff , C 1v -Horn C bij , C dHorn , C Horn C CNF IS 2 0 , IS 2 11 , IV IN Terms E aff C bij , C dHorn , C Horn C CNF IM , IS 2 0 , IS 2 1 IN PosCNFs C impl , Cneg,=, C 1v -Horn C bij , C dHorn , E aff , C Horn C CNF IS 2 0 , IS 2 11 , ID, IV , IL IN CNFs C bij , C dHorn , E aff , C Horn C CNF IBF IN P-Abd PosLits or C IHSB-, C bij , C dHorn , E aff , C 1v -Horn C Horn C 1v C CNF PosClauses IE 0 IN IN 2 , II 0 Lits or C IHSB-/k , Cneg,=, C bij , C dHorn , E aff , C 1v -Horn C Horn C 1v C CNF Clauses IS 11 IN IN 2 , II 0 PosTerms Cneg,=, E aff /2 , C dHorn , E 1v -aff , C 1v -Horn C bij , E aff , C Horn C 1v C CNF IS 2 11 , IL 3 , IL 0 IN IN 2 , II 0 Terms E aff /2 , C dHorn , E 1v -aff , C 1v -Horn C bij , E aff , C Horn C 1v C CNF IS 2 1 , IL 3 , IL 0 IN IN 2 , II 0 PosCNFs Cneg,=, C dHorn , E 1v -aff , C 1v -Horn C bij , E aff , C Horn C 1v C CNF IS 2 11 , ID, IL 0 IN IN 2 , II 0 CNFs C dHorn , E 1v -aff , C 1v -Horn C bij , E aff , C Horn C 1v C CNF IS 2 1 , ID, IL 0 IN IN 2 , II 0 N-Abd PosLits or C IHSB+/k , Cpos,=, C bij , E aff , C Horn , C 0v C dHorn C CNF PosClauses IS 01 IN 2 , II 1 Lits or C IHSB+/k , Cpos,=, C bij , C 0v -dHorn , E aff , C Horn C dHorn C 0v C CNF Clauses IS 01 IN IN 2 , II 1 PosTerms E aff /2 , C Horn , C 0v C bij , C dHorn , E aff C CNF IS 2 0 , IL 1 , IL 3 IN 2 , II 1 Terms E aff /2 , C 0v -dHorn , E 0v -aff , C Horn C bij , C dHorn , E aff C 0v C CNF IS 2 0 , IL 1 , IL 3 IN IN 2 , II 1 PosCNFs C Horn , C 0v C bij , C dHorn , E aff C CNF IS 2 0 , ID, IL 1 IN 2 , II 1 CNFs C 0v -dHorn , E 0v -aff , C Horn C bij , C dHorn , E aff C 0v C CNF IS 2 0 , ID, IL 1 IN IN 2 ,
As a sidenote we want to remark that in the literature on computational problems over restricted constraint languages there are two notions of tractability: local and global. A problem over a constraint language Γ is said to be locally tractable if the problem is tractable over every finite subset of Γ, and global tractability coincides with the tractability notion used in this paper. Thus, as first noted by Creignou [START_REF] Creignou | [END_REF] (and as should be obvious from the discussion above), the notions of global and local tractability disagree for the abduction problem. This highlights a difference between the complexity of abduction and many other computational problems over constraint language restrictions, such as Sat(Γ), for which the notions of local and global tractability coincide.

Coming back to the completeness of the classification, it is a tedious but straightforward task (thanks to Post's classification) to check that, for all constraint languages Γ and restrictions on hypotheses and manifestations considered in the paper (which are not in one of the special cases already treated above), our results show that either

• the abduction problem over Γ is in P as a consequence of Γ ⊆ C for some tractable clausal or equational language C, or • the abduction problem over Γ is NP-complete (coNP-complete, Σ P 2 -complete) as a consequence of Γ ′ ⊆ Γ for some finite NP-hard (coNP-hard, Σ P 2 -hard) constraint language Γ ′ , and Γ ⊆ C for some clausal or equational language C which is in NP (coNP, Σ P 2 ).

Hence, we have a classification for the complexity of abduction over any constraint language Γ and any combination of restrictions on hypotheses and manifestations considered in the paper.

When it comes to clausal and equational languages C, the reasoning is very similar. First note that all finite clausal/equational languages C are covered by our discussion about constraint languages above. This is because abduction over C has the same complexity as abduction over Γ when Γ and C are both finite and Γ = C. This is because finite languages allow us to use a simple lookup table to translate between the different representations in polynomial time. Hence, we can concentrate on infinite clausal/equational languages C. Now, by Lemma 22 any lower bound on the complexity of abduction over a finite constraint language Γ carries over to any (infinite) clausal or equational language C such that Γ ⊆ C . Moreover, the infinite clausal languages C corresponding to the exceptional cases discussed above (where lower bounds cannot be proved by reductions from finite constraint languages) can all be proved to be NP-hard by Proposition 63. For infinite clausal or equational languages C consisting only of either clauses or equations (and not in the exceptional cases discussed above) the results in the paper show that either

• the abduction problem over C is in P as a consequence of C ⊆ C ′ for some tractable clausal or equational language C ′ , or • the abduction problem over C is NP-complete (coNP-complete, Σ P 2 -complete) as a consequence of Γ ′ ⊆ C for some finite NP-hard (coNP-hard, Σ P 2 -hard) constraint language Γ ′ , and C ⊆ C ′ for some clausal or equational language C ′ which is in NP (coNP, Σ P 2 ).

The only remaining problem is upper bounds for infinite clausal and equational languages C expressed by both equations and clauses. For example, C = C neg,= ∪ {(x 1 ⊕ x 2 ⊕ x 3 = 1)}. Post's classification yields that all these infinite clausal/equational languages C satisfy C ∈ { C CNF , C 0v , C 1v }. It is very easy to verify that the (trivial) upper bounds that hold for abduction problems over C CNF , C 0v , and C 1v also hold for the corresponding abduction problems over C (see the proofs of Propositions 41, 44, and 45). Hence, our results cover any clausal and equational language.

As already mentioned, the authors have used a computer program to doublecheck the completeness of the classification.

Further restrictions

As evoked in Section 3.2, several restrictions on the problem were not considered until now but are worth investigating. It turns out that most of them do not affect the complexity of the problem.

Unsatisfiable and tautological manifestations

The first kind of restrictions is about the satisfiability of manifestations. For instance, in typical applications, abduction is the process of explaining a given observation of the world. As a consequence, one may assume that manifestations are always satisfiable.

We first give a straightforward result.

Proposition 74 Let P = (V, H, M, KB ) be an instance of any abduction problem. If M is tautological, then P has an explanation if and only if KB is satisfiable. If M is unsatisfiable, then P has no explanation.

Observe that one can efficiently recognize unsatisfiable and tautological literals (vacuously), clauses, or terms. Thus the complexity of abduction is not affected by the extra assumption that such manifestations are nontautological or satisfiable, since deciding whether the knowledge base is satisfiable is always at least as hard as abduction. As for CNFs, tautological ones can be efficiently recognized, but not unsatisfiable ones. Nevertheless, it turns out that the complexity is not affected either.

Proposition 75 L-Abd(Γ,CNFs) is polynomial-time reducible to L-Abd(Γ,CNFs) where the manifestation is guaranteed to be satisfiable. The same result holds for V-Abd, P-Abd, or N-Abd instead of L-Abd.

PROOF. Let (V, H, M, KB ) be an instance of L-Abd(Γ,CNFs). Let new be a fresh variable (new / ∈ V ), and let V ′ = V ∪ {new}, M ′ = M ∨ new. Clearly, from the CNF M a CNF M ′′ for M ∨ new can be computed efficiently by distributing ∨new to each clause, and M ′′ is satisfiable. We claim that (V ′ , H, M ′′ , KB ) has an explanation if and only if (V, H, M, KB ) has one. Indeed, if KB ∧ E is satisfiable and entails M , this is still true for M ′′ . Conversely, if KB ∧ E is satisfiable and entails M ∨ new, then we have that KB ∧ E ∧ ¬M ∧ ¬new is unsatisfiable. Since new does not occur at all in KB ∧ E ∧ ¬M (and ¬new alone is satisfiable), we have that KB ∧ E ∧ ¬M alone is unsatisfiable, that is, KB ∧ E |= M . ✷

Variables in hypotheses and manifestations

Another interesting kind of restrictions is over the variables allowed to occur in the set of hypotheses and in manifestations. In particular, it is interesting to consider cases where variables which do not occur in the knowledge base occur in hypotheses and manifestations. This indeed allows to model situations where the knowledge base tells nothing about a part of the abduction problem at hand. First of all, it turns out that allowing or not such extra variables in the set of hypotheses does not affect the complexity of abduction.

Proposition 76 Let Γ be a constraint language, and let P = (V, H, M, KB ) be an instance of Abd(Γ). Then for any explanation E for P there is an explanation E 1 for P such that E 1 ⊆ E and Vars(E 1 ) ⊆ Vars(KB )∪Vars(M ).

PROOF. Let E be an explanation for P , and let E 1 = E ∩ Lits(Vars(KB ) ∪ Vars(M )) and E 2 = E \ E 1 . Then clearly KB ∧ E 1 is satisfiable, since so is KB ∧ E. Now by definition of an explanation we have KB ∧ E 1 ∧ E 2 |= M . Since the left-hand side is satisfiable and Vars(E 2 ) is disjoint from Vars(KB ), Vars(E 1 ), and Vars(M ), we get that E 2 is irrelevant to the entailment relation. Thus E 1 alone is an explanation. ✷ As concerns variables occurring in manifestations, the situation is a bit more involved. The following lemma is relevant to the cases of literals, clauses, or terms, for which the complexity is not affected. Indeed, it shows that for such manifestations, one can consider independently the part of the manifestation which is over Vars(KB ) and the other part, with almost no computational overhead for the latter.

Proposition 77 Let Γ be a constraint language, and let P = (V, H, M, KB ) be an instance of Abd(Γ). If M = M 1 ∧ M 2 with Vars(M 1 ) ⊆ Vars(KB ) and Vars(M 2 ) ∩ Vars(KB ) = ∅, then for any explanation E for P there is a partition of E into {E 1 , E 2 } such that E 1 is an explanation for (V, H, M 1 , KB ) and E 2 |= M 2 holds.

Dually, if M = M 1 ∨ M 2 with Vars(M 1 ) ⊆ Vars(KB ) and Vars(M 2 ) ∩ Vars(KB ) = ∅, then for any explanation E for P there is a partition of

E into {E 1 , E 2 } such that E 1 is an explanation for (V, H, M 1 , KB ) or E 2 |= M 2 holds.
PROOF. Consider M = M 1 ∧ M 2 ; the case M = M 1 ∨ M 2 is similar. Let E be an explanation for P , and let E 1 = E ∩ Lits(Vars(KB )) and

E 2 = E \ E 1 .
Then by definition of an explanation we have

KB ∧ E 1 ∧ E 2 |= M 1 and KB ∧ E 1 ∧ E 2 |= M 2 .
In the first entailment relation, since Vars(M 1 ) ⊆ Vars(KB ∧ E 1 ) and Vars(E 2 )∩Vars(KB ∧ E 1 ) = ∅ hold, and the left-hand side is satisfiable, we get that E 2 is irrelevant, that is, KB ∧ E 1 alone entails M 1 ; since moreover KB ∧ E 1 ∧ E 2 is satisfiable, E 1 is an explanation for explain what makes it NP-complete. We also compare our observations with Bylander et al.'s about set-covering abduction [START_REF] Bylander | The computational complexity of abduction[END_REF].

We discuss the two most meaningful cases first, namely those of clausal Schaefer languages (Horn, dual Horn and bijunctive) with terms and literals as manifestations. The other cases are only briefly discussed afterwards.

Manifestations expressed by terms

Given restrictions on the abduction problem, we say that a literal is a valid hypothesis (resp. individual manifestation) if it can be part of H (resp. of M ) for some instance (V, H, M, KB ) of the problem. For instance, the valid individual manifestations for N-Abd(C CNF ,PosTerms) are all positive literals.

Fact 80 Let C be a clausal Schaefer language, and assume a restriction on hypotheses and a restriction of manifestations to PosTerms, NegTerms, or Terms. Then propositional abduction is NP-hard for C if and only if it is so with stronger restrictions or C can express both

• implication from hypotheses to individual manifestations, that is, ℓ H → ℓ M for any valid hypothesis ℓ H and valid manifestation ℓ M , and • forbidden combinations of hypotheses, that is, ℓ H,1 ∨ ℓ H,2 for any two valid hypotheses ℓ H,1 , ℓ H,2 .

For instance, P-Abd(C,PosTerms) is NP-hard exactly when C can express both (x 1 → x 2 ) and (¬x 1 ∨¬x 2 ) for any two variables x 1 , x 2 . P-Abd(C,Terms) is NP-hard exactly when P-Abd(C,PosTerms) or P-Abd(C,NegTerms) is NP-hard, or when C can express (x 1 → x 2 ), (x 1 → ¬x 2 ) (implication) and (¬x 1 ∨ ¬x 2 ).

Importantly, observe from Fact 80 that if abduction is NP-hard for, e.g., unrestricted terms as manifestations, then so it is for positive or for negative terms with the same restriction on hypotheses. That is, arbitrary combinations of polarities in the manifestation do not add to the complexity of the problem. The same holds for hypotheses, that is, being able to explain with unrestricted hypotheses (or sets of hypotheses closed under complement) is not harder than being able to explain with only positive or with only negative hypotheses.

The validity of Fact 80 is proved by the generic reduction given by Lemma 61, applied to each precise problem. More intuitively, the idea is that in the NPhard cases, each literal m to be explained in a term gives rise to several possible explanations, one for each implication h → m expressed by the knowledge base. Thus, each m gives rise to a disjunction of hypotheses, and the whole manifestation M gives rise to a conjunction of disjunctions (CNF) of hypothe-ses. Now if the knowledge base can forbid some combinations of hypotheses, we thus have a second CNF, which excludes some models of the first one as explanations. Since the clauses in the first CNF are unbounded, it is easily seen that this characterization of explanations captures a whole class of hard satisfiability problems.

As for the tractable cases, if no implication from hypotheses to individual manifestations can be expressed, then there cannot be any explanation, since an explanation for a term is an explanation for each of its literals (Lemma 28). Now if no conjunction of hypotheses can be forbidden, then the search space can be reduced to the conjunction of all hypotheses (Lemma 43).

Importantly, Fact 80 gives some intuition about the complexity of abduction for some classes of formulas which are not captured by Schaefer's framework of constraint languages. Consider for instance the class of acyclic Horn CNFs, that is, of Horn CNFs which do not contain any cyclic set of clauses of the form

{(• • • ∨ ¬x 1 ∨ • • • ∨ x 2 ), (• • • ∨ ¬x 2 ∨ • • • ∨ x 3 ), . . . (• • • ∨ ¬x k ∨ • • • ∨ x 1 ), }.
Clearly, such a formula can contain an arbitrary number of clauses equivalent to (h → m) and (¬h 1 ∨ ¬h 2 ) for variables h, m, h 1 , h 2 . Thus Fact 80 gives the intuition that explaining positive terms with positive hypotheses is NP-hard when the knowledge base is restricted to be an acyclic Horn CNF. This result has indeed been shown by Selman and Levesque [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF]. Note however that we cannot formally state Fact 80 for such general classes of formulas, since the ability to express a given relation would not be properly defined.

Another important remark is that in our generic reduction from the satisfiability problem, all variables (or all positive, all negative literals) not occurring in the query can be hypotheses while the problems remains hard. We come back to this point when comparing to the case of manifestations expressed by single literals and in the conclusion.

A parallel with set-covering abduction

In their seminal paper [START_REF] Bylander | The computational complexity of abduction[END_REF], Bylander et al. study the complexity of set-covering abduction, and also identify a frontier between some polynomial and some NPcomplete abduction problems.

In their framework, an abduction problem is given by a set of manifestations M , a set of hypotheses H (hypotheses and manifestations are atoms), and by a map e ("explains") from subsets of H to subsets of M . An explanation is a subset E of H such that e(E) = M and E is minimal for inclusion. The only assumptions about e is that the size of its representation is polynomial in the size of H and M , and that it is tractable to compute e(E) for E ⊆ H as well as a kind of inverse of e (we refer to their paper for details).

} ∈ I, h, h ′ ∈ H) ⇒ e(E) = ∅.
Observe that all independent problems are also monotonic. The notion of independence is adapted to incompatibility as follows. An incompatibility problem is said to be independent if e(E) = h∈E e({h}) as soon as there is no {h, h ′ } ∈ I such that h, h ′ ∈ E.

Proposition 81 ( [START_REF] Bylander | The computational complexity of abduction[END_REF]) The problem of deciding whether an explanation exists is in P for independent abduction problems and for monotonic abduction problems. It is NP-complete for independent incompatibility problems.

Although the framework is different from ours, it is clear that the condition for NP-hardness in Proposition 81 is very close to our Fact 80.

Incompatible pairs of hypotheses of Bylander et al.'s framework clearly correspond in our framework to sets of hypotheses E which are not consistent with the knowledge base (KB ∧ E is unsatisfiable) 3 . Now, since we study abduction in classical propositional logic, where the consequence relation |= is monotonic, our abduction problems are monotonic. Thus, leaving details out, our abduction problems are incompatibility monotonic problems in the terms of [START_REF] Bylander | The computational complexity of abduction[END_REF], where e is represented in intension by the knowledge base KB . It is also easily seen that any independent incompatibility problem can be transformed into a problem in our framework.

With this correspondence in mind, it is clear that Fact 80 confirms Bylander et al.'s results. Indeed, the condition for NP-hardness in Proposition 81 states that abduction is hard when some combinations of hypotheses are forbidden (expressiveness of implication from hypotheses to manifestations is implicit in their framework), but becomes tractable without this assumption. Thus our observation for terms as manifestations can be seen as generalizing Bylander et al.'s to more complex interactions between hypotheses, and between hypotheses and manifestations.

Manifestations expressed by literals

The condition for manifestations expressed by literals is a bit more involved than that for terms, but it can intuitively be seen as the condition allowing to capture the complexity of conjunctive manifestations because it allows to express (m

1 ∧ • • • ∧ m k → m).
Call submanifestation any literal which is neither a hypothesis nor the manifestation (intuitively, the m i 's in the previous implication). Given a polarity restriction (to positive, to negative, or to any literal), a submanifestation is said to be valid if it satisfies the restriction.

Fact 82 Let C be a clausal Schaefer language, and assume a restriction on hypotheses and a restriction of manifestations to PosLits, NegLits, or Lits. Observe that in general, depending on the restriction on submanifestations, there may be several different expressiveness conditions for the same restrictions on hypotheses and manifestations. Nevertheless, as in the case of terms as manifestations, it can be seen from Fact 82 that allowing arbitrary combinations of polarities for hypotheses makes the problem no harder than allowing only positive or negative sets of hypotheses (the corresponding statement for manifestations is obvious).

The proof of our observation can be derived from Lemmata 61 and 29. Intuitively, the "intermediate layer" serves to generate conjunctions of (intermediate) hypotheses needed to explain the manifestation, through each implication y 1 ∧ • • • ∧ y n → m where the y i 's are submanifestations. Thus the manifestation can be explained by a disjunction of conjunctions of submanifestations, each of which can be seen as a term which has to be explained by hypotheses. Thus, provided arbitrarily long conjunctions of submanifestations can entail the manifestation, the complexity is the same as in the case of a term.

An important difference to manifestations expressed by terms is that in general, NP-hardness arises when some "intermediate" set of literals can be expressed, where these literals can neither be hypothesized nor observed. For instance, this explains why the complexity of explaining single literals from Horn CNFs falls from NP-complete to polynomial when all variables except those in the manifestation are hypotheses, as shown by Selman and Levesque [START_REF] Selman | Abductive and default reasoning: a computational core[END_REF]. This also confirms their intuition that selecting the right set of literals is the computational core in abduction. Nevertheless, this intuition is confirmed only as far as literals are considered as manifestations. Indeed, as we have seen this is not the case for manifestations expressed by terms.

Finally, like for terms our characterization gives intuition about the complexity of abduction for classes of formulas which are not captured by Schaefer's framework. Consider for instance the class of monotone CNF formulas, that is, formulas in which every variable occurs always negated or always unnegated.

A variable which always occurs with the same polarity cannot be a submanifestation for an abduction problem like in Fact 82, since it should occur both on the right of implications coming "from the hypotheses layer"(and thus, unnegated) and on the left of implications "going to the manifestation layer" (and thus, negated). Thus if all variables are monotone, the intermediate layer has to be empty and thus, abduction should be tractable. We thus recover (the intuition about) a well-known result (see, e.g., [37, Section 4.2]).

Manifestations expressed by clauses or CNFs

We are now able to explain a posteriori why one can observe that the complexity of the abduction problem is always the same, may (positive) clauses or (positive) literals be used as manifestations.

To this aim, first observe that naturally, when the problem is hard for literals, then so it has to be for clauses. Now concerning tractable cases, we use the condition exhibited above for literals. Indeed, the condition states that abduction is tractable for literals if either

(1) the knowledge bases cannot express a "two-layers" set of implications, from hypotheses to literals, and from arbitrary combinations of the latter to the manifestation, (2) or no conjunction of hypotheses can be forbidden.

It is easily seen that Condition 2 is the same, may literals or clauses (or terms) be considered as manifestations. Now regarding Condition 1, if it is true with literals, then it has to be true for clauses, since literals are a special case of clauses. We thus deduce tractability exactly as for literals.

Let us mention that, as noted for example by Eiter and Makino [23, Section 5.2], there is a rather generic polynomial-time reduction from clausal manifestations to single-literal manifestations. The idea is that M = (ℓ 1 ∨ • • • ∨ ℓ k ) can be replaced with a literal ℓ, over a fresh variable, up to adding constraints ℓ i → ℓ (i = 1, . . . , k) to the knowledge base. This reduction covers many cases, but fails to explain, for instance, why P-Abd(C 1v -Horn ,Clauses) has the same complexity as P-Abd(C 1v -Horn ,Lits). Indeed, the added constraints would not C 1v -Horn in general.

Similarly to the case of clauses vs. literals, we can observe that, as far as clausal, Schaefer language are concerned, the complexity of abduction with manifestations expressed by CNFs is the same as that with manifestations expressed by terms. The case of affine knowledge bases is different, with problems harder for CNFs than for terms. Nevertheless, we do not elaborate on that point here, since most of the hardness for CNF manifestations simply comes from deciding whether the manifestation alone is satisfiable.

Affine knowledge bases

The case of equational instead of clausal languages is a bit more involved, but follows the same reasoning. We only sketch the idea, since equational languages are less interesting than CNF ones for knowledge representation purposes.

The main difference to the clausal case is that implications cannot be directly expressed. Indeed, if, for instance, h → m is a prime implicate of an affine knowledge base, then so must m → h be. In other words, in this case, the knowledge base entails h ↔ m. It follows that if the knowledge base entails both h 1 → m and h 2 → m, in fact it entails both h 1 ↔ m and h 2 ↔ m, and finally, any explanation for m must also satisfy h 1 and h 2 .

In general this makes the problem easier. The hard cases arise when implication can be simulated by imposing polarities on some hypotheses, just as is done, for instance, in the proof of Proposition 68. This also explains why the complexity for equational languages sometimes changes from V-Abd to L-Abd, contrary to clausal languages.

A note on NP-complete and coNP-complete cases

As can be seen from the results presented in the previous sections, it turns out that some restrictions on knowledge bases yield NP-complete problems, while others yield coNP-complete problems. This may seem strange at first sight, and deserves some explanation. In particular, we are not aware of any previous results in the literature where coNP-complete propositional abduction problems have been identified.

Recall that Σ P 2 is NP NP or, equivalently, NP NP∪coNP .

Essentially there are two sources of complexity in the general, Σ P -complete abduction problem: finding the right candidate explanation E (non-determinism, represented by the "basis" of the "exponential" NP NP∪coNP ), and checking that it is indeed a witness, i.e., that KB ∧ E is satisfiable and KB ∧ E |= M (represented by the "exponent").

That various restrictions on the hypotheses, manifestations, and knowledge bases in the abduction problem yield NP-complete problems is not very surprising. These NP-complete cases occur when both checking a candidate explanation is a polynomial problem, which is the case for Schaefer languages (Proposition 35), and the satisfiability problem for a set of clauses can be reduced to finding "the right candidate explanation", as illustrated by Lemma 61. The perhaps more surprising coNP-complete cases all occur when checking a candidate explanation is coNP-complete and only one candidate explanation needs to be considered, removing nondeterminism as a source of complexity and thus, in some sense, the "basis of the exponential". Observe that in this paper, when only one candidate explanation needs to be considered, this is always a result of KB ∧ H being trivially satisfiable as is, for example, the case for P-Abd(C 1v ,M).

Conclusion and future work

We have presented a thorough study of the complexity of deciding whether there is an explanation for a propositional abduction problem, under various restrictions over hypotheses and manifestations. We have derived the complexity for every possible local restriction on the knowledge bases for the problem, that is, for every Boolean constraint language and for every clausal or equational language, under the assumptions that the constraints in the knowledge base are given in extension or implicitly as CNFs or systems of equations, respectively. In particular this covers all the classical classes of CNF formulas defined by local properties and commonly considered for knowledge representation purposes. Moreover, we have shown that the problem, when not tractable, is complete for one of NP, coNP, or Σ P 2 .

In order to obtain these results, we have used now well-known techniques for obtaining tractability (e.g., prime implicate generation and projection). We have nevertheless uncovered new tractable cases. But we have also exhibited new conditions for intractability, some of which turn out to be very weak, as already observed in [START_REF] Nordh | Propositional abduction is almost always hard[END_REF].

Importantly, this study allows us to precisely explain what makes propositional abduction hard when the knowledge base is over a Schaefer language. Several points are very interesting, such as the need for variables which are neither hypothesized nor observed for making the task of explaining a literal hard, contrary to the case of a term. It also turns out that the conditions for intractability of abduction are so weak that almost no interesting class of problems can be tractable. In fact, only classes where there can be no explanation or there can be no conflicting hypotheses are tractable. This confirms the need for designing algorithms which are efficient in practice. Not surprisingly, our conditions for intractability confirm the results and observations by Bylander et al. in a different framework [START_REF] Bylander | The computational complexity of abduction[END_REF].

We have also argued that our explanation of the hardness of abduction gives hints for the complexity of problems which do not fit our framework. We demonstrated that argument for nonlocal (structural) propositional restrictions, but conjecture that it could also apply to completely different frameworks, such as abduction with nonclassical consequence relations or abduction in logic programming.

Propositional abduction turns out to be a very rich problem from a computational complexity perspective. By imposing various syntactic restrictions on the problem, no less than four complexity classes are covered. Thus our results can serve as a source of results allowing to derive the complexity of other problems. As a matter of fact, it is well-known that under various restrictions, several nonmonotonic reasoning problems reduce to each other. As an example, our classification for abduction with negative hypotheses and positive terms as manifestations gives the complexity of circumscriptive inference of negative clauses, as far as clausal languages restrict the knowledge base. Indeed, it is known (see [START_REF] Nordh | Propositional abduction is almost always hard[END_REF]Proposition 11]) that a negative clause follows from a knowledge base by circumscription if and only if its negation cannot be explained with all negative variables as hypotheses (except those in the clause). Thus, the complement of circumscriptive inference of negative clauses is at most as hard as abduction of positive terms with negative hypotheses. Now, as we discuss in Section 15.1, our classification for Schaefer clausal languages is preserved by the assumption that all variables except those in the manifestation are abducible. Thus, provided that KB is in CNF and subject to a restriction over each of its clauses, we get that deciding whether a negative clause follows from a knowledge base KB under circumscription of all variables is

• polynomial-time solvable if KB is restricted to be Horn or 0-valid,

• otherwise, coNP-complete if KB is restricted to be in 2CNF or dual Horn,

• otherwise, Π P 2 -complete.

We believe that our results may be used to derive other results in a similar fashion.

We now wish to note that in the paper, we have only studied the decision problem associated to abduction, leaving the search problem out. That is, we have not considered the complexity of computing an explanation instead of only deciding whether there is at least one. However, obviously the search problem is hard as soon as the decision one is, and as is easily seen from our results, all of which are constructive, the converse is also true. Importantly, this is still true when searching for ⊂-minimal explanations, because tractability of abduction entails tractability of satisfiability (considering an unsatisfiable manifestation) and deduction (considering an empty set of hypotheses), and this in turn is enough for minimizing an explanation with a greedy algorithm.

To conclude, it would be very interesting to extend this work into several directions. First of all, other problems related to abduction are of importance: for instance, deciding whether a hypothesis is relevant (part of at least one preferred explanation) or necessary (part of all of them) [START_REF] Eiter | The complexity of logic-based abduction[END_REF]; enumerating all explanations [START_REF] Eiter | On computing all abductive explanations from a propositional Horn theory[END_REF]; counting the number of (preferred) explanations [START_REF] Hermann | Counting complexity of propositional abduction[END_REF]. Our work provides results which can serve as a basis for studying the complexity of these problems, in particular for deriving hard cases. Moreover, as we have done, it would be interesting to understand what exactly makes these problems easy or hard.

Another important direction is to go further than the propositional setting and Schaefer's framework. As mentioned above, we believe that our observations about the reasons for (in)tractability can explain results beyond our framework. In particular, it would be interesting to study the complexity of abduction with nonlocal restrictions over knowledge bases (like, e.g., Eshghi [START_REF] Eshghi | A tractable class of abduction problems[END_REF] and del Val [START_REF] Del Val | The complexity of restricted consequence finding and abduction[END_REF] do) and with higher-cardinality domains.

  over three variables) satisfied by exactly 010, 011, 100. The unary relations F = {0} and T = {1} have a special role for abduction problems, as well as the binary relations R = = {00, 11} and R = = {01, 10}. Relations and formulas are linked to each other by the following definition. Definition 3 (representation) An n-ary relation R is said to be represented by a formula ϕ if Vars(ϕ) = {x 1 , . . . , x n } and ϕ ≡ R(x 1 , . . . , x n ).

Fig. 1 .

 1 Fig. 1. Post's lattice of Boolean relational clones in the form of a Hasse diagram.

Fig. 2 .

 2 Fig.2. Results for P-Abd(Γ,Terms), white is in P, light grey is NP-complete, mid grey is coNP-complete, dark grey is Σ P 2 -complete.

Theorem 33 (

 33 upper bounds for Deduction) Let C be a class of clauses or equations. Then Deduction(C,CNFs) is in coNP. Moreover, Deduction(C,CNFs) is in P when C is one of C Horn , C dHorn , C bij , and E aff .Theorem 34 (lower bound for Deduction) Let Γ be a constraint language with Γ = II 1 . Then Deduction(Γ,PosLits) is coNP-hard.

  PosTerms) and N-Abd(Γ,PosTerms) are NPhard.

  j ∈ H. ✷ Proposition 70 Let Γ be a constraint language satisfying Γ = IL 3 . Then P-Abd(Γ,PosTerms) and N-Abd(Γ,PosTerms) are NP-hard. PROOF. Since IL ⊂ IL 3 , by Proposition 68 L-Abd(Γ,PosTerms) NPhard. Now we know L-Abd(Γ,PosTerms)≤ P L-Abd(Γ,Terms) (Lemma 19). Finally, since R = (x, y) is the set of models of x ⊕ y = 1, R = is in IL 3 . Thus by Lemma 27 we know that L-Abd(Γ,Terms) ≤ P P-Abd(Γ,PosTerms), N-Abd(Γ,PosTerms), which concludes the proof. ✷ Proposition 71 Let Γ be a constraint language satisfying Γ = ID. Then V-Abd(Γ,PosCNFs), P-Abd(Γ,PosCNFs), and N-Abd(Γ,PosCNFs) are NP-hard.

  Proposition 8 Γ ∪ {F} is the least upper bound (in Post's lattice) of Γ and IR 0 . Γ ∪ {T} is the least upper bound of Γ and IR 1 . ≤ P Π ′ . If Π ≤ P Π ′ and Π ′ ≤ P Π, then we write Π ≡ P Π ′ . We write Π ≤ P Π 1 , Π 2 if Π ≤ P Π 1 and Π ≤ P Π 2 , and dually for Π 1 , Π 2 ≤ P Π.

	2.4 Complexity notions
	We assume that the reader is familiar with the basic notions of complexity
	theory, but we briefly recall the following. P is the class of decision problems
	solvable in deterministic polynomial time. NP is the class of decision problems
	solvable in nondeterministic polynomial time. Σ P 2 = NP NP is the class of de-
	cision problems solvable in nondeterministic polynomial time with access to
	an NP-oracle. A problem is NP-hard (Σ P 2 -hard) if every problem in NP (Σ P 2 ) is polynomial-time reducible to it. A problem is NP-complete (Σ P 2 -complete) if it is in NP and NP-hard (resp. in Σ P 2 and Σ P 2 -hard). Throughout the paper we assume that P, NP, and Σ P 2 are pairwise distinct.
	coNP is the dual complexity class of NP. That is, a problem is in coNP (resp.
	coNP-complete) if its complement is in NP (resp. NP-complete).
	If a problem Π can be reduced to a problem Π ′ under polynomial-time many-
	one reductions, then we write Π

•

  Lits denotes the class of all literals. • Similarly, PosClauses, NegClauses and Clauses denote classes of clauses, • PosTerms, NegTerms and Terms denote classes of terms, and • PosCNFs, NegCNFs and CNFs denote classes of CNFs.

Table 2 Minimal

 2

	R. Clone/class	Complexity Result
	C CNF (BR)	in Σ P 2	Proposition 41
	II 0	Σ P 2 -hard	Proposition 46
	IN 2	Σ P 2 -hard	Proposition 47
	C 1v (II 1 )	in coNP	Proposition 44
	IN	coNP-hard Proposition 48
	C Horn (IE 2 ), E aff (IL 2 ), C bij (ID 2 ) in NP	Proposition 35
	IS 2 1	NP-hard	Proposition 62 (dual)
	IL 0	NP-hard	Proposition 69
	IL 3	NP-hard	Proposition 70
	C 1v -Horn (IE 1 ), E 1v -aff (IL 1 )	in P	Proposition 44
	C dHorn (IV 2 )	in P	Proposition 52
	E aff /2 (ID 1 )	in P	Theorem 17

set of results for P-Abd(Γ,Terms)

  101, 000}. As for languages, we have, e.g., C d Horn = C dHorn , E d aff /2 = E aff /2 and (IS k 00 ) d = IS k 10 .

  [START_REF] Pschel | Funktionen-und Relationenalgebren[END_REF] Let P = (V, H, M, KB ) be an instance of any abduction problem. If KB ∧ H is satisfiable, then P has an explanation if and only if KB ∧ H |= M .

PROOF. Obviously, if KB ∧ H is satisfiable and KB ∧ H |= M , then E = H is an explanation. Conversely, assume KB ∧ H |= M . Then there is a model µ of KB ∧ H such that µ |= M ; then, for any E ⊆ H, µ |= KB ∧ E and µ |= M , hence KB ∧ E |= M and hence, E is not an explanation. ✷ As a direct consequence of Lemma 43, Theorems 32 and 33, we have the following results. The algorithm simply consists of deciding whether KB ∧ H entails M . Proposition 44 (1-valid) P-Abd(C 1v ,CNFs) is in coNP, and P-Abd(C 1v -Horn ,CNFs), P-Abd(E 1v -aff ,CNFs) are in P.

  Thus the set E C of all such ℓ's can be computed in polynomial time by testing the |H| candidates. Now consider the case when M is a CNF of the form (C 1 ∧ • • • ∧ C p ). Then by Lemma 28 and the reasoning above, a set E ⊆ H is an explanation for P if and only if KB ∧ E is satisfiable and for all i ∈ {1, . . . , p}, ∅ is an explanation for C i or there is someh i ∈ E such that h i ∈ E C i .As is easily seen, this is true if and only if the formula KB ∧ p i=1,KB |=C i ( h∈E C i h) is satisfiable. Since for all i ∈ {1, . . . , p}, E C i contains only positive literals, this formula is IHSB+ and thus, it can be decided in polynomial time whether it is satisfiable (Theorem 32, since C IHSB+ ⊆ C dHorn ). ✷ Proposition 60 L-Abd(C neg,= ,PosCNFs) is in P.

  II 1 Cpos,=, C IHSB-, C bij , E aff , C 1v -Horn C dHorn , C Horn C CNF Cneg,=, C 1v -Horn C bij , C dHorn , E aff , C Horn C CNF

		PosLits or C IHSB+/k , PosClauses	IS 01 , IV , IE 0	IN
		Lits or	C IHSB+/k , Cpos,=, C IHSB-/k , Cneg,=, C bij , E aff	C dHorn , C Horn	C CNF
		Clauses		IS 01 , IS 11 , IV , IE	IN
	L-Abd	PosTerms	C impl , Cneg,=, E aff /2 , C 1v -Horn	C bij , C dHorn , E aff , C Horn IS 2 0 , IS 2 11 , IV , IL	C CNF IN
		Terms	E aff /2	C bij , C dHorn , E aff , C Horn IM , IS 2 0 , IS 2 1 , IL	C CNF IN
		PosCNFs	C impl , IS 2 0 , IS 2 11 , ID, IV , IL	IN
		CNFs		C bij , C dHorn , E aff , C Horn	C CNF
				IBF	IN

Table 3

 3 Complexity of propositional abduction• L-Abd(Γ,M), where Γ ∈ {IS 01 , IS 00 , IS 11 , IS 10 }, M ∈ {Lits, Clauses}, • N-Abd(Γ,M), where Γ ∈ {IS 01 , IS 00 }, M ∈ {(Pos)Lits, (Pos)Clauses}, • P-Abd(Γ,M), where Γ ∈ {IS 11 , IS 10 }, M ∈ {Lits, Clauses}, • V-Abd(Γ,M), where Γ ∈ {IS 01 , IS 00 }, M ∈ {(Pos)Lits, (Pos)Clauses}, and • V-Abd(Γ,M), where Γ ∈ {IS 01 , IS 00 , IS 11 , IS 10 }, M ∈ {Lits, Clauses}.

  Bylander et al. study the complexity of abduction under various further assumptions about e. Of direct relevance to our study are the following restrictions. The problem is said to be• independent if ∀E ⊆ H, e(E) = h∈E e({h}), • monotonic if ∀E, E ′ ⊆ H, E ⊆ E ′ ⇒ e(E) ⊆ e(E ′ ),and • an incompatibility problem if there is a set I of pairs of elements of H (incompatible hypotheses) such that ∀E ⊆ H, (∃{h, h ′

  Then propositional abduction is NP-hard for C if and only if it is so with stronger restrictions or there is a polarity restriction on submanifestations such that C can express • implication from hypotheses to individual submanifestations, that is, ℓ H → ℓ S for any valid hypothesis ℓ H and valid submanifestation ℓ S , • implication from arbitrary conjunctions of submanifestations to individual manifestations, that is, (ℓ S,1 ∧ • • • ∧ ℓ S,k → ℓ M ) for any k ∈ N and any k valid submanifestations ℓ S,1 , . . . , ℓ S,k , • forbidden combinations of hypotheses, that is, ℓ H,1 ∨ ℓ H,2 for any two valid hypotheses ℓ H,1 , ℓ H,2 .

For instance, N-Abd(C,PosLits) is NP-hard when, among other cases, C can express implication from hypotheses to individual (negative) submanifestations (¬x 1 → ¬x 2 ), implication from arbitrary conjunctions of submanifestations to manifestations ((¬x 1 ∧ • • • ∧ ¬x n → x n+1 ), for any n), and forbidden conjunctions of hypotheses (x 1 ∨ x 2 ).

Note that even if the problem at hand is NP-hard, or even Σ P 2 -hard, most instances may be solved efficiently in practice. This may be done, for instance, using stateof-the-art solvers for Quantified Boolean formulas, which is the approach in[START_REF] Egly | Solving advanced reasoning tasks using quantified boolean formulas[END_REF].

As observed in[START_REF] Bylander | The computational complexity of abduction[END_REF], considering incompatible pairs, triples, etc. instead of only pairs does not affect the complexity results.

 [START_REF] Aspvall | A linear-time algorithm for testing the truth of certain quantified Boolean formulas[END_REF]Partially supported by the Swedish-French Foundation and the National Graduate School in Computer Science (CUGS), Sweden

PROOF. It follows from Post's lattice and Proposition 8 that II 1 ∪ {F} = BR. Thus from Theorem 32 it follows that Sat(II 1 ∪ {F}) is NP-complete. Let KB II 1 ∪{F} = KB II 1 ∧ i∈I F(x i ) be a knowledge base over II 1 ∪ {F}, where KB II 1 is a knowledge base over II 1 and I is nonempty (clearly, the problem remains NP-complete even with this assumption). Now let i 0 ∈ I, and let KB be the knowledge base obtained from KB II 1 by replacing every occurrence of x i for some i ∈ I \ {i 0 } with x i 0 . By construction, KB is a knowledge base over II 1 , and KB ∧ F(x i 0 ) is satisfiable if and only if KB II 1 ∪{F} is. But KB ∧ F(x i 0 ) is unsatisfiable if and only if KB entails x i 0 , which concludes the proof. ✷ Schaefer languages are precisely those maximal languages (for inclusion) for which deduction of clauses is tractable, i.e., C Horn , C dHorn , C bij and E aff . From the results above we immediately get the following result.

Proposition 35

For any type of restriction on hypotheses and manifestations considered in this paper and for all Schaefer languages C, Abd(C) is in NP.

Prime implicates

The notion of a prime implicate is widely used for studying various computational problems in propositional logic, especially for problems in nonmonotonic reasoning. The relevance of this notion to abduction has been first pointed out by Reiter and de Kleer [START_REF] Reiter | Foundations of assumption-based truth maintenance systems: preliminary report[END_REF]. Marquis [START_REF] Marquis | Consequence finding algorithms[END_REF] gives a survey of the various notions of prime implicates, their use for nonmonotonic reasoning (including abduction), and methods for computing them.

Definition 36 (prime implicate) Let KB be a propositional formula or a conjunction of constraints. A clause C is said to be a prime implicate of KB if KB entails C but no proper subclause of it.

The following characterization of explanations, first shown by Reiter and de Kleer in the ATMS setting [START_REF] Reiter | Foundations of assumption-based truth maintenance systems: preliminary report[END_REF], will be of great use to us.

Lemma 37 ([45]

) Let P = (V, H, M, KB ) be an instance of an abduction problem, where

Then E is an explanation for P if and only if there is a prime implicate of KB of the form

, . . . , j s } ⊆ {1, . . . , p} and {j 1 , . . . , j s } = ∅ (with possibly ℓ i = m j for some i, j).

Finally, recall from Quine's result [START_REF] Quine | On cores and prime implicants of truth functions[END_REF] that all the prime implicates of a CNF KB can be generated by resolution, i.e., by repeatedly adding C 1 ∨ C 2 to KB PROOF. Let Γ be a constraint language such that Γ = II 0 . By Post's lattice and Proposition 8, Γ ∪ {T} = BR and thus, by Proposition 42 P-Abd(Γ ∪ {T},PosLits) is Σ P 2 -complete. We give a reduction of this latter problem to P-Abd(Γ,PosLits).

To this aim, let P ′ = (V ′ , H ′ , m ′ , KB ′ ) be an instance of P-Abd(Γ∪{T},Pos-Lits). Write KB ′ = KB Γ ∧ x∈V T T(x), where KB Γ is a conjunction of constraints over Γ and V T is a set of variables. We assume V T = ∅ without loss of generality. Then we define KB to be any conjunction of constraints (possibly with existentially quantified auxiliary variables) over Γ and logically equivalent to KB Γ ∧ x∈V T (¬m ′ ∨ x); such a formula exists because Γ = II 0 is the set of all 0-valid relations and (¬m ′ ∨x) is 0-valid. We also define H = H ′ ∪V T , and P = (V ′ , H, m ′ , KB ). Then, clearly P has an explanation if and only if P ′ has one, since KB is logically equivalent to KB Γ ∧ (m ′ → x∈V T T(x)) (the reasoning is similar to that in [START_REF] Creignou | A complete classification of the complexity of propositional abduction[END_REF]Lemma 19]). ✷

Complementive languages

We give two new lower bounds.

Proposition 47 Let Γ be a constraint language satisfying Γ = IN 2 . Then P-Abd(Γ,PosLits) and N-Abd(Γ,PosLits) are Σ P 2 -hard.

PROOF. We know from Theorem 18 that V-Abd(Γ,PosLits) is Σ P 2 -complete. Now V-Abd(Γ,PosLits) ≤ P L-Abd(Γ,Lits) (Lemmata 19 and 20), and since R = ∈ IN 2 , we have L-Abd(Γ,Lits) ≤ P P-Abd(Γ,PosLits), N-Abd(Γ,PosLits) (Lemma 27), which concludes the proof. ✷ Proposition 48 Let Γ be a constraint language satisfying Γ = IN . Then P-Abd(Γ,PosLits) is coNP-hard.

PROOF. We know from Post's lattice and Proposition 8 that Γ ∪ {T} = II 1 . Thus it follows from Theorem 34 that Deduction(Γ ∪ {T},PosLits) is coNP-hard. We give a reduction of this latter problem to P-Abd(Γ,PosLits).

Let (V, KB T , q) be an instance of Deduction(Γ ∪ {T},PosLits), where q ∈ V , and write KB T = KB ∧ x∈V T T(x), where KB is a knowledge base over Γ. Now define an instance P of P-Abd(Γ,PosLits) by P = (V, H = V T , q, KB ). Since KB is 1-valid we have that KB ∧ H is satisfiable, and thus, by Lemma 43, P has an explanation if and only if KB ∧ H entails q, i.e., if and only if KB T entails q. ✷ (V, H, M 1 , KB ). Similarly, in the second entailment relation both KB and E 1 are irrelevant, thus E 2 |= M 2 holds. ✷

We now turn to CNF manifestations. The following lemma shows that for almost all languages, we can assume Vars(M ) ⊆ Vars(KB ) or not without affecting the complexity of abduction.

Proposition 78 Let Γ be any constraint language with Γ ⊆ IR 2 or R = ∈ Γ. Then one can assume up to polynomial-time reductions that an instance (V, H, M, KB ) of Abd(Γ) satisfies Vars(M ) ⊆ Vars(KB ).

PROOF. If Γ ⊆ IR 2 or R = ∈ Γ, then Γ contains at least one relation R which is nonempty, n-ary and not equivalent to any term of length n. Then there is at least one place i ∈ {1, . . . , n} and two tuples (µ 1 , . . . , µ i-1 , 0, µ i+1 , . . . , µ n ),

Then the assumption Vars(M ) ⊆ Vars(KB ) can be enforced as follows. For each variable x in Vars(M )\Vars(KB ) add n-1 fresh variables new x,1 , . . . , new x,n-1 to V and add the constraint R(new x,1 , . . . , new x,i-1 , x, new x,i , . . . to KB . Write KB ′ and V ′ for the resulting KB and V . By construction x is unconstrained by KB ′ , and thus (V ′ , H, M, KB ′ ) has an explanation if and only if (V, H, M, KB ) has one. ✷

The only special case is the following, for the class of CNF formulas containing only unit clauses (and no equality relations), when Vars(M ) ⊆ Vars(KB ).

Proposition 79 L-Abd(C unit,= \{R = },CNFs) is in P if instances (V, H, M, KB ) are required to satisfy Vars(M ) ⊆ Vars(KB ). This holds even if nothing is known about the satisfiability of M .

PROOF. Obvious since with the assumptions, KB is logically equivalent to a term which defines a complete assignment to Vars(M ). Thus we only have to decide whether this assignment satisfies M . ✷

Discussion

We now explain in an intuitive manner what makes propositional abduction hard. We focus on Schaefer languages (Horn, dual Horn, bijunctive and affine), i.e., those languages for which deduction of CNFs is tractable, since they are the most interesting ones for reasoning and knowledge representation. Recall from Proposition 35 that abduction is in NP for all such languages. Thus we