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 [
Developers of modern ASP solvers such as Clasp [
In the literature, more ne-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 identi ed under which the
computational complexity drops and where the problems can be solved more
e ciently [
In this paper, we consider backdoor trees, which provide a more ne-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 2k (total) assignments to the atoms in the backdoor and thus 2k 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 xed 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 signi cantly fewer than 2k assignment reducts and (ii) we can signi cantly 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 de ne 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 su cient to nd all answer sets. 2. We show that backdoor tree evaluation is xed-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 xed-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 [
We consider a universe U of propositional atoms. A literal is an atom a 2 U or its negation a. A disjunctive logic program (or simply a program) P is a set of rules of the form a1 _ : : : _ al b1; : : : ; bn; c1; : : : ; cm where a1; : : : ; al; b1; : : : ; bn; c1; : : : ; cm are atoms and l; n; m are non-negative integers. We write H(r) = fa1; : : : ; alg (the head of r), B+(r) = fb1; : : : ; bng (the positive body of r), and B (r) = fc1; : : : ; cmg (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 ) = Sr2P at(r), respectively. We denote the number of rules of P by jP j = jf r : r 2 P gj. The size kP k of a program P is de ned as Pr2P jH(r)j + jB+(r)j + jB (r)j. A rule r is is normal if jH(r)j 1, r is a constraint (integrity rule) if jH(r)j = 0, 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 0 be programs. We say that P 0 is a subprogram of P (in symbols P 0 P ) if for each rule r0 2 P 0 there is some rule r 2 P with H(r0) H(r), B+(r0) B+(r), B (r0) B (r). Let C be a class of programs. We call a class C of programs hereditary if for each P 2 C all subprograms of P are in C as well.
A set M of atoms satis es a rule r if (H(r) [ B (r)) \ M 6= ; or B+(r)nM 6=
;. M is a model of P if it satis es 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 rst removing all rules r with B (r) \ M 6= ; and then removing all z
where z 2 B (r) from the remaining rules r [
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 brie y give some background on parameterized complexity. For more detailed
information we refer to other sources [
In the following, we brie y summarize the concept of ASP backdoors [
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 [
3
When we exploit a backdoor X of a program P to nd answer sets according
to a backdoor-based approach [
Py0
Px0 Px0;x1 Py0y1
Py0y1
Py0y1
Py0y1 Py0y1y2 : : :
Py0y1y2 : : :
Py0y1y2 : : :
Py0y1y2 : : :
Py0y1y2 : : :
Py0y1y2 : : :
Py0y1y2 : : :
Py0y1y2 : : : (a) Constructed from the strong Horn-backdoor Y (b) Constructed from the strong Horn-backdoor X backdoors e ciently. Evaluation of backdoors then consists of two steps: (i) computing the answer sets of the program P under the assignment for all 2 2X , which produces candidates for answer sets of P (or AS(P; X)1 for short), and (ii) checking for each M 2 AS(P; X) whether M is a minimal model of P M . In Step (i) we determine for each 2 2X 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 2jXj assignments in the worst case. However, there are answer set programs where we can nd a backdoor X for which we do not need all 2jXj assignments, as \shorter" assignments already yield a reduct that belongs to the considered target class. More formally, there is an assignment 0 such that 0 1 ( 1 for some 2 2X and the reduct P 0 already belongs to the target class C. Hence, when we incrementally assign truth values to atoms instead of taking an assignment 2 2X , 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. 1 Formally, AS(P; X) := f M [
Px0
Px0 We observe that Y = fy0; : : : ; ym 1g is a smallest strong Horn-backdoor. Figure 1(a) visualizes the assignments that we obtain when incrementally constructing the reducts for 2 2Y . Obviously, we need all 2jY j reducts since \removing" any atom from an assignment results in P 2= Horn. The set X = fx0; : : : ; x2m 1g is also a strong backdoor into Horn. The set X is larger than the set Y , but already for \shorter" assignments 0 than the assignment reducts 2 2X we obtain that the reduct belongs to Horn. For instance, the assignment 0 = fx1g yields the reduct Px1 = f y1 x0; x2; : : : ; x2m 1 g, 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 xed-parameter tractable when parameterized by the size of a
smallest backdoor into a subclass of normal programs [
Before we can make the observations from the previous examples precise, we provide some basic de nitions. 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 2 N to a set (t) f a; a : a 2 X g. We denote by X1(t) the positive literals of the labeling (t), i.e., X1(t) := (t) \ X. The corresponding assignment (t) of t is the assignment (t) where (t)(a) = 1 if a 2 (t) and (t)(a) = 0 if a 2 (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; t0 2 N , if t0 is a child of t, then either (t0) = (t) [ fag or (t0) = (t) [ fag for some atom a 2 X n (1t), and (iii) for any three nodes t; t1; t2 2 N , if t1 and t2 are children of t, then (t1) 6= (t2). We denote by at(BT ) the atoms occurring in assignments of BT , i.e., at(BT ) := St2N (1t).
Next, we give a de nition for backdoor trees of answer set programs. De nition 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 2 C for every leaf t 2 N and = (t). We denote by #leaves(BT) the number of leaves of T , i.e., #leaves(BT ) := jf t : t is a leaf of T gj. 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 speci cally, gs(BT ) := maxf jX1(t)j : t is a leaf of T g. For reasons explained below, we call gs(BT ) the Gallo-Scutella 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 2X 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 Scutella [
We consider the parameter in its original context and de nition as nested classes of families of sets on a family to generalize Horn formulas. Let S be a family of sets S1; : : : ; Sm, SX = S n f Y 2 S : X Y g, and S X := f S n X : S 2 S g for some set X. Moreover, (i) S 2 0 if and only if jSj 1 for each S 2 S and (ii) S 2 k if and only if there is some v 2 S1 i m Si such that Sfvg 2 k 1 and S fvg 2 k. Then, the class k consists of all propositional formulas F such that F 0 2 k where F 0 is obtained from F by removing all negative literals (note that we consider F 0 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. 4
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.
De nition 4 Let P be a program, X = at(P ), and BT = (T; ) a binary decision tree.
AS(P; ) :=f M [ 1(1) : M 2 AS(P ) g and
AS(P; BT ) :=f M : t is a leaf of T; = (t); M 2 AS(P; ) g:
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 ). 2 Due to space limitations, proofs of statements marked with \(?)" have been omitted. 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(` 2g nc) for some constant c.
Recall that Example 2 yields programs that have a C-backdoor tree BT with Gallo-Scutella 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(22mnc) 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) nc). 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 2 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 \justi cation" to set the atom to true.
We establish the following result.
Proposition 7 (?) Let C Normal. Given a program P of input size n, a C-backdoor tree BT = (T; ) of P of Gallo-Scutella parameter g = gs(BT ), a leaf t of T , and a set M AS(P; (t)) of atoms, we can check in time O(2g n) whether M is an answer set of P .
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 2 C and C is enumerable, we can compute AS(P ) in polynomial time for each leaf t 2 N and = (t), say in tim=e O((tn).cB)yfoPrrsoopmoesictoionnst7a,nwtec.cHanendceec,idjAeSw(hPet)hjer MO(n2cA)fSo(rPe)acihn lteimafetO2(N2g anncd) and jAS(P; )j O(2g nc) for each M 2 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 g nc) and check whether for Mg 2nAc)S.(PT;hTen) awlesocMan 2alsAoSs(oPlv)ehaollldpsrionbtleimmes Oin(`As2pFull from jAS(P; T )j O(` 2 AS(P ) within polynomial time. Consequently, the problem is xed-parameter tractable when parameterized by g + `. tu
There are two factors for hardness of ASP problems when parameterized by the Gallo-Scutella 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 re ned 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. 5
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 .
Observation 9 (?) Let BT be a binary decision tree, n = jat(BT )j, g = gs(BT ), and ` = #leaves(BT ). Then, g n ` 1 (1 + n)g 1.
We establish that every strong backdoor of size k yields a backdoor tree consisting of at least k + 1 leaves and at most 2k 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, jXj + 1 #leaves(BT ) 2jXj.
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) := f M [ 1(1) : 2 2X\ at(P ); M 2 AS(P ) g. Then, AS(P; BT ) AS(P; X).
Lemma 12 (?) 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 Gallo-Scutella parameter gs(BT ) of P . Then, gs(BT ) jXj.
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 xing an arbitrary order on the atoms in X
and constructing incrementally all partial assignments until P 2 C or assigns
all atoms in X. Therefore, we have to consider at most 2k+1 1 reducts as we
xed the order on the backdoor atoms. Using the standard backdoor approach
requires to solve the problems in AspFull a running time O(22jXjnc) [
When we want to exploit backdoor trees to solve a problem instance, we have to
detect the backdoor tree rst. In this section, we show that detecting
Horn-backdoor trees is xed-parameter tractable when parameterized by Gallo-Scutella
parameter and number of leaves. We establish our xed-parameter tractability
results via kernelization, which is in parameterized complexity theory a
fundamental method for establishing such results [
We rst de ne the following decision problem: C-Backdoor-Tree Detection(GS,Leaves) Given: A program P , an integer g 0, and an integer ` 0. Parameter: The integer g + `.
Task: Decide whether P has a C-backdoor tree BT of Gallo-Scutella parameter gs(BT ) g and #leaves(BT ) `.
By self-reduction (or self-transformation) [
In the following, we consider backdoor tree detection when parameterized by
the Gallo-Scutella parameter g and the number of leaves ` of a backdoor tree.
Therefore, we consider notions coined by Samer and Szeider [
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 k2 + 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 nd such kernels for the problem Strong Horn-Backdoor Detection.
De nition 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 jKj f (k).
Lemma 16 ([
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 k2 + k (if it exists). If P has a C-backdoor tree BT = (T; ) of Gallo-Scutella 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 nd a suitable C-backdoor tree, we can just try in brute-force all possible C-backdoor trees of P of Gallo-Scutella parameter at most g and of at most ` leaves. Consequently, the theorem follows. tu
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 xed-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 nd 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 xed-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 o when using our minimality check approach. In other words, the evaluation problem is xed-parameter tractable when parameterized by the number of leaves of backdoor tree. We obtain a parameter that might be signi cantly smaller, but the running time of the evaluation algorithm can be signi cantly worse (exponentially). On the other hand, one could parameterize the evaluation problem just by the Gallo-Scutella parameter (the maximal number of atoms that we have to set to true in any leaf) of the backdoor tree. Since the Gallo-Scutella 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-Scutella parameter of the backdoor tree, the number of reducts remains non-uniformly bounded. Hence, it remains open whether we obtain xed-parameter tractability. Moreover, the backdoor tree detection problem when parameterized by the Gallo-Scutella parameter is only known to be in XP and the question of whether it can be carried out in xed-parameter tractable time is currently open.