Backdoors to Tractable Answer-Set Programming

1 Introduction

Answer-Set Programming (ASP) is an increasingly popular framework for declarative programming [Marek and Truszczy´nski, 1999; Niemel¨a, 1999]. ASP allows to describe a problem by means of rules and constraints that form a disjunctive logic program. Solutions to the program are socalled stable models or answer sets. Many important problems of AI and reasoning can be represented and successfully solved within the ASP framework. However, the main computational problems for ASP (such as deciding whether a program has a solution, or if a certain atom is contained in at least one or in all solutions) are of high worst-case complexity and are located at the second level of the Polynomial Hierarchy [Eiter and Gottlob, 1995]. The known complexity results do not rule out the possibility for exact algorithms that work efficiently for real-world instances by exploiting the presence of a "hidden structure."

∗Research supported by ERC (COMPLEX REASON 239962).

In this paper we follow a new approach of making the vague notion of a hidden structure precise. Our approach is based on the concept of backdoors which is widely used in the areas of propositional satisfiability and constraint satisfaction (see, e.g., [Williams et al., 2003a; Gottlob and Szeider, 2006; Samer and Szeider, 2009]), and also for quantified Boolean formulas and argumentation [Samer and Szeider, 2009a; Ordyniak and Szeider, 2011].

A backdoor is a small set of key atoms that represent a "clever reasoning shortcut" through the search space. By deciding the status of the atoms in the backdoor, we can reduce a given program to several tractable programs belonging to a target class of programs. Consequently the evaluation of the given program is fixed-parameter tractable in the size of the backdoor, i.e., polynomial for fixed backdoor size k where the order of the polynomial is independent of k [Downey and Fellows, 1999]. By allowing backdoors of increasing size k = 1, 2, 3, . . . we can gradually augment a known tractable class of programs.

Results:

• We show that the most important computational problems of propositional answer-set programming, including credulous/skeptical reasoning (and even counting all answer sets) are fixed-parameter tractable in the size of the backdoor.
• We show that the detection of backdoors is fixedparameter tractable for various target classes, including the class of all Horn programs and classes based on various notions of acyclicity. This way we make recent results of fixed-parameter algorithmics accessible to the field of answer-set programming.
• We show that the concept of backdoors entails fixedparameter tractability results for answer-set programming [Ben-Eliyahu, 1996] and so provides a unifying framework.
• We compare backdoor size with respect to various base classes with each other and with the recently studied parameter incidence treewidth [Jakl et al., 2009].
• We present first empirical results where we consider the backdoor size of structured programs and random programs of varied density.

2 Formal Background

We consider a universe U of propositional atoms. A literal is an atom a ∈ U or its negation ¬a. A disjunctive logic program (or simply a program) P is a set of rules of the form x1 ∨ . . . ∨ xl ← y1, . . . , yn, ¬z1, . . . , ¬zm where x1, . . . , xl, y1, . . . , yn, z1, . . . , zm are atoms and l, n,m are non-negative integers. We write {x1, . . . , xl} = H(r) (the head of r) and {y1, . . . , yn, z1, . . . , zm} = B(r) (the body of r), B+(r) = {y1, . . . , yn} and B-(r) = {z1, . . . , zn}. We denote the sets of atoms occurring in a rule r or in a program P by at(r) = H(r) ∪ B(r) and at(P) = ⋃r∈P at(r), respectively.

A rule r is negation-free if B-(r) = ∅, r is normal if |H(r)| = 1, r is a constraint if |H(r)| = 0, r is disjunctionfree if |H(r)| ≤ 1, r is Horn if it is negation-free and disjunction-free, and r is tautological if B+(r) ∩ (H(r) ∪ B-(r)) ̸= ∅. We say that a program has a certain property if all its rules have the property. We denote by Horn the classes of all Horn programs.

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 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 second removing all ¬z where z ∈ B-(r) from all remaining rules r [Gelfond and Lifschitz, 1991]. M is an answer set (or stable set) of a program P if M it is a minimal model of P M . We denote by AS(P) the set of all answer sets of P.

