Backdoors to Abduction

1 Introduction

Abductive reasoning (or Abduction, for short) is among the most fundamental reasoning methods. It is used to explain observations by finding appropriate causes. In contrast to deductive reasoning, it is therefore a method for "reverse inference". Abduction has a broad range of applications in AI, including system and medical diagnosis, planning, configuration, and database updates.

Unfortunately, Abduction is of high computational complexity. Already propositional Abduction, the focus of this paper, is ΣP2 -complete and thus located at the second level of the Polynomial Hierarchy [Eiter and Gottlob, 1995]. Consequently, Abduction is harder than NP and co-NP. This complexity barrier rules out the existence of a polynomialtime transformation to the propositional satisfiability problem (SAT). As a consequence, one cannot directly apply powerful SAT solvers to Abduction. However, this would be very desirable in view of the enormous power of state-of-theart SAT solvers that can handle instances with millions of clauses and variables [Gomes et al., 2008; Katebi et al., 2011; J¨arvisalo et al., 2012].

∗Supported by the Austrian Science Fund (FWF): P25518-N23.

†Supported by the European Research Council (ERC), project 239962.

Main contribution. We present a new approach to utilize problem structure in order to break this complexity barrier for Abduction. More precisely, we present transformations from Abduction to SAT that run in quadratic time, with a constant factor that is exponential in the distance of the given propositional theory from being HORN or KROM. We measure the distance in terms of the size of a smallest strong backdoor set into the classes HORN or KROM, respectively [Williams et al., 2003]. Thus the exponential blow-up-which is to be expected when transforming a problem from the second level of the Polynomial Hierarchy into SAT-is confined to the size of the backdoor set, whereas the order of the polynomial running time remains constant independent of the distance. Such transformations are known as fixedparameter tractable reductions and are fundamental to Parameterized Complexity Theory [Downey and Fellows, 1999; Flum and Grohe, 2006].

Our new approach to Abduction has several interesting aspects. It provides flexibility and openness. Any additional constraints that one might want to impose on the solution to the Abduction problem can simply be added as additional clauses to the SAT encoding. Hence such constraints can be handled without the need for modifying the basic transformation. The reduction approach readily supports the enumeration of subset-minimal solutions, as we can delegate the enumeration to the employed SAT solver. Any progress made for SAT solvers directly translates into progress for Abduction.

As a by-product, our approach gives rise to several new fixed-parameter tractability results. For instance, Abduction is fixed-parameter tractable when parameterized by the number of hypotheses and the size of a smallest HORN- or KROMbackdoor set. Parameterized by the size of backdoor sets alone, Abduction is para-NP-complete.

Related Work. Methods from parameterized complexity have turned out to be well-suited to tackle hard problems in Knowledge Representation & Reasoning [Gottlob and Szeider, 2008]. In particular, the concept of backdoor sets provides a natural way of parameterizing such problems [Samer and Szeider, 2009; Fichte and Szeider, 2011; Gaspers and Szeider, 2012a; 2012b; Lackner and Pfandler, 2012a; 2012b; Dvor´ak et al., 2012]. The parameterized complexity of Abduction was subject of previous work, where different parameters have been considered [Gottlob et al., 2010; Fellows et al., 2012]. The most significant difference to our work is that we use fixed-parameter tractability not to solve the Abduction problem itself, but to reduce it from the second level of the Polynomial Hierarchy to the first. This way, our parameters can be less restrictive and are potentially small for larger classes of Abduction instances. This novel use of fixedparameter tractability was recently applied in the domain of answer-set programming [Fichte and Szeider, 2013], and we believe it can be applied to other hard reasoning problems as well. Abduction can be transformed in polynomial time to QBF [Egly et al., 2000], but then one remains on the second level of the Polynomial Hierarchy.

2 Preliminaries

Propositional Logic. A formula in conjunctive normal form is a conjunction of disjunctions of literals; we denote the class of all such formulas by CNF. It is convenient to view a formula in CNF also as a set of clauses and a clause as a set of literals. KROM denotes the class of all CNF formulas having clause size at most 2. HORN formulas are CNF formulas with at most one positive literal per clause. Let var (ϕ) be the set of variables occurring in ϕ ∈ CNF.

