We translate the concept of backdoor trees from SAT to propositional Answer Set Programming (ASP). By means of backdoor trees we can reduce a reasoning task for a general ASP instance to reasoning tasks on several tractable ASP instances. We demonstrate that the number of tractable ASP instances can be drastically reduced in comparison to a related approach based on strong backdoors.
Answer Set Programming (ASP) is a popular framework for declarative modelling and problem solving [25,33,35]. It has successfully been used to solve a wide variety of problems in artificial intelligence and reasoning, e.g., match making [23], optimization of packaging of Linux distributions [24], reasoning in robots [4], and shift design [1]. In ASP, problems are usually modelled by means of rules and constraints that form a disjunctive logic program. The solutions to the program are the so-called answer sets (or stable models). Solving a problem means to search for answer sets of logic programs. In this paper, we are mainly interested in computational decision problems for propositional disjunctive ASP such as deciding whether a program has an answer set (Consistency), whether a certain atom is contained in at least one (Brave Reasoning) or in all answer sets (Skeptical Reasoning). Further, we consider the problems counting all answer sets (Counting) and enumerating all answer sets (Enum).
Developers of modern ASP solvers such as Clasp [26] or Wasp [3] have demonstrated in several competitions [2,8,10,27,28] that ASP solving can be efficiently used to solve a wide variety of instances. However from the perspective of classical worst case complexity, many decision problems for disjunctive ASP are "harder than NP" and have a higher worst-case complexity than CSP and Sat. More precisely, the problems Consistency, Brave Reasoning, and Skeptical Reasoning are complete for the second level of the Polynomial Hierarchy [13].
In the literature, more fine-grained results on computational complexity of the ASP decision problems have been established. Syntactic properties where the input is restricted to certain fragments have been identified under which the computational complexity drops and where the problems can be solved more
The first author has been supported by the Austrian Science Fund (FWF), Grant Y698, and is also affiliated with the Institute of Computer Science and Computational Science at University of Potsdam, Germany.
efficiently [29,5,6,39,18]. Parameterized complexity analyses, which take the input size of an instance along with a parameter, indicating the presence of a certain "hidden structure", have been carried out [7,14,15,16,17,32]. The central idea of parameterized complexity is that instances originating in practical applications are often structured in a way that facilitates obtaining a solution relatively fast. An interesting parameter can be gained from backdoors [16]. Backdoors can be used as clever reasoning shortcuts through the search space. For a backdoor one usually fixes a class C of programs, commonly called target class, where the problem under consideration is computationally easier, e.g., the class of Horn programs. Given an input program P , a strong backdoor into the target class C is a preferably small set X of atoms such that for any truth assignment τ to the atoms in X the program under the truth assignment τ (the reduct P τ , see Definition 1) belongs to C. Then, for program P and a strong backdoor X into C we have to consider 2 |X| truth assignments to the atoms in the backdoor X. Exploiting backdoors usually consists of two steps (i) finding a backdoor of the given instance (backdoor detection) and (ii) applying the backdoor to the instance, determining a candidate solution, and verifying its minimality (backdoor evaluation).
In this paper, we consider backdoor trees, which provide a more fine-grained approach to the evaluation of strong backdoors, where we take partial assignments in the evaluation into account. When using backdoors for a parameterized complexity analysis one only considers the size k of a backdoor as a parameter. Evaluating a given backdoor results in 2 k (total) assignments to the atoms in the backdoor and thus 2 k programs with respect to the possible assignments. However, a partial assignment to fewer than k atoms can already yield a program that belongs to the fixed target class. Therefore, we consider binary decision trees, which make partial assignments to backdoor atoms in a program precise and lead us to the notion of backdoor trees. We investigate under which conditions (i) we need to consider significantly fewer than 2 k assignment reducts and (ii) we can significantly improve parts of the backdoor evaluation (minimality check) if those assignments set only a small number of atoms to true.
Our main contributions are as follows:
1. We define backdoor trees for Answer Set Programming, extend the concept of backdoors from sets to trees (with similar steps detection and evaluation), and establish that the reducts that we obtain from a backdoor tree are sufficient to find all answer sets. 2. We show that backdoor tree evaluation is fixed-parameter tractable when parameterized by a composed parameter, which incorporates considerations of (i) and (ii) from above of a given backdoor tree into Horn and other classes. 3. We establish fixed-parameter tractability for backdoor tree detection for backdoor trees into the target class Horn.
Related Work. Backdoors were originally introduced by Williams, Gomes, and Selman [40] as a tool for the theoretical analysis of decision heuristics in the area of Sat and CSP. Nishimura et al. [36] started a systematic investigation of the parameterized complexity of backdoor detection for SAT, which triggered a lot of follow-up work [21]. Samer and Szeider [37] introduced backdoor trees for Sat as a refinement of backdoors and showed that Sat is fixed parameter tractable when parameterized by the number of leaves in a backdoor tree. The problems of detecting backdoor trees into 2CNF and Horn formulas are fixed parameter tractable.
2 Preliminaries We write H(r) = {a 1 , . . . , a l } (the head of r), B + (r) = {b 1 , . . . , b n } (the positive body of r), and B − (r) = {c 1 , . . . , c m } (the negative body of r). We denote the sets of atoms occurring in a rule r or in a program P by at(r) = H(r) ∪ B + (r) ∪ B − (r) and at(P ) = r∈P at(r), respectively. We denote the number of rules of P by |P | = |{ r : r ∈ P }|. The size P of a program P is defined as
r is Horn if it is positive and normal or a constraint. We say that a program has a certain property if all its rules have the property. Horn refers to the class of all Horn programs. We denote the class of all normal programs by Normal. Let P and P be programs. We say that P is a subprogram of P (in symbols P ⊆ P ) if for each rule r ∈ P there is some rule r ∈ P with H(r ) ⊆ H(r), B + (r ) ⊆ B + (r), B − (r ) ⊆ B − (r). Let C be a class of programs. We call a class C of programs hereditary if for each P ∈ C all subprograms of P are in C as well.
A set M of atoms satisfies a rule r if (H(r) ∪ B − (r)) ∩ M = ∅ or B + (r)\M = ∅. M is a model of P if it satisfies all rules of P . The Gelfond-Lifschitz (GL) reduct of a program P under a set M of atoms is the program P M obtained from P by first removing all rules r with B − (r) ∩ M = ∅ and then removing all z where z ∈ B − (r) from the remaining rules r [30]. M is an answer set (or stable model ) of a program P if M is a minimal model of P M . We denote by AS(P ) the set of all answer sets of P . A class C of programs is enumerable if for each P ∈ C we can compute AS(P ) in polynomial time.
In this paper, we consider the following fundamental ASP problems for a given program P : Consistency asks whether P has an answer set, Brave Reasoning asks whether a belongs to some answer set of P , Skeptical Reasoning asks whether a belongs to all answer sets of P , Counting asks to compute the number of answer sets of P , and Enum asks to list all answer sets of P . We denote by AspFull the family of all problems Consistency, Brave Reasoning, Skeptical Reasoning, Counting, and Enum.
We briefly give some background on parameterized complexity. For more detailed information we refer to other sources [11,12,19,31,34]. An instance of a parameterized problem L is a pair (I, k) ∈ Σ * × N for some finite alphabet Σ. For an instance (I, k) ∈ Σ * × N we call I the main part and k the parameter. I denotes the size of I. L is fixed-parameter tractable if there exist a computable function f and a constant c such that we can decide by an algorithm whether
FPT is the class of all fixed-parameter tractable decision problems. The class XP of non-uniform polynomial-time tractable problems consists of all parameterized decision problems that can be solved in polynomial time if the parameter is considered constant. That is, (I, k) ∈ L can be decided in time O( I f (k) ) for some computable function f .
In the following, we briefly summarize the concept of ASP backdoors [17]. A (truth) assignment is a mapping τ : X → {0, 1} defined for a set X ⊆ U of atoms. For x ∈ X, we define τ (x) = 1 − τ (x). By 2 X we denote the set of all assignments τ :
Definition 1 (Strong C-Backdoor [17]) Let P be a program, X a set of atoms, and τ ∈ 2 X an assignment. The reduct of P under τ is the logic program P τ obtained from P by (i) removing all rules r with H(r) ∩ τ −1 (1) = ∅ or H(r) ⊆ X; (ii) removing all rules r with B + (r) ∩ τ −1 (0) = ∅; (iii) removing all rules r with B − (r) ∩ τ −1 (1) = ∅; (iv) removing from the heads and bodies of the remaining rules all literals a, ā with a ∈ X. Let C be a class of programs. A set X of atoms is a strong C-backdoor of a program P if P τ ∈ C for all assignments τ ∈ 2 X . By a minimal strong C-backdoor of a program P we mean a strong C-backdoor of P that does not properly contain a smaller strong C-backdoor of P ; a smallest strong C-backdoor of P is one of smallest cardinality.
A result by Fichte and Szeider [17] states that all problems in AspFull are fixed-parameter tractable when parameterized by the size of a given strong C-backdoor for an enumerable target class C ⊆ Normal and that finding a strong backdoor is also fixed-parameter tractable for various target classes, including Horn.
When we exploit a backdoor X of a program P to find answer sets according to a backdoor-based approach [17], the exponential blowup of the running time depends only on the size of the backdoor X. Thus, we want to find smallest backdoors efficiently. Evaluation of backdoors then consists of two steps: (i) computing the answer sets of the program P under the assignment τ for all τ ∈ 2 X , which produces candidates for answer sets of P (or AS(P, X)1 for short), and (ii) checking for each M ∈ AS(P, X) whether M is a minimal model of P M . In
Step (i) we determine for each τ ∈ 2 X the answer sets of the reducts P τ and then check whether these answer sets give rise to an answer set of P . Consequently, we have to consider all the 2 |X| assignments in the worst case. However, there are answer set programs where we can find a backdoor X for which we do not need all 2 |X| assignments, as "shorter" assignments already yield a reduct that belongs to the considered target class. More formally, there is an assignment τ such that τ −1 τ −1 for some τ ∈ 2 X and the reduct P τ already belongs to the target class C. Hence, when we incrementally assign truth values to atoms instead of taking an assignment τ ∈ 2 X , some atoms in τ can be irrelevant for the question whether the reduct belongs to C.
Interestingly, in some cases it is of advantage to use a backdoor that is not a smallest backdoor into the target class C. We show this in the following example. Example 1. Let m be some positive integer. Consider the following program:
We observe that Y = {y 0 , . . . , y m−1 } is a smallest strong Horn-backdoor.
Figure 1(a) visualizes the assignments that we obtain when incrementally constructing the reducts for τ ∈ 2 Y . Obviously, we need all 2 |Y | reducts since "removing" any atom from an assignment τ results in P τ / ∈ Horn. The set X = {x 0 , . . . , x 2m−1 } is also a strong backdoor into Horn. The set X is larger than the set Y , but already for "shorter" assignments τ than the assignment reducts τ ∈ 2 X we obtain that the reduct belongs to Horn. For instance, the assignment τ = {x 1 } yields the reduct P x1 = { y 1 ← x 0 , x 2 , . . . , x 2m−1 }, which belongs to Horn. Hence, we obtain only 2m + 1 reducts, see Figure 1(b).
Example 1 shows that incrementally assigning backdoors can yield reducts that belong to the considered target class even though not all atoms of the backdoor are assigned. Then, larger backdoors can yield an exponentially smaller number of such reducts. A main part for backdoor evaluation is to check whether a model is a minimal model ("minimality check"). The task is co-NP-complete in general, but fixed-parameter tractable when parameterized by the size of a smallest backdoor into a subclass of normal programs [17]. For the minimality check we have to consider all backdoor atoms that have been set to true by any assignment. Hence the backdoor Y from Example 1 yields a significantly smaller number of reducts, however for the minimality check we still have to consider all subsets of Y . Conversely, we construct subsequently in Example 2 a program where the number of assignments that we obtain from a smallest strong backdoor can be arbitrarily larger than the maximum number of atoms in a backdoor that have been set to true by any assignment on a much larger number of atoms.
Example 2. Let m be some positive integer. We define the following program:
Y = {y 0 , . . . , y m−1 } is a smallest strong Horn-backdoor and again Figure 1(a) illustrates how we incrementally construct the reducts until P τ ∈ Horn. Same as in Example 1 we have a complete binary tree with 2 m leaves. Further, we easily observe that X = {x 0 , x 1 , . . . , x 2m−1 } is a strong Horn-backdoor. Figure 2 visualizes the assignments that we obtain when incrementally constructing the reducts τ ∈ 2 X . There we have only 2m + 1 reducts where at most one atom is set to true.
Before we can make the observations from the previous examples precise, we provide some basic definitions. Let X be a set of atoms, T = (N, E, r) a binary tree with root r, and χ a labeling that maps any node t ∈ N to a set χ(t) ⊆ { a, ā : a ∈ X }. We denote by X 1 (t) the positive literals of the labeling χ(t), i.e., X 1 (t) := χ(t) ∩ X. The corresponding assignment τ χ(t) of t is the assignment τ χ(t) where τ χ(t
The pair BT = (T, χ) is a binary decision tree of P if X ⊆ at(P ) and the following conditions hold: (i) for the root r we have χ(r) = ∅, (ii) for any two nodes t, t ∈ N , if t is a child of t, then either χ(t ) = χ(t) ∪ {ā} or χ(t ) = χ(t) ∪ {a} for some atom a ∈ X \ τ −1 χ(t) , and (iii) for any three nodes t, t 1 , t 2 ∈ N , if t 1 and t 2 are children of t, then χ(t 1 ) = χ(t 2 ). We denote by at(BT ) the atoms occurring in assignments of BT , i.e., at(BT ) := t∈N τ −1 χ(t) . Next, we give a definition for backdoor trees of answer set programs.
Definition 2 Let P be a program and BT = (T, χ) be a binary decision tree of P where T = (N, E, r). The pair BT = (T, χ) is a C-backdoor tree of P if P τ ∈ C for every leaf t ∈ N and τ = τ χ(t) . We denote by #leaves(BT) the number of leaves of T , i.e., #leaves(BT ) := |{ t : t is a leaf of T }|. We denote by gs(BT ) the maximum number of atoms that have been set to true by a corresponding assignment of any leaf of T , more specifically, gs(BT ) := max{ |X 1 (t)| : t is a leaf of T }. For reasons explained below, we call gs(BT ) the Gallo-Scutellà parameter of BT .
In other words, a backdoor tree of a program P is a binary decision tree where the nodes of the tree are labeled by assignments τ ∈ 2 X on subsets X ⊆ at(P ), the corresponding partial assignment τ of an inner node yields a reduct P τ that does not belong to the considered target class, and the corresponding assignment τ of a leaf yields a reduct P τ that belongs to the considered target class.
Gallo and Scutellà [20] introduced a hierarchy of classes of CNF formulas, with the class of Horn formulas (each clause containing at most one positive literal) forming its lowest level. They showed that for each level g of the hierarchy, there are polynomial time algorithms fro checking whether a given formula belongs to this level and whether a given formula from this level is satisfiable. The order of the polynomial bounding the running time, however, depends on the level k. Therefore these algorithms do not establish fixed-parameter tractability of these problems, and only render the problems as being in the class XP (see Subsection 2.2).
We consider the parameter in its original context and definition as nested classes of families of sets on a family to generalize Horn formulas. Let S be a family of sets S 1 , . . . , S m , S X = S \ { Y ∈ S : X ⊆ Y }, and S − X := { S \ X : S ∈ S } for some set X. Moreover, (i) S ∈ Σ 0 if and only if |S| ≤ 1 for each S ∈ S and (ii) S ∈ Σ k if and only if there is some v ∈ 1≤i≤m S i such that S {v} ∈ Σ k−1 and S − {v} ∈ Σ k . Then, the class Γ k consists of all propositional formulas F such that F ∈ Σ k where F is obtained from F by removing all negative literals (note that we consider F as a set of clauses and a clause is a set of literals). Observe that Γ 0 consists of all Horn formulas.
A backdoor tree of F into Horn formulas is a binary decision tree where the reduced formula F τ is Horn for each leaf t and its corresponding assignment τ . Proposition 3 (2 ) A propositional formula F belongs to Γ k if and only if there is a backdoor tree BT = (T, χ) into Horn formulas of F such that gs(BT ) ≤ k.
In this section, we establish an analogue to backdoor evaluation for backdoor trees. Again we consider the reducts P τ together with the atoms that are set to true and extend this notion to the corresponding assignments of the leaves for binary decision trees.
Definition 4 Let P be a program, X = at(P ), and BT = (T, χ) a binary decision tree.
In other words, the sets in AS(P, BT ) are answer sets of P τ for assignments τ to χ(t) ∩ at(P ) extended by those atoms which are set to true by τ . In the following lemma we will see that the elements in AS(P, BT ) are all the "answer set candidates" of the original program P . The concepts are similar to ASP backdoors, but slightly more sophisticated. Lemma 5 ( ) Let P be a program and BT = (T, χ) a binary decision tree of P . Then, AS(P ) ⊆ AS(P, BT ).
Theorem 6 Given a disjunctive program P , an enumerable class C ⊆ Normal, and a C-backdoor tree BT = (T, r, χ) of P . Let g = gs(BT ), = #leaves(BT ), and n be the input size of P . Then, the problems in AspFull can be solved in time O( • 2 g • n c ) for some constant c.
Recall that Example 2 yields programs that have a C-backdoor tree BT with Gallo-Scutellà parameter gs(BT ) = 1 and 2m + 1 leaves whereas a smallest backdoor is of size m. Backdoor evaluation [16,Thm. 3.9] yields a running time O(2 2m n c ) for some constant c and input size n of program P . In contrast, using Theorem 6 we can evaluate the backdoor tree BT in time O(2(2m + 1) • n c ). Consequently, we obtain an exponential speedup for certain programs. In the next section, we will compare backdoor trees with backdoors in more detail.
Before proving Theorem 6, we need to make some observations. In view of Lemma 5 we have to consider the corresponding reducts of the leaves t in the backdoor tree. For each leaf t and its corresponding assignment τ we construct the reduct P τ and compute the set AS(P τ ). Then, we obtain the set AS(P ) by checking for each M ∈ AS(P τ ) whether it gives rise to an answer set of P . The crucial part is again to consider minimality with respect to the Gelfond-Lifschitz reduct. For the leaf t and its corresponding assignment τ we can guarantee minimality with respect to the reduct (P τ ) M . Setting atoms to true by the assignment τ does apparently not guarantee minimality with respect to P M (cf. Lemma 5). Hence, we have to check for each atom in τ −1 (1) whether there is a "justification" to set the atom to true.
We establish the following result. whether M is an answer set of P .
We are now in position to establish Theorem 6.
Proof of of Theorem 6. Let BT = (T, r, χ) be the given C-backdoor tree, g = gs(BT ), = #leaves(BT ), T = (N, E, r), and n the input size of P . According to Lemma 5, AS(P ) ⊆ AS(P, BT ). Since P τ ∈ C and C is enumerable, we can compute AS(P τ ) in polynomial time for each leaf t ∈ N and τ = τ χ(t) , say in time O(n c ) for some constant c. Hence, |AS(P τ )| ≤ O(n c ) for each leaf t ∈ N and τ = τ χ(t) . By Proposition 7, we can decide whether
) for each M ∈ AS(P, τ ) where τ = τ χ(t) and t is a leaf of T . Since there are at most l many leaves, we can compute AS(P, T ) and check whether for M ∈ AS(P, T ) also M ∈ AS(P ) holds in time O( • 2 g • n c ) and
). Then we can also solve all problems in AspFull from AS(P ) within polynomial time. Consequently, the problem is fixed-parameter tractable when parameterized by g + .
There are two factors for hardness of ASP problems when parameterized by the Gallo-Scutellà parameter plus the size a backdoor tree (i) atoms that are set to true which yield potential candidates and are hence important for the minimality check in each leaf; and (ii) leaves in a backdoor tree which yield the reducts we have to consider. Both factors of hardness are "used" in the proof of Theorem 6. Hence, in contrast to Sat backdoor trees we do not simply parameterize the reasoning problems in AspFull by #leaves(BT ) of a given backdoor tree BT = (T, χ) of P to obtain a more refined view on backdoors. Instead we also consider gs(BT ) which is the maximum number of atoms that are set to true in a leaf of T . This is attributed to the minimality check where we have to consider the number of atoms that are set to true.
In this section, we investigate some connections between backdoors and backdoor trees. We show that our composed parameter based on backdoor trees is more general than the size of a backdoor. Lemma 8 ( ) Let P be a program and C be a hereditary class of programs. If BT is a C-backdoor tree of P , then at(BT ) is a strong C-backdoor of P .
We make the following observations about binary decision trees. Observation 9 ( ) Let BT be a binary decision tree, n = |at(BT )|, g = gs(BT ), and = #leaves(BT ). Then,
We establish that every strong backdoor of size k yields a backdoor tree consisting of at least k + 1 leaves and at most 2 k leaves. Lemma 10 ( ) Let P be a program, C a hereditary class of programs, X a strong C-backdoor of smallest size of P , and BT = (T, χ) a C-backdoor tree of smallest number of leaves of P . Then,
The next observation states that we obtain fewer "answer set candidates" when evaluating ASP backdoor trees than by evaluating ASP backdoors. Observation 11 ( ) Let P be a program, BT = (T, χ) a binary decision tree of P , X := at(BT ), and AS(P, X) := { M ∪τ −1 (1) : τ ∈ 2 X∩ at(P ) , M ∈ AS(P τ ) }. Then, AS(P, BT ) ⊆ AS(P, X). Besides having the potential of an exponential speedup (see Example 2), we can trivially construct from a strong C-backdoor X a C-backdoor tree of P with g = gs(BT ) and = #leaves(BT ) by fixing an arbitrary order on the atoms in X and constructing incrementally all partial assignments τ until P τ ∈ C or τ assigns all atoms in X. Therefore, we have to consider at most 2 k+1 − 1 reducts as we fixed the order on the backdoor atoms. Using the standard backdoor approach requires to solve the problems in AspFull a running time O(2 2|X| n c ) [16] for some constant c. By Theorem 6 we can produce solutions in time O(2 g+log • n c ) for some constant c. Since g ≤ k and log ≤ k by Lemmas 12 and 10, 2 2|X| ≥ 2 g+log . In that way, backdoor trees can only improve the efficiency compared to the traditional backdoor approach.
When we want to exploit backdoor trees to solve a problem instance, we have to detect the backdoor tree first. In this section, we show that detecting Horn-backdoor trees is fixed-parameter tractable when parameterized by Gallo-Scutellà parameter and number of leaves. We establish our fixed-parameter tractability results via kernelization, which is in parameterized complexity theory a fundamental method for establishing such results [22]. Intuitively, we can think of a kernel as a "compressed" version of the input, where the size of a kernel is bounded by some computable function of the parameter only and the kernel is produced by a polynomial-time reduction. However, here we need a more restrictive notion of a kernel, loss-free kernels [37], which also occur in the context of subset minimization under the notion of a full kernel [9]. A loss-free kernel contains the union of all minimal solutions and represents in a certain way all solutions.
We first define the following decision problem:
C-Backdoor-Tree Detection(GS,Leaves)
A program P , an integer g ≥ 0, and an integer ≥ 0. Parameter: The integer g + .
Decide whether P has a C-backdoor tree BT of Gallo-Scutellà parameter gs(BT ) ≤ g and #leaves(BT ) ≤ .
By self-reduction (or self-transformation) [38,11,12], we can use a decision algorithm for C-Backdoor-Tree Detection(GS,Leaves) to actually find the backdoor. Again we only require the target class to be hereditary. Lemma 13 ( ) Let C be a hereditary class of programs. If C-Backdoor-Tree Detection(GS,Leaves) is fixed-parameter tractable, then also finding a C-backdoor tree of a given program P of Gallo-Scutellà parameter at most g and at most leaves is fixed-parameter tractable (when parameterized by g + ).
In the following, we consider backdoor tree detection when parameterized by the Gallo-Scutellà parameter g and the number of leaves of a backdoor tree. Therefore, we consider notions coined by Samer and Szeider [37] in the setting of propositional satisfiability and apply it to Answer Set Programming.
The problem Horn-Backdoor-Tree Detection(GS,Leaves) is fixed-parameter tractable.
The main ingredient for the proof is that we obtain in polynomial-time an input program a set K of atoms of size at most k 2 + k such that we preserve the union of all minimal strong Horn-backdoors of size at most k (Lemma 16). In the previous section, we observed that k is bounded by 2 . Then, because of the loss-less kernel we can enumerate all C-backdoor trees by brute-force and check for each tree whether the desired parameters are present.
Before we can establish the result, we introduce the notion of a loss-free kernelization for ASP and show how to find such kernels for the problem Strong Horn-Backdoor Detection.
Definition 15 Let C be a class of programs. A loss-free kernelization of the problem Strong C-Backdoor Detection is a polynomial-time algorithm that given an instance (I, k), either correctly decides that I does not have a strong C-backdoor of size at most k, or computes a set K ⊆ at(P ) such that the following conditions hold:
1. X ⊆ K for every minimal strong C-backdoor X of size at most k and 2. there is a computable function f such that |K| ≤ f (k).
The problem Strong Horn-Backdoor Detection has a loss-free kernelization with loss-free kernels of size k 2 + k.
We are now in position to establish Theorem 14.
Proof of Theorem 14. Let C be a class of programs, P a program, g, > 0 integers, and k := 2 . According to Lemma 16, we compute in polynomial-time for the problem Strong Horn-Backdoor Detection a loss-free kernel K ⊆ at(P ) of size at most k 2 + k (if it exists). If P has a C-backdoor tree BT = (T, χ) of Gallo-Scutellà parameter g and at most leaves, then at(BT ) is a minimal strong C-backdoor, g ≤ at(BT ), and #leaves(BT ) ≤ − 1. We claim that at(BT ) ⊆ K for any C-backdoor tree BT with gs(BT ) ≤ g and ≤ #leaves(BT ). This follows since at(BT ) contains all minimal strong C-backdoors of size at most k and K is a loss-free kernel. To actually find a suitable C-backdoor tree, we can just try in brute-force all possible C-backdoor trees of P of Gallo-Scutellà parameter at most g and of at most leaves. Consequently, the theorem follows.
In view of this result we can drop the assumption in Theorem 6 that the backdoor is provided as input:
Corollary 17 Let C ⊆ Normal be an enumerable class. The problems in AspFull are all fixed-parameter tractable when parameterized by gs(BT ) + #leaves(BT ) of a smallest gs(BT ) + #leaves(BT ) C-backdoor tree BT .
Proof. Let P be a program and k an integer. Since there are only linearly many combinations for k = g + l, we can use Lemma 13 to find a C-backdoor tree BT of smallest gs(BT ) + #leaves(BT ) where gs(BT ) ≤ g and #leaves(BT ) ≤ l if it exists. The remainder follows from Theorem 6.
We have introduced backdoor trees to Answer Set Programming. The general concept is similar to the Sat setting but requires additional considerations. The minimality check, which is necessary to verify minimality of potential answer set candidates with respect to the Gelfond-Lifschitz reduct, yields to additional requirements. Therefore, we parameterize the problem of backdoor tree evaluation by a parameter composed of the number of leaves of a backdoor tree and maximum number of atoms that are set to true by a corresponding assignment in a leaf. The former part is crucial to bound the number of potential reducts and hence to bound the number of answer set candidates. The latter part is crucial to bound the number of atoms in any assignment, which we additionally have to consider for the minimality check.
Our parameterization raises the question of whether we can drop one part from the composed parameter. On the one hand, one could parameterize the evaluation problem just by the number of leaves of the backdoor tree, which yields fixed-parameter tractability, but then the evaluation algorithm does not necessarily yield any speedup in the algorithm since we still have to consider the minimality check where a bound on the number of leaves does not pay off when using our minimality check approach. In other words, the evaluation problem is fixed-parameter tractable when parameterized by the number of leaves of backdoor tree. We obtain a parameter that might be significantly smaller, but the running time of the evaluation algorithm can be significantly worse (exponentially). On the other hand, one could parameterize the evaluation problem just by the Gallo-Scutellà parameter (the maximal number of atoms that we have to set to true in any leaf) of the backdoor tree. Since the Gallo-Scutellà parameter of a backdoor tree can be arbitrarily small compared to the number of leaves of a backdoor tree (and hence the size of a smallest backdoor), we obtain an arbitrarily smaller parameter. However, since our upper bound for the number of reducts is (1 + n) g , where n is the number of atoms of the given program and g the Gallo-Scutellà parameter of the backdoor tree, the number of reducts remains non-uniformly bounded. Hence, it remains open whether we obtain fixed-parameter tractability. Moreover, the backdoor tree detection problem when parameterized by the Gallo-Scutellà parameter is only known to be in XP and the question of whether it can be carried out in fixed-parameter tractable time is currently open.