We also need some notions from propositional satisfiability. A clause is a finite set of literals, a CNF formula is a finite set of clauses. A truth assignment is a mapping τ : X → {0, 1} defined for a set X ⊆ U of atoms. For x ∈ X we put τ (¬x) = 1-τ (x). By ta(X) we denote the set of all truth assignments τ : X → {0, 1}. The truth assignment reduct of a CNF formula F with respect to τ ∈ ta(X) is the CNF formula Fτ obtained from F by first removing all clauses c that contain a literal set to 1 by τ, and second removing from the remaining clauses all literals set to 0 by τ . τ satisfies F if Fτ = ∅, and F is satisfiable (in symbols sat(F)) if it is satisfied by some τ.

ASP Problems The main computational problems for ASP are as follows. CONSISTENCY: given a program P, does P have an answer-set? CREDULOUS/SKEPTICAL REASONING: given a program P and an atom a ∈ at(P), is a contained in some/all answer-set(s) of P? AS COUNTING: how many answer sets does P have? AS ENUMERATION: list all answer sets of P. CONSISTENCY and CREDULOUS REASONING are ΣP2 -complete, SKEPTICAL REASONING is ΠP2 -complete [Eiter and Gottlob, 1995]. The problems remain NP (or co-NP) hard for normal programs [Marek and Truszczy´nski, 1991], but are polynomial-time solvable for Horn programs [Gelfond and Lifschitz, 1988]. AS COUNTING is easily seen to be #P-hard even for normal programs in view of the #P -completeness of #SAT.