A (partial) truth assignment is a mapping τ : X → {0, 1} defined for a set X of variables. We write var (τ ) to denote the domain X. To extend τ to literals we put τ(¬x) = 1 - τ(x) for x ∈ X. By ta(X) we denote the set of all truth assignments τ : X → {0, 1}. Let S be a set of variables. We denote by ta(X, S) the set {τ ∈ ta(X) | ∀s ∈ S∩X : τ(s) = 1}. We say that τ satisfies literal l if τ(l) = 1. A clause is tautological if it contains a variable x and its negation ¬x. A truth assignment τ satisfies a CNF formula if in each non-tautological clause, there exist a literal that is satisfied by τ. A CNF formula ϕ is satisfiable (or consistent) if there exists some truth assignment τ that satisfies ϕ. If, additionally, var (τ) contains all variables of ϕ, we call it a model of ϕ. The truth assignment reduct of a CNF formula ϕ under a truth assignment τ is the CNF formula ϕ[τ ] obtained from ϕ by deleting all clauses that are satisfied by τ and by deleting from the remaining clauses all literals that are set to 0 by τ . Let ϕ, ψ ∈ CNF, then ϕ entails ψ (denoted by ϕ ⊨ ψ) if every model τ of ϕ with var (ψ) ⊆ var (τ) is also a model of ψ.

Let Res(ϕ) denote the set of clauses computed from ϕ ∈ CNF by iteratively applying resolution and dropping tautological clauses until a fixed-point is reached. Applying resolution adds the clause C∪D to ϕ if C∪{x} ∈ ϕ and D∪{¬x} ∈ ϕ. Let C be a non-tautological clause then C ∈ Res(ϕ) if and only if ϕ ⊨ {C}. For more information, cf. [Leitsch, 1997].

Let X be a set of variables, we define X := {¬x | x ∈ X}. For convenience, we view a set of variables X as the conjunction of its elements, whenever it is used as a formula.

Propositional Abduction. A (propositional) abduction instance consists of a tuple 〈V,H,M, T〉, where V is the set of variables, H ⊆ V is the set of hypotheses, M ⊆ V is the set of manifestations, and T is the theory, a formula in CNF over V . It is required that M ∩ H = ∅. We define the size of an abduction instance P to be the size of a reasonable encoding of P. For instance taking |V | + |H| + |M| + ∑C∈T |C| would do. A set S ⊆ H is a solution to (or explanation of) P if T ∪ S is consistent and T ∪ S |= M (entailment). Sol (P)

denotes the set of all solutions to P. The solvability problem for propositional abduction ABD is the following problem:

ABD Instance: An abduction instance P. Problem: Decide whether Sol(P) ̸= ∅.

We will additionally consider a version of the abduction problem where we search for certain solutions only. A solution S is subset-minimal if there is no solution S′ ⊊ S.

ABD⊆

Instance: An abduction instance P and a hypothesis h. Problem: Is there a subset-minimal solution S ⊆ H to P with h ∈ S.

Recall that ABD is ΣP2 -complete in general while it becomes NP-complete when the theory is a HORN or KROM formula. The same holds for ABD⊆ [Eiter and Gottlob, 1995; Nordh and Zanuttini, 2008; Selman and Levesque, 1990].

Example. In this example we look for explanations why the nicely planned skiing trip ended up so badly. The abduction instance is given as follows:

V = {snows, rains, precipitation, warm, hurt, sad} H = {precipitation, warm, hurt} M = {sad} T = { precipitation → rains ∨ snows, hurt → sad, warm → ¬snows, rains → sad}

One can easily verify that S1 = {hurt} and S2 = {precipitation, warm} are solutions to this abduction instance. Notice that S1 and S2 are the only subset-minimal solutions while, e.g., S3 = {hurt, warm} is a solution as well.

Parameterized Complexity. We give some basic background on parameterized complexity. For more detailed information we refer to other sources [Downey and Fellows, 1999; Flum and Grohe, 2006]. A parameterized problem L is a subset of Σ∗ × N for some finite alphabet Σ. For an instance (I, k) ∈ Σ∗ × N we call I the main part and k the parameter. L is fixed-parameter tractable if there exists a computable function f and a constant c such that there exists an algorithm that decides whether (I, k) ∈ L in time O(f(k)‖I‖c ) where ‖I‖ denotes the size of I. Such an algorithm is called an fptalgorithm. We will use the O∗ (·) notation which is defined in the same way as O(·), but ignores polynomial factors.