Fixed-Parameter Tractability We give some basic background on parameterized complexity. For more detailed information we refer to other sources [Downey and Fellows, 1999; Gottlob and Szeider, 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 exist a computable function f and a constant c such that we can decide whether (I, k) ∈ L in time O(f(k)‖I‖c ) where ‖I‖ denotes the size of I. FPT is the class of all fixed-parameter tractable decision problems. The Weft Hierarchy consists of parameterized complexity classes W[1] ⊆ W[2] ⊆ · · · which are defined as the closure of certain parameterized problems under parameterized reductions. There is strong theoretical evidence that parameterized problems that are hard for classes W[i] are not fixed-parameter tractable.

3 Backdoors

Before we introduce the notion of backdoors to the ASP domain we review it in the domain where it originates from.

Satisfiability Backdoors Let F be a CNF formula and X a set of atoms. The following is obvious from the definitions:

• (∗) F is satisfiable if and only if Fτ is satisfiable for at least one truth assignment τ ∈ ta(X).

This observation leads to the definition of a strong backdoor relative to a class C of polynomially solvable CNF formulas: a set X of atoms is a strong C-backdoor of a CNF formula F if Fτ ∈ C for all truth assignments τ ∈ ta(X). Assume that the satisfiability of formulas F ∈ C of size ‖F‖ = n can be decided in time O(nc ). Then we can decide the satisfiability of an arbitrary formula F for which we know a strong Cbackdoor of size k in time O(2k nc ) which is efficient as long as k remains small.

Before we can use the strong backdoor we need to find it first. For most reasonable target classes C the detection of a strong backdoor of size at most k is NP-hard if k is part of the input. However, as we are interested in finding small backdoors, it makes sense to parameterized the backdoor search by k and consider the parameterized complexity of backdoor detection. Indeed, with respect to the classes of Horn CNF formulas and 2-CNF formulas, the detection of strong backdoors of size ≤ k is fixed-parameter tractable [Nishimura et al., 2004; Samer and Szeider, 2009]. For other target classes (clustering formulas and renamable Horn formulas) the detection of deletion backdoors (a subclass of strong backdoors) of size at most k is fixed-parameter tractable [Nishimura et al., 2007; Razgon and O'Sullivan, 2008].

ASP Backdoors In order to translate the notion of backdoors to the domain of ASP, we first need to come up with a suitable concept of a reduction with respect to a truth assignment. The following is a natural definition which generalizes a concept of Gottlob et al. [2002].

Definition 1. Let P be a program, X a set of atoms, and τ ∈ ta(X). The truth assignment reduct of P under τ is the logic program Pτ obtained from P by

1. removing all rules r with H(r) ∩ τ -1 (1) ̸= ∅ or H(r) ⊆ X;
2. removing all rules r with B+(r) ∩ τ -1 (0) ̸= ∅;
3. removing all rules r with B-(r) ∩ τ -1 (1) ̸= ∅;
4. removing from the heads and bodies of the remaining rules all literals v, ¬v with v ∈ X.

Definition 2. 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 truth assignments τ ∈ ta(X).

Example 1. Consider the program P = {s ← w; u ← s, q; r ← w, s; t ← ¬r; q ← ¬s, u; w ← ¬r, u}. The set X = {r, s} is a strong Horn-backdoor since all four truth assignment reducts Pr=0,s=0 = P00 = {t ←; q ← u; w ← u}, P01 = {u ← q; t ←; w ← u}, P10 = {q ← u}, and P11 = {u ← q} are Horn programs.

A direct equivalence similar to (∗) does not hold for ASP, even if we consider the most basic problem CONSISTENCY. Take for example the program P = { x ← ¬x; y ←} and the set X = {x}. Both reducts Px=0 = { y } and Px=1 = { y } have answer sets, but P has no answer set. However, we can show a somewhat weaker asymmetric variant of (∗), where we can map each answer set of P to an answer set of Pτ for some τ ∈ ta(X). This is made precise by the following definition and lemma.

Definition 3. Let P be a program and X a set of atoms. We define AS(P, X) =

Lemma 1. AS(P) ⊆ AS(P,X) holds for every program P and every set X of atoms.

Owing to space restrictions we omit the proof which can be found in a longer version of this paper at http://arxiv.org/abs/ 1104.2788.

In view of Lemma 1, we can compute AS(P) by (i) computing AS(Pτ) for all τ ∈ ta(X) and (ii) checking for each M ∈ AS(Pτ) whether it gives rise to an answer-set of P. Observe that in particular any constraint contained in P is removed in the truth assignment reduct Pτ but is then considered in step (ii). If we can compute AS(Pτ) in polynomial time for each τ ∈ ta(X), we have a fixed-parameter algorithm for computing AS(P) for parameter k = |X|. This consideration leads to the following definition and result.

Definition 4. A class C of programs is enumerable if for each P ∈ C we can compute AS(P) in polynomial time.

For any class C of programs we denote by C ∗ the class containing all programs that belong to C after removal of tautological rules and constraints. It is easy to see that whenever C is enumerable, then so is C ∗ . Note that all classes considered in this paper are enumerable.

Theorem 1. Let C be an enumerable class of programs. Problems CONSISTENCY, CREDULOUS and SKEPTICAL REASONING, AS COUNTING and AS ENUMERATION are all fixed-parameter tractable when parameterized by the size of a smallest strong C backdoor, assuming that the backdoor is given as an input.

Proof. Let X be the given backdoor. Since we have |AS(P,X)| ≤ 2|X| , we can solve each listed problem by making at most 2|X| polynomial checks.

If we know that each program in C has at most one answer set, and P has a strong C-backdoor of size k, then we can conclude that P has at most 2k answer sets. Thus, we obtain an upper bound on the number of answer sets of P by computing a small strong C-backdoor of P .

Example 2. We consider program P of Example 1. The answer sets of Pτ are AS(P00) = {{t}}, AS(P01) = {{t}}, AS(P10) = {∅}, and AS(P11) = {∅} for τ ∈ ta({r, s}). AS(P, X) = {{t}, {t, s}, {r}, {r, s}}, and since only {t} ∈ AS(P, X) is an answer set of P , we obtain AS(P ) = {{t}}.

Deletion Backdoors We will see below that the following variant of strong backdoors is often useful. For a program P and a set X of atoms we define P-X as the program obtained from P by deleting all atoms contained in X from all the rules (heads and bodies) of P .

Definition 5. Let C be a class of programs. A set X of atoms is a deletion C-backdoor of a program P if P -X ∈ C.

In general, not every strong C-backdoor is a deletion C-backdoor, and not every deletion C-backdoor is a strong C-backdoor. We call C to be rule induced if for each P ∈ C, P ′ ⊆ P implies P ′ ∈ C. Note that many natural classes of programs (and all classes considered in this paper) are rule induced.

Proposition 1. If C is rule induced, then every deletion C-backdoor is a strong C-backdoor.

Proof. The statement follows from the fact that Pτ ⊆ P -X for every τ ∈ ta(X) and every program P .

Backdoor Detection In order to use Theorem 1 we need to find the backdoor first. Each class C of programs gives rise to the following parameterized problem: STRONG CBACKDOOR DETECTION: given a program P and an integer k, find a strong C-backdoor X of P of size at most k, or report that such X does not exist. We also consider the problem DELETION C-BACKDOOR DETECTION, defined similarly (which is in some cases easier to solve).

4 Target Class Horn

We first consider the important case Horn∗ as the target class for backdoors. It is well known that normal Horn programs have a unique answer set and this set can be found in linear time [Dowling and Gallier, 1984], hence Horn and Horn∗ are enumerable. The following lemma shows that Horn∗ is particularly well suited as a target class.

Lemma 2. A set X is a strong Horn∗ -backdoor of a program P if and only it is a deletion Horn∗ -backdoor of P .

Owing to space restrictions we omit the proof.

Theorem 2. STRONG Horn∗ -BACKDOOR DETECTION is fixed-parameter tractable in k. In fact, given a program P with n atoms we can find a strong Horn∗ -backdoor of size ≤ k in time O(1.2738k + kn) or decide that no such backdoor exists.

Proof. (Sketch) Let G be the undirected graph defined on the set of atoms of the given program P , where two atoms x, y are joined by an edge if and only if P contains a non-tautological rule r with x, y ∈ H(r) or x ∈ H(r) and y ∈ B-(r). Now it is easy to see that a set X ⊆ at(P) is a vertex cover of G if and only if X is a deletion Horn∗ -backdoor of P. A vertex cover of size ≤ k, if it exists, can be found in time O(1.2738k + kn) [Chen et al., 2006]. The theorem follows by Lemma 2.

For instance, the undirected graph G of the program P of Example 1 consists of the two paths (w, r, t) and (s, q). Then {r, s} is a vertex cover of G. We observe easily that there exists no vertex cover of size 1. Thus {r, s} is a smallest strong Horn∗ -backdoor of P .

Ben-Eliyahu [1996] showed that evaluation of normal logic programs is fixed-parameter tractable in (i) the number of atoms that appear in negative rule bodies, and (ii) the total number of non-Horn rules. It is not difficult to see that both numbers are greater or equal to the size of a smallest strong Horn∗ -backdoor, and so entailed by our approach.

5 Acyclicity-Based Target Classes

There are two causes for a program to have a large number of answer sets: (i) disjunctions in the heads of rules, and (ii) certain cyclic dependencies between rules. Disallowing both causes yields so-called stratified programs [Gelfond and Lifschitz, 1988]. In the following we will study backdoor detection for various classes of stratified programs. We define the classes by requiring normality and acyclicity (the absence of certain types cycles). In order to define acyclicity we associate with each normal program P its directed dependency graph DP [Apt et al., 1988], and its undirected dependency graph UP [Gottlob et al., 2002]. DP has as vertices the atoms of P and a directed edge (x, y) between any two atoms x, y for which there is a rule r ∈ P with x ∈ H(r) and y ∈ B(r); if there is a rule r ∈ P with x ∈ H(r) and y ∈ B-(r), then the edge (x, y) is called a negative edge. UP is obtained from Dp by replacing each negative edge e = (x, y) with two undirected edges {x, ve}, {ve, y} where ve is a new negative vertex, and by replacing each remaining directed edge (u, v) with an undirected edge {u, v}. By a directed cycle of P we mean a directed cycle in DP , by an undirected cycle of P we mean an undirected cycle in UP . Figure 1 visualizes DP and Up of the program P of Example 1. A directed (undirected) cycle is bad if it contains a negative edge (a negative vertex), otherwise it is good. Various classes of programs arise by requiring the programs to have no directed bad cycles (DBC-Acyc), no undirected bad cycles (BC-Acyc), no directed cycles (DCAcyc), and no undirected cycles (C-Acyc). DBC-Acyc, the largest class among the considered classes, is exactly the class Strat of stratified programs [Apt et al., 1988].

For instance in the program P of Example 1, (r,v(w,r),w, r) is an undirected cycle, (u, q, u) is a directed cycle, (s,vq,s, q, u, s) is an undirected bad cycle, and (w, r, w) is a directed bad cycle (see Figure 1).

In order to compare the size of backdoors for the various classes, we need to compare the classes themselves (evidently, if C ⊊ C ′ , then every strong (deletion) C ′ -backdoor is also a strong (deletion) C ′ -backdoor, but not necessarily the other way around). By definition we have DC-Acyc ⊊ DBC-Acyc and C-Acyc ⊊ BC-Acyc ⊊ DBC-Acyc; it is easy to see that the inclusions are proper. However, contrary to what one expects, C-Acyc ̸⊆ DC-Acyc, which can be seen by considering the program P0 = {x ← y, y ← x}, hence C-Acyc and DC-Acyc are incomparable. Requiring that a program has no directed cycles but may have directed good cycles of length 2 (as in P0) gives rise to the class DC2-Acyc, which generalizes both classes C-Acyc and DC-Acyc. The diagram in Figure 2 shows the relationship between the various program classes.

Theorem 3. For each class C ∈ {C-Acyc, BC-Acyc, DCAcyc, DC2-Acyc, Strat} the problem STRONG C-BACKDOOR DETECTION is W[2]-hard and therefore unlikely to be fixed-parameter tractable.

Proof. (Sketch)We give a reduction from theW[2]-complete problem HITTING SET [Downey and Fellows, 1999]. An instance of this problem is a pair (S, k) where S = {S1, . . . , Sm} is a family of sets and k is an integer (the parameter). The question is whether there exists a set H of size at most k which intersects with all the Si; such H is a hitting set. We construct a program P as follows. As atoms we take the elements of X = ⋃mi=1 Si and new atoms aji and bji for 1 ≤ i ≤ m, 1 ≤ j ≤ k + 1. For each 1 ≤ i ≤ m and 1 ≤ j ≤ k + 1 we take two rules rj i , sji where H(rj i ) = {aji }, B-(rj i ) = Si, B+(rj i ) = Si ∪ {bji }; H(sji ) = {bji }, B-(sji ) = {aji }, B+(sji ) = ∅. The result now follows by showing that S has a hitting set of size ≤ k if and only if P has a strong C-backdoor of size ≤ k where C is any of the classes mentioned.

For DC-Acyc, DC2-Acyc, and Strat we can avoid the use of tautological rules in the reduction and so strengthen Theorem 3 (it would be interesting to know if this is also possible for the remaining two classes mentioned in Theorem 3).

The W[2]-hardness results suggest to relax the considered problems and to look for deletion backdoors: Which of the classes mentioned in Theorem 3 admit fixed-parameter tractable detection of deletion backdoors? Using very recent results from fixed-parameter algorithmics we can answer this question positively for all considered classes except for Strat whose complexity remains open.

Theorem 4. For each class C ∈ {C-Acyc, BC-Acyc, DCAcyc, DC2-Acyc} the problem DELETION C ∗ -BACKDOOR DETECTION is fixed-parameter tractable.

Proof. (1) DELETIONC-Acyc-BACKDOOR DETECTION can be solved by solving the FEEDBACK VERTEX SET (FVS) problem for Up, which is well-known to be FPT [Downey and Fellows, 1999], this was already observed by Gottlob et al. [2002]. (2) DELETION DC-Acyc-BACKDOOR DETECTION is equivalent to the DIRECTED FVS problem on Dp. The parameterized complexity of DIRECTED FVS remained open for many years and was recently shown FPT by Chen et al. [2008] with a break-through result. (3) DELETION BC-Acyc-BACKDOOR DETECTION can be solved by solving the EDGE SUBSET FVS problem, where only cycles need to be covered that contain an edge from a given set S. This problem was recently shown FPT by Cygan et al. [2010] and Kawarabayashi and Kobayashi [2010]. (4) Finally, the problem DELETION DC2-Acyc-BACKDOOR DETECTION can be solved by finding a feedback vertex set in a mixed graph (a graph containing directed and undirected edges), as we can replace a good cycle on two edges by one undirected edge. FVS FOR MIXED GRAPHS was recently shown FPT by Bonsma and Lokshtanov [2010].

The classes mentioned in Theorem 3 are rule-induced. Hence we can use this theorem to strengthen the fixedparameter tractability result of Theorem 1 by dropping the assumption that the backdoor is given.

The considered classes can be generalized by taking the parity of the number of negative edges on bad cycles into account. In recent research Fichte [2011] generalized the tractability results of Lin and Zhao [2004] by considering backdoors with respect to such parity classes.

6 Theoretical Comparison of Parameters

In this section we compare ASP parameters in terms of their generality.

Jakl et al. [2009] applied the graph parameter treewidth to ASP and showed that the main reasoning problems for ASP are fixed-parameter tractable by the treewidth of the incidence graph of the program. The incidence graph of a program P is the bipartite graph on the rules and atoms of P, where a rule and an atom are joined by an edge if and only if the atom occurs in the rule. It turns out that incidence treewidth is incomparable with backdoor size for various target classes considered.

Theorem 5. Let C ∈ {Horn, C-Acyc, DC-Acyc, DC2Acyc, BC-Acyc, Strat}. There are programs whose incidence graphs have constant treewidth but require arbitrarily large strong and deletion C-backdoors, and there are programs where the converse prevails.

Proof. (Sketch) Clearly each of the considered classes contains programs of arbitrary high treewidth of the incidence graph. Conversely, we consider a program P /∈ C. We denote by nP the program consisting of the union of n atom-disjoint copies of P. By basic properties of treewidth it follows that the treewidth of the incidence graph of P equals to that of nP , however, smallest C-backdoors are of size ≥ n.

The treewidth approach is based on dynamic programming which is of high space complexity and therefore only practical for instances of treewidth below 10 [Jakl et al., 2009]. The backdoor approach is more space efficient since for each partial truth assignment τ ∈ ta(X) of a backdoor X, the computations of AS(Pτ ) and the corresponding elements of AS(Pτ ) can be carried out independently.

One might ask whether it makes sense to consider restrictions on the treewidth of the undirected dependency graph, defined above. However, this restriction does not yield tractability, as the reduction of [Eiter and Gottlob, 1995] produces programs with undirected dependency graphs of treewidth 2.

7 Empirical Comparison of Parameters

We have determined the size of smallest backdoors for various programs, including structured real-world instances and random instances. The results are summarized in Table 1. It is known that so-called tight programs are closely related to SAT [Lin and Zhao, 2003]. The QueensEqTest instances and two of the Daimler-Chrysler instances are tight, all other instances considered are not tight. For pragmatic reasons we have used Horn∗ as the target class as smallest backdoors are easy to compute, even for large inputs. Our experimental results indicate that structured instances have smaller backdoors than random instances. It also seems that random instances with higher density have larger backdoors.

We have conducted a second series of experiments on random instances where we have analyzed how much we gain by considering the more general acyclicity-based target classes instead of Horn. It appears that smallest deletion Horn∗ -backdoors are indeed significantly larger than deletion backdoors for acyclicity-based target classes. The distinction between directed and undirected cycles seems to have a significant effect on the backdoor size, whereas the distinction between good and bad cycles seems to be less significant. However these results are not fully conclusive as the considered programs were rather small.

8 Conclusion

We have introduced the backdoor approach to the domain of propositional answer-set programming. The backdoor approach allows to augment a known tractable class and makes the efficient solving methods for the tractable class generally applicable. Our approach makes recent results in fixedparameter algorithmics applicable to nonmonotonic reasoning. The comparison results show that the parameters based on backdoor size are incomparable with treewidth and therefore provide fixed-parameter tractability for programs that are hard for the treewidth approach.

The results and concepts of this paper give rise to several interesting research questions. For instance, it would be interesting to consider backdoors for target classes that contain programs with an exponential number of answer-sets, but where the set of all answer-sets can be succinctly represented. A simple example is the class of programs that consist of independent components of bounded size. Other questions are concerned with alternative ways of using backdoors. For instance, by means of "backdoor trees" [Samer and Szeider, 2008] one can avoid the consideration of all 2k partial assignments of the backdoor and thus make the backdoor approach feasible for programs with larger backdoors. A further use of backdoors that seems worth exploring is the control of heuristics of ASP solvers.