Let L ⊆ Σ∗ × N and L′ ⊆ Σ′∗ × N be two parameterized problems for some finite alphabets Σ and Σ′ . An fpt-reduction r from L to L′ is a many-to-one reduction from Σ∗ × N to Σ′∗ ×N such that for all I ∈ Σ∗ we have (I, k) ∈ L if and only if r(I, k) = (I ′ , k′ ) ∈ L′ . Thereby, k′ ≤ g(k) for a fixed computable function g : N → N, and there is a computable function f and a constant c such that r is computable in time O(f(k)‖I‖c ) where ‖I‖ denotes the size of I [Flum and Grohe, 2006]. Thus, an fpt-reduction is, in particular, an fpt-algorithm. We would like to note that the theory of fixedparameter intractability is based on fpt-reductions.

Backdoors. Williams et al. [2003] introduced the notion of backdoors to explain favorable running times and the heavytailed behavior of SAT and CSP solvers on practical instances.

Backdoors are defined with respect to a fixed class C of CNF formulas, the base class (or more figuratively, island of tractability). A strong C-backdoor set of a formula ϕ ∈ CNF is a set B of variables such that ϕ[τ ] ∈ C for each τ ∈ ta(B). B is also called a strong C-backdoor set of an abduction instance P = 〈V,H,M, T〉 if B is a strong C-backdoor set of T. Observe that the instance from the example above has a strong HORN-backdoor set and a strong KROM-backdoor set of cardinality one (consider, e.g., B = {snows}).

Backdoor Approach. The backdoor approach consists of two phases. First, a backdoor set is computed (detection) and afterwards the backdoor is used to solve the problem (evaluation). For example, for SAT this approach works as follows. If we know a strong C-backdoor set of a CNF formula ϕ of size k, we can reduce the satisfiability of ϕ to the satisfiability of 2k easy formulas that belong to the base class. The challenging problem, however, is to find a strong backdoor set of size at most k, if it exists. This problem is NP-hard for all reasonable base classes, but fortunately, fixed-parameter tractable for the base classes KROM and HORN if parameterized by k [Nishimura et al., 2004]. In particular, efficient fixed-parameter algorithms for the 3-HITTING SET problem and for the VERTEX COVER problem can be used for detecting strong backdoor sets for the base classes KROM and HORN. Fastest known fixed-parameter algorithms for these two problems run in time O∗ (2.270k ) and O∗ (1.2738k ) [Niedermeier and Rossmanith, 2003; Chen et al., 2010], respectively. For further information on the parameterized complexity of backdoor set detection we refer to a recent survey [Gaspers and Szeider, 2012b].

For Abduction the detection phase is the same as for SAT, but the evaluation phase becomes the new challenge. We therefore focus on the evaluation phase, and assume that the backdoor set is provided as part of the input. However, whether or not we provide the backdoor set as part of the input does not affect the parameterized complexity of the overall problem, since, as explained above, the detection of strong HORN/KROM-backdoors is fixed-parameter tractable.

3 Transformations using Horn Backdoors

In this section we present the transformation from ABD to SAT using strong HORN-backdoor sets. In our transformation we will build upon ideas from Dowling and Gallier [1984] for computing the unique minimal model (with respect to set-inclusion) of HORN formulas in linear time. Recall that manifestations in the considered Abduction formalism are assumed to be positive literals (i.e., variables). The following lemma captures the evaluation phase of our backdoor approach. The proof can be found in the full version [Pfandler et al., 2013].

Lemma 1. Let P = 〈V,H,M, T〉 be an abduction instance, let S ⊆ H, and let B ⊆ V . Then S is a solution to P if and only if (i) ∃τ ∈ ta(B, S) such that T[τ]∪S is consistent, and (ii) ∀τ ∈ ta(B, S), T [τ ] ∪ S ⊨ M[τ ].

Based on this lemma, Algorithm 1 checks whether a given candidate is indeed a solution.

Algorithm 1: Solution-Checker HORN-bds

Input : An abduction instance P = 〈V,H,M, T〉, a strong

HORN-backdoor set B of P and a solution candidate S ⊆ H to be checked. Output : Decision whether S is a solution to P. 1 consistent← false 2 entailment ← true 3 foreach τ ∈ ta(B, S) do 4 if ¬ consistent then 5 if T [τ ] ∪ S is consistent then 6 consistent ← true 7 if T [τ ] ∪ S is consistent then 8 U← the unique minimal model of T [τ ] ∪ S 9 if U ⊭ M[τ] then // Thus T[τ] ∪S ⊭ M[τ] 10 entailment ← false 11 break 12 return consistent ∧ entailment

Proof. (⇒) Assume there exists a solution S ∈ Sol(P). By Lemma 1 there exists a τ ∈ ta(B, S) such that T[τ] ∪ S is consistent. Therefore, for one of the assignments from Line 3, the flag consistent will be set to true in Line 6. Furthermore, by Lemma 1, for all τ ∈ ta(B, S) it holds that T[τ] ∪ S ⊨ M[τ]. Therefore, Line 10 will not be reached and the flag entailment will remain true. Hence, the algorithm returns yes.

(⇐) Assume that the algorithm returns yes. Therefore, Line 10 is never reached and U ⊨ M[τ] for all τ ∈ ta(B, S). Since M[τ] is entailed in the minimal model and contains only positive literals, it is entailed in every model and T [τ ] ∪ S ⊨ M[τ] for all τ ∈ ta(B, S). Furthermore, there exists a τ ∈ ta(B, S) such that Line 6 is reached and hence T [τ ] ∪ S is consistent. It follows from Lemma 1 that S ∈ Sol (P).

Corollary 3. Let P = 〈V,H,M, T〉 be an abduction instance and B a strong HORN-backdoor set of P. We can check whether P has a solution in time O∗ (2|B|+|H| ). Hence, ABD is fixed-parameter tractable when parameterized by |B|+|H|.

Proof. One has to check for each of the 2|H| -many solution candidates S ⊆ H, whether S is a solution to P. To this end we apply Algorithm 1, which runs in time O∗ (2|B| ).

If the number of hypotheses is large, this fpt-algorithm is not efficient. To overcome this limitation, we present next an fpt-reduction to SAT using only the backdoor size as the parameter. This is the main result of this section.

Theorem 4. Given an abduction instance P of input size n and a strong HORN-backdoor B of P of size k, we can create in time O(2k n2 ) a CNF formula FHORN-Solv of size O(2k n2 ) such that FHORN-Solv is satisfiable if and only if Sol(P) ̸= ∅.

Proof. Let P = 〈V,H,M, T〉. We will first construct a propositional formula F ′HORN-Solv which is not in CNF. The required CNF formula FHORN-Solv can then be obtained from F ′HORN-Solv by means of the well-known transformation due to Tseitin [1968], in which auxiliary variables are introduced.

This transformation produces for a given propositional formula F ′ in linear time a CNF formula F such that both formulas are equivalent with respect to their satisfiability, and the length of F is linear in the length of F ′ .

Note that in this encoding a solution S ⊆ H can be obtained by projecting a model of F ′HORN-Solv to the variables in H, i.e., h ∈ S if and only if h ∈ H is true in the model. We define

where F ent is a formula, defined below, that checks the entailment T ∪ S |= M. Let B1, . . . , B2k be an enumeration of all the subsets of B. Each subset implicitly denotes a truth assignment for B. For each variable v ∈ B and each subset Bi with 1 ≤ i ≤ 2k , we use a propositional constant Bi(v) that is true if and only if v ∈ Bi. Now we can define F ent :

where F ent i , defined below, checks entailment for the i-th truth assignment for B. By Lemma 1 we have to ensure entailment only for those truth assignments that match the truth value of all h ∈ S. This is done via the implication (∧h∈H∩B (h → Bi(h))) → F ent i . We define F ent i using three auxiliary formulas:

where F lm i creates the least model of the HORN theory, F check i checks whether this model satisfies all constraints of the theory, and F man i checks if the model satisfies all manifestations. Next we will define F lm i . The idea behind the construction is to simulate the linear-time algorithm of Dowling and Gallier [1984], where initially all variables are set to false and then a variable is flipped from false to true if and only if it is in the head of a rule where all the variables in the rule body are true (a fact is a rule with empty body). Once a fixed-point is reached, we have obtained the least model. We encode this idea as follows. Since we are interested in the least model of T ∪ S instead of just T, we initialize those variables that are contained in S by setting them to true. Let p := min{|T | , |V |} be the maximum number of steps after which the fixed-point is reached. For each i with 1 ≤ i ≤ 2k , we introduce a new set of variables Ui := {uji [v] | v ∈ V, 0 ≤ j ≤ p}. The intended meaning of a variable uji [v] is the truth value of the original variable v after the j-th step of the computation of the least model. The following auxiliary formulas encode this computation:

As mentioned above, we initially set the variables to false with the exception of the hypotheses. This is done in the formulas F (v,0) i . The computation steps are represented by the formulas F (v,j) i . Thereby we set a variable uji [v] to true if and only if it was already true in the previous step (uj-1 i [v]), or there is a rule r in T [Bi] such that Head(r) = v and all body variables b ∈ Body(r) were already true in the previous step (uj-1 i [b]). In order to check whether the least model satisfies all the constraints (purely negative clauses), we define:

Finally, we check whether the model satisfies all manifestations with the following formula:

It follows by Lemma 2 and by the construction of the auxiliary formulas that F ′HORN-Solv is satisfiable if and only if Sol(P) ̸= ∅. Hence it remains to observe that for each 1 ≤ i ≤ 2k the auxiliary formula F lm i can be constructed in quadratic time, and the auxiliary formulas F check i and F man i can be constructed in linear time. Therefore, formula F ent can be constructed in time O(2k n2 ) and has size O(2k n2 ).

4 Transformations using KromBackdoors

Recall that (in contrast to HORN formulas) a KROM formula might have several (subset) minimal models. Hence we cannot use the above approach for the base class KROM. However, we can exploit special properties of KROM formulas with respect to resolution. Analogously to Section 3 we start with an algorithm for verifying a solution and show fixedparameter tractability with respect to the combined parameter backdoor size and number of hypotheses. Subsequently we establish the main result of this section, an fpt-reduction with backdoor size as the single parameter.

Lemma 5. Let P = 〈V,H,M, T〉 be an abduction instance and B be a strong KROM-backdoor set of P. A set S ⊆ H is a solution to P if and only if Algorithm 2 returns yes.

Corollary 6. Let P = 〈V,H,M, T〉 be an abduction instance and B be a strong KROM-backdoor set of P. We can check whether P has a solution in time O∗ (2|B|+|H| ). Hence, ABD is fixed-parameter tractable when parameterized by |B| + |H|.

The transformation in the next theoremwill use resolution in a preprocessing step, where we compute for each assignment τ ∈ ta(B, S) the set containing all (non-tautological) resolvents restricted to variables in H ∪M. Computing these resolvents is possible in polynomial time for KROM formulas, since resolution on a KROM formula always yields a KROM formula. We employ the following definition and lemma.

Definition 7 (Fellows et al. [2012], Definition 17). Given an abduction instance for KROM theories 〈V,H,M, T〉. We define the function TrimRes(T,H,M) := {C ∈ Res(T) | C ⊆ X}, with X = H ∪ M ∪ {¬x | x ∈ (H ∪ M)}. In case TrimRes(T, H,M) contains the empty clause □, we set TrimRes(T,H,M) := {□}.

Algorithm 2: Solution-Checker KROM-bds

Input : An abduction instance P = 〈V,H,M, T〉, a strong KROM-backdoor set B of P and a solution candidate S ⊆ H to be checked.

1 consistent← false 2 entailment ← true 3 foreach τ ∈ ta(B, S) do 4 if ¬ consistent then 5 if T [τ ] ∪ S is consistent then 6 consistent ← true 7 if M[τ] is consistent then 8 foreach m ∈ M \ var (τ ) do 9 if (T [τ ] ⊭ m) ∧ (∀h ∈ S: T [τ ] ∧ h ⊭ m) then 10 entailment ← false 11 break 12 else 13 if T [τ ] ∪ S is consistent then 14 entailment ← false 15 break

16 return consistent ∧ entailment

Lemma 8 (Fellows et al. [2012], Lemma 20). Let 〈V,H,M, T〉 be an abduction instance for KROM theories, S ⊆ H, m ∈ M, and T ∧ S be satisfiable. Then T ∧ S |= m if and only if either {m} ∈ TrimRes(T,H,M) or there exists some h ∈ S with {¬h, m} ∈ TrimRes(T, H, M).

We extend this notion by using TrimRes(T,H,M, τ) := TrimRes(T [τ ], H \ var (τ ), M \ var (τ )).

Theorem 9. Given an abduction instance P of input size n and a strong KROM-backdoor B of P of size k, we can create in time O(2k n2 ) a CNF formula FKROM-Solv of size O(2k n2 ) such that FKROM-Solv is satisfiable if and only if Sol(P) ̸= ∅.

Proof. By the same argument as in Theorem 4, it suffices to create first a formula F ′KROM-Solv which is not in CNF. Formula F ′KROM-Solv is identical to formula F ′HORN-Solv except for the subformula F ent i , for which a completely new approach is needed.

Let P = 〈V, H, M, T 〉 and let B1, . . . , B2k be an enumeration of all the subsets of B. Each subset Bi implicitly defines a truth assignment τi of B. In a preprocessing step, for each assignment τi the function TrimRes(T,H,M, τi) is computed. In order, to connect the result of TrimRes(T,H,M, τi) with the encoding we use logical constants which are defined as follows: Let C be a clause over H ∪ M or the empty clause □. Then we define TRCi to be true if and only if C ∈ TrimRes(T, H, M, τi).

We obtain the formula F ′KROM-Solv from F ′HORN-Solv by replacing F ent i , see Equation (1), by:

For each assignment τi (represented by Bi(·)) we have to check whether the entailment T [τi]∪S ⊨ M[τi] holds. This is done in F ent i . The proof of the correctness of this construction can found in the full version [Pfandler et al., 2013]. Note that F ent i can be constructed in quadratic time. Thus FKROM-Solv can be constructed in time and space of O(2k n2 ).

5 Subset Minimality

In abductive reasoning one is often more interested in subsetminimal solutions than in "ordinary" solutions [Eiter and Gottlob, 1995]. Consider the example from the preliminaries. Clearly, S3 is a solution but actually the hypothesis warm is dispensable. In larger settings unnecessary hypotheses in the solution might blur the explanation. We demonstrate now how the previously presented transformations can be modified to produce only subset-minimal solutions and thus solve ABD⊆.

Theorem 10. Given an instance 〈P, h∗ 〉 for ABD⊆ of size n and a strong HORN- or KROM-backdoor set B of P of size k, we can create in time O(2k n2 ) a CNF formula of size O(2k n2 ) that is satisfiable if and only if 〈P, h∗ 〉 is a yesinstance for ABD⊆.

Proof. In order to construct a formula FHORN-⊊-Solv in case of a strong HORN-backdoor set, we modify F ′HORN-Solv from Theorem 4. The first change is that a solution S ⊆ H is no longer represented by the restriction of a model to the variables in H. Instead we introduce a new propositional variable sh for each h ∈ H with the intended meaning of sh being true if and only if h ∈ S. Let VS denote the set of these variables.

The new conjunction ∧h∈H (sh → h) ensures that the choice over the variables VS is propagated to the variables representing the hypotheses. Furthermore, we change F ent and F (v,0) i so that these formulas use the new variables VS:

The other subformulas from the proof of Theorem 4 remain unchanged. We can now write F ′HORN-⊊-Solv as follows.

where for each h ∈ H the formula F h non-ent enforces that for S \{h} the manifestations M are no longer entailed. Thereby we introduce for each h ∈ H a new copy vh of each variable v ∈ V . Let T h and M h denote T and M, respectively, where the variables are replaced by the new copies. It remains to observe that the formula F ′HORN-⊊-Solv can be constructed in time O(2k n2 ).

The construction of the formula FKROM-⊊-Solv in case of a strong KROM-backdoor set is analogous. We modify the formula F ′KROM-Solv from Theorem 9 similarly to the HORN case above. Again we use new variables sh to decouple the solution from the hypotheses. The important change is to replace the subformula F ′HORN-Solv by a decoupled version of F ′KROM-Solv . This decoupling is achieved by adding the clauses ∧h∈H (sh → h) and replacing each occurrence of h by sh, and h1, h2 by sh1 , sh2 accordingly.

6 Completeness for para-NP

A parameterized problem L is contained in the parameterized complexity class para-NP if L can be decided by a nondeterministic fpt-algorithm [Flum and Grohe, 2003].

For a non-parameterized problem that is NP-complete, it is considered a bad result if adding a parameter makes it paraNP-complete, since this indicates that the considered parameter does not help. But in the case of abduction, which is ΣP2 - complete, showing that it becomes para-NP-complete is indeed a positive result. In fact we get the following result as a corollary to Theorems 4, 9, and 10.

Corollary 11. For C ∈ {HORN, KROM}, the problems ABD and ABD⊆ are para-NP-complete when parameterized by the size of a smallest strong C-backdoor set of the given abduction instance.

7 Enumeration and Further Extensions

In this section we sketch how the transformations presented above can be used to enumerate all (subset-minimal) solutions.

Obtaining a solution to the abduction instance from the models returned by the SAT solver is straightforward. For the formulas FHORN-⊊-Solv and FKROM-⊊-Solv (Theorem 10) it suffices to restrict the models to the variables sh, for all h ∈ H. In order to enumerate all possible solutions, one can exclude already found solutions by adding appropriate clauses that eliminate exactly these models.

The formulas FHORN-Solv and FKROM-Solv (Theorems 4 and 9) need to be slightly modified, since a solution S ⊆ H is not expressed explicitly. This is for example a problem, if an hypothesis h1 implies another hypothesis h2, because no solution candidate containing only h1 but not h2 will be considered. This problem does not occur in the formulas F ′HORN-⊊-Solv and F ′KROM-⊊-Solv , since there the encoding of a solution is decoupled from the hypotheses via ∧h∈H (sh → h). The same technique can be used in the encoding of F ′HORN-Solv and F ′KROM-Solv . Note, that several occurrences of hypotheses h have to be changed to sh.

The transformations from Sections 3 and 4 can be extended easily to the corresponding relevance problem, i.e., asking whether there exists some S ∈ Sol(P) containing a certain h∗ ∈ H. It suffices to check only those S ⊆ H where h∗ ∈ S.

Corollary 12. Let C ∈ {HORN, KROM}. Given an abduction instance P = 〈V,H,M, T〉, an atom h∗ ∈ H, and a strong C-backdoor set of P, we can decide whether h∗ belongs to some solution to P in time O∗ (2|B|+|H| ). Thus, the relevance problem is fixed-parameter tractable when parameterized by |B| + |H|. This also holds for ABD⊆.

Furthermore, the SAT encoding allows us to easily restrict solutions for ABD or ABD⊆ in terms of any constraints that are expressible in CNF. For example, using the encoding of a counter [Sinz, 2005], we can restrict the cardinalities of solutions and therefore solve the variants of ABD as proposed by Fellows et al. [2012]. In contrast, adding these constraints directly to the theory of the Abduction instance can increase the size of the backdoor set.

8 Conclusion

We have presented fixed-parameter tractable transformations from various kinds of abduction-based reasoning problems to SAT that utilize small HORN/KROM-backdoor sets in the input. These transformations are complexity barrier breaking reductions as they reduce problems from the second level of the Polynomial Hierarchy to the first level. A key feature of our transformations is that the exponential blowup of the target SAT instance can be confined in terms of the size of a smallest backdoor set of the input theory, a number that measures the distance to the "nice" classes of HORN and KROM formulas. There are various possibilities for further reducing the size of the target instance, which would be important for a practical implementation. For instance, one could use more sophisticated computations of the least model combined with target languages that are more compact than propositional CNF [Janhunen, 2004; Janhunen et al., 2009; Thiffault et al., 2004]. An extension of our approach to Abduction with other notions of solution-minimality, as surveyed by Eiter and Gottlob [1995], is left for future work. Adding empty clause detection can lead to smaller backdoors [Dilkina et al., 2007] and thus making our approach applicable to a larger class of instances. While finding such backdoors is not fixed-parameter tractable [Szeider, 2009], one could use heuristics to compute them [Dilkina et al., 2007].