A Multiparametric View on Answer Set Programming∗ Johannes K. Fichte1 , Martin Kronegger2 , and Stefan Woltran1 lastname@dbai.tuwien.ac.at 1 TU Wien, Vienna, Austria lastname@dbai.tuwien.ac.at 2 Johannes Kepler University Linz, Austria martin.kronegger@jku.at Abstract. Disjunctive answer set programming (ASP) is an important framework for declarative modeling and problem solving, where the com- putational complexity of basic decision problems like consistency (deciding whether a program has an answer set) is located on the second level of the polynomial hierarchy. During the last decades different approaches have been applied to find tractable fragments of programs, in particu- lar, also using parameterized complexity. However, the full potential of parameterized complexity has not been unlocked since only one or very few parameters have been considered at once. In this paper, we consider several natural parameters for the consistency problem of disjunctive ASP. In addition, we also take the size of the answer set into account; a restriction that is particularly interesting for applications requiring small solutions. Previous work on parameterizing the consistency problem by the size of answer sets yielded mostly negative results. In contrast, we start from recent findings for the problem WMMSAT and show several novel fixed-parameter tractability (fpt) results based on combinations of parameters. Moreover, we establish a variety of hardness results (paraNP, W[2], and W[1]-hardness) to assess tightness of our combined parameters. 1 Introduction Answer set programming (ASP) is an important framework for declarative modelling and problem solving [15]. In propositional ASP, a problem is described in terms of a logic program consisting of rules over propositional atoms. Answer sets, which are sometimes also referred as stable models, are then the solutions to such a logic program. Computational problems for disjunctive, propositional ASP such as the consistency problem (deciding whether a program has a solution) are complete for the second level of the Polynomial Hierarchy [4]. However, classical worst case complexity does not rule out efficient solutions if a certain (hidden) ∗ The work has been supported by the Austrian Science Fund (FWF), Grant Y698 and S11408-N23. The first author is also affiliated with the Institute of Computer Science and Computational Science at University of Potsdam, Germany. The second author is also affiliated with TU Wien, Austria. 2 Fichte et al. structure is present in an input instance. On that score, several restrictions on input programs have been identified in the literature that make the consistency problem tractable or NP-complete, for a detailed trichotomy see [16]. A prominent approach to analyze and understand computational complexity incorporating the existence of certain hidden structure is to use the framework of parameterized complexity [3]. The main idea of parameterized complexity is to fix a certain structural property (the parameter) of a problem instance and to consider the computational complexity of the problem in dependency of the parameter. Various parameterized complexity analyzes have been carried out for ASP problems, see e.g., [6,7,14,8]. In particular, Lonc and Truszczyński [14] have considered the parameterized complexity of the consistency problem parameterized by a given integer k, when the input is restricted to normal (i.e., disjunction-free) programs and when then answer sets are allowed to be of size exactly k, or at most k, or at least k, and established various hardness results. In AI more fine-grained complexity analysis, where hidden structure may consist of a combination of various structural properties, have also been established for problems such as weighted minimal model satisfiability (WMMSat) [13] and planning [12]. So far, there has been no rigorous study of disjunctive ASP when considering various combinations of structural properties. Contribution. In this paper, we study the computational complexity of propo- sitional disjunctive ASP using the framework of parameterized complexity the- ory [1,3]. We consider several combinations of structural properties at once. Since the problem WMMSat and ASP are quite related in terms of their problem questions, we start from results by Lackner and Pfandler [13] for WMMSat, transform several of these results to ASP, point out limitations where the methods used for WMMSat are insufficient and require to take additional structural properties into account, and finally extend them accordingly. Furthermore, we incorporate results by Lonc and Truszczyński [14] and Truszczyński [16]. This allows us to draw a detailed map for various combined ASP parameters. Main Contributions. Our main contributions can be summarized as follows: 1. We provide a parameterized complexity analysis for fundamental ASP prob- lems that respects various combinations of natural ASP parameters, which allows us to draw a detailed map for a multivariate view on ASP complexity. 2. We study main ASP problems that also take the size of the answer set into account. Such a restriction is particularly interesting for applications that require small solutions. 2 Preliminaries Let U be a universe of propositional atoms. A literal is an atom a ∈ U or its nega- tion ¬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. Further, let H, B + , and B − map A Multiparametric View on Answer Set Programming 3 rules to sets of atoms such that for a rule r we have H(r) = {a1 , . . . , al } (the head of r), B + (r) = {b1 , . . . , bn } (the positive body of r), and B − (r) = {c1 , . . . , cm } (negative body of r). In addition to the traditional representation of a rule above, we sometimes also write H(r) ← B + (r), ¬B − (r), and H(r) ← B + (r) instead of H(r) ← B + (r), ¬∅. We denote the sets of atoms occurring in S 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 write occP (a) := { r ∈ P : a ∈ at(r) }. We denote the number P rules of P by |P+| = |{ r : r−∈ P }|. The size kP k of a program P is defined as of r∈P |H(r)| + |B (r)| + |B (r)|. A rule r is negation-free if B − (r) = ∅, r is normal if |H(r)| ≤ 1, r is a constraint (integrity rule) if |H(r)| = 0, r is Horn if it is negation-free and normal or a constraint, r is definite Horn if it is Horn and not a constraint, r is tautological if B + (r) ∩ (H(r) ∪ B − (r)) 6= ∅, and non-tautological if it is not tautological, r is positive-body-free if B + (r) = ∅, and r is a fact if r is definite and (B + (r) ∪ B − (r)) = ∅. 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. NF+Cons refers to the class of all programs where negation-free rules and arbitrary constraint rules (may also contain negative atoms) are allowed. 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 ∈ P 0 there is some rule r ∈ P with H(r0 ) ⊆ H(r), B + (r0 ) ⊆ B + (r), B − (r0 ) ⊆ B − (r). Let P ∈ Horn, we write Constr(P ) for the set of constrains of P and DH(P ) = P \ Constr(P ). We also identify the parts of a program P consisting of proper rules as Pr = { r ∈ P : H(r) 6= ∅ } and constraints as Pc = P \Pr . We occasionally write ⊥ as a head if H(r) = ∅. If B + (r)∪BS− (r) = ∅, we simply write S H(r) instead of H(r) ← ∅, ∅. We also write H(P ) := r∈P H(r), B − (P ) := r∈P B − (r). A set M of atoms satisfies a rule r if (H(r) ∪ B − (r)) ∩ M 6= ∅ or B + (r) \ M = 6 ∅. 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 6= ∅ and then removing all ¬z where z ∈ B − (r) from the remaining rules r [11]. 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 and for some integer k ≥ 0 by ASk (P ) the set of all answer sets of P of size at most k. It is well known that normal Horn programs have a unique answer set or no answer set and that this set can be found in linear time. Note that every definite Horn program P has a unique minimal model which equals the least model LM (P ) [10]. Dowling and Gallier [2] have established a linear-time algorithm for testing the satisfiability of propositional Horn formulas which easily extends to Horn programs. In this paper, we consider the following ASP problems. k-Consistency: Given a program P and an integer k decide whether P has an answer set of size at most k. k-Brave Reasoning: Given a program P , an atom a ∈ at(P ), and an integer k decide whether P has an answer set M of size at most k such that a ∈ M . We denote by k-AspProblems the family of the reasoning problems k-Consistency and k-Brave Reasoning. Further, we use the problem k-Enum: 4 Fichte et al. Given a program P and an integer k list all answer sets of size at most k of P . We refer to the problems as Consistency, Brave Reasoning, and Enum, respectively, if the integer k can be arbitrarily large. We denote by AspProblems the family of the reasoning problems Consistency and Brave Reasoning. 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. The set of variables of a CNF formula F is denoted by var (F ). A truth assignment is a mapping τ : X → {0, 1} defined for a set X ⊆ U of atoms. By 2X we denote the set of all truth assignments τ : X → {0, 1}. For x ∈ X we define τ (¬x) = 1 − τ (x). The truth assignment reduct of a CNF formula F with respect to τ ∈ 2X 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 if it is satisfied by some τ . Note that if a formula F contains some clause C of only positive literals and we have a truth assignment τ that sets all literals occurring in C to 0, then we obtain {∅} ⊆ Fτ , which is obviously not satisfiable. The problem Weighted Minimal Model Satisfiability (WMMSat) asks to decide given two propositional (CNF) formulas ϕ and π and an integer k whether there is a minimal model M of ϕ that sets at most k variables to true and also satisfies π. The problem WSat≤ is defined as follows. Weighted Satisfiability (WSat≤ ): Given A CNF formula F and some integer k decide whether F has a model M ⊆ var (F ) of cardinality |M | ≤ k. Parameterized Complexity. We give some basic background on parameterized complexity. For more detailed information we refer to other sources [1,3]. A parameterized problem L is a subset of Σ ∗ × N for some finite alphabet Σ. For k maximum size of an answer set maxsizerH,B + ,B − maximum size of a non-constraint rule maxsizerH,B − maximum size of the head and negative body of a rule maxsizerH,B + maximum size of the head and positive body of a rule maxsizeH maximum size of the head of a rule maxsizerB + maximum size of the positive body of a non-constraint rule maxsizerB − maximum size of the negative body of a rule maxsizecB − maximum size of the negative body of a constraint #non-Hornr number of non-(definite Horn) rules maxoccrH,B − maximum number of occurrences of a variable in Pr when only the head and negative-body occurrences are counted maxoccrB + maximum number of occurrences of a variable in Pr when only the positive-body occurrences are counted #atH number of atoms that occur in the head #atB + number of atoms that occur in the positive body #atB − number of atoms that occur in the negative body ||Pc || the total number of variable occurrences in Pc Table 1: List and informal description of the considered parameters. A Multiparametric View on Answer Set Programming 5 #at maxsize maxocc k ||Pc || ·rH ·B + ·B − nH ·rH ·rB + ·rB − ·cB + ·cB − ·rH ·rB + ·rB − Result 7 ∈ FPT 7 7 7 ∈ FPT 7 7 7 ∈ FPT 7 7 7 7 7 7 ∈ FPT 7 7 7 7 7 open 7 7 7 7 ∈ FPT 7 7 7 open 7 7 7 7 7 7 7 W[1]-h 7 7 7 7 7 7 W[2]-h 7 7 7 7 W[2]-h 7 7 7 7 7 W[2]-h 7 7 7 7 7 7 W[2]-h 7 7 7 7 7 7 paraNP-h 7 7 7 7 paraNP-h k ||Pc || ·rH ·rB + ·rB − nH ·rH ·rB + ·rB − ·cB + ·cB − ·rH ·rB + ·rB − Result Table 2: Summary of multi-parametric complexity results for k-Consistency. For each line the marked columns indicate according to the header a combined ASP parameter. Membership or hardness results are stated in the last column. 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)kIkc ) where kIk 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. It is well-known that different variations of WSat≤ can be used to define the W-hierarchy (see, e.g., the work of Flum and Grohe [9]). Let L ⊆ Σ ∗ × N and L0 ⊆ Σ 0∗ × N be two parameterized problems for some finite alphabets Σ and Σ 0 . An fpt-reduction r from L to L0 is a many-to-one reduction from Σ ∗ × N to Σ 0∗ × N such that for all I ∈ Σ ∗ we have (I, k) ∈ L if and only if r(I, k) = (I 0 , k 0 ) ∈ L0 such that k 0 ≤ 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)kIkc ) where kIk denotes the size of I [9]. Thus, an fpt-reduction is, in particular, an fpt-algorithm. It is easy to see that the class FPT is closed under fpt-reductions. We would like to note that the theory of fixed-parameter intractability is based on fpt-reductions [9]. The parameterized complexity of the problems WSat≤ and WMMSat has been studied in the work of Lackner and Pfandler [13]. Several hardness and tractability results for combined parameter turn out to be useful to show hardness and tractability results for the considered ASP problems. 6 Fichte et al. #atB + #atH maxsizecB − maxoccrH,B − maxsizerB + maxsizeH ||Pc || #non-Hornr maxsizerH,B + ,B − maxsizerH,B − k maxsizerH,B + maxsizerB − Fig. 1: Domination Graph (relationship between parameters). Let x and y be parameters. There is an arc x → y whenever x  y holds. 2.1 Considered Parameters In this section, we introduce a list of ASP-parameters, which mainly originate from earlier work for WMMSat, for our parameterized complexity analysis. In particular, we are interested in parameter combinations. First, we first give a definition what we mean by an ASP parameter. Definition 1 An ASP parameter is a function p that assigns to every program P some non-negative integer p(P ). Let p and q be ASP parameters. We say that p dominates q (in symbols p  q) if there is a computable function f such that p(P ) ≤ f (q(P )) holds for all programs P . Table 1 lists the considered parameters, which can be computed in polynomial time, and their intuitive description. For a more formal de- scription, let P be a program and X ⊆ {H, B + , B − } where H, B + , and B − are mappings defined as in Section 2. We omit P if the pro- gram is clear from the context. Further,  P let atX,r := ∪f ∈X f (r), #atX := | ∪r∈P atX,r |, maxsizerX := max 0 f ∈X,r ∈P |f (r 0 )| : |H(r0 )| > 0 , r maxsizecX := max 0 0  P f ∈X,r 0 ∈P |f (r )| : |H(r )| = 0 , #non-Horn := 0 0 0 r |{r : r ∈ P, r not Horn}|, and maxoccX := max i : a ∈ at(P ), i = 0 P f ∈X, r 0 ∈P, |H(r 0 )|>0 |{ a : a ∈ f (r ) }| . Figure 1 depicts the relationship in terms of domination of parameters that are useful for our results. Note, that this list is not complete. 2.2 Relationship of AspProblems and k-AspProblems Recent research in parameterized complexity in the setting of answer set pro- gramming, has mainly focused on consistency or reasoning problems, which allow arbitrarily large answer sets. However, we focus on ASP problems that also take the size of the answer set into account. In the following, we explain and summarize connections between both versions. We observe that if the param- eters do not depend on the maximum size of an answer set state conditions, we can trivially extend known membership and hardness results for problems in AspProblems to the respective problem in k-AspProblems . In other words, the A Multiparametric View on Answer Set Programming 7 problem k-Consistency is at least as hard as Consistency. Finally, we state how to extend known results for Consistency using standard counters that do not effect the other considered parameters. Observation 2 Let p be an ASP parameter, C be a parameterized complexity class, and L ∈ {Consistency, Brave Reasoning}, and k-L its corresponding decision problem k-Consistency or k-Brave Reasoning, respectively, in other words, k-L decides the question of L when restricted to answer sets of size at most k. 1. If the problem k-L ∈ C when parameterized by p and p does not depend on k, then the problem L ∈ C under fpt-reductions when parameterized by p. 2. Further, if problem L is C-hard when parameterized by p and p does not depend on k, then the problem k-L is C-hard under fpt-reductions when parameterized by p. Note that the restriction “p does not depend on k” is quite weak as in that case both problems coincide. Next, we will see that if a decision problem in AspProblems is fixed-parameter tractable when parameterized by some fixed parameter p and p is not affected by restricting the solution size to at most k, then the corresponding problem for answer sets of size at most k is fixed-parameter tractable when parameterized by the combined parameter p + k where k is the size of the answer set. Definition 3 Let p be an ASP parameter. Then we call p counter-preserving if p(P ) = f (p(Pk )) for some computable function f , an integer k and Pk0 := P ∪ { ⊥ ← ¬c1,k+1 } ∪ { ci,j ← ci+1,j , ai ; ci,j ← ci+1,j : 1 ≤ i ≤ n, 0 ≤ j ≤ k + 1 } ∪ { cn+1,0 ← > } where a1 , . . . , an are the atoms of P . Proposition 4 (?3 ) Let p be a counter-preserving ASP parameter, C be a pa- rameterized complexity class, L ∈ {Consistency, Brave Reasoning}, and k-L its corresponding decision problem k-Consistency or k-Brave Reasoning, respectively. If the problem L belongs to class C when parameterized by p, then the problem k-L belongs to class C under fpt-reductions when parameterized by p. 3 Membership Results In this section, we present for ASP reasoning problems several novel fixed- parameter tractability results, which are summarized in Table 2. We first observe that parameterizing in the number of head atoms already yields fixed-parameter tractability. Observation 5 (?) For each problem L ∈ {k-Consistency, k-Brave Reasoning}, we have L is fixed-parameter tractable when parameterized by at least one of the following parameters (i) #atH or (ii) maxsizeH + |Pr |. 3 Statements whose proofs are omitted due to space limitations are marked with “(?)”. 8 Fichte et al. We now proceed to two tractability results that can be obtained by a reduction to WMMSat. Theorem 6 (?) Let L ∈ {k-Consistency, k-Brave Reasoning}. Then, L is fixed-parameter tractable when parameterized by at least one of the following combined parameters 1. k + maxsizerH,B − , or 2. #non-Hornr + maxsizerH,B − . Proof (Idea). The main idea of the proof is a reduction to WMMSat. WMMSat is fixed-parameter tractable when parameterized by at least one of the following combined parameters (i) k+ maximum positive clause size, or (ii) maximum positive clause size + number of non-Horn clauses [13]. Our reduction runs in linear time and preserves all necessary parameters. The reduction consists of two reductions: (i) from P we construct in linear time programs P mmod ∪ P subset and P supset , and (ii) from P mmod ∪ P subset and P supset we construct in linear time an instance of WMMSat. For a set X, we let (X)0 := 0 {a0 | a ∈ X}. In Step (i) we set: P mmod := H(r), B − (r) ← B + (r) : r ∈ P ,  P subset := a0 ← a : a ∈ at(P ) , P supset := a ← a0 : a ∈ at(P ) , and  P * := P 0 ∪ P supset . Then in Step (ii) we construct a WMMSat instance by ϕ := Fmmod ∧ Fsubset and π := Fsupset . Where every ∗ ∈ {mmod, subset, supset} we construct formula F* from P * as follows:   ^ _ _ F* :=  ¬v[a] ∨ v[a] r∈P * a∈B + (r) a∈H(r) Then, the formula Fmmod encodes P mmod and expresses that an atom a belongs to the minimal model if and only if the atom occurs either in the head or the negative body of a rule. Fsubset encodes P subset and expresses that whenever an atom a belongs to the minimal model then also its copy a0 belongs to the minimal model. Finally, Fsupset encodes P supset and “simulates the GL reduct” and expresses that whenever the copy a0 of atom a belongs to the model, also its originating atom a has to be in the model. It remains to observe that the reduction preserves all parameters. – maxsizerH,B − : Let d ≥ 2 be some integer. Moreover, assume that maxsizerH,B − ≤ d, by construction of FP’ each clause in Fsubset contains at most 1 positive literal and the maximum number of positive literals in a clause of Fmin is at most d. Moreover, each clause in Fsupset contains at most 1 positive literal. Hence, the maximum number of positive literals in each clause of the resulting formulas is at most d. – k: Let k ≥ 0 be some integer. Moreover, assume that |M | ≤ k. By construction of FP’ , M ⊆ at(P ) is an answer set of P if and only if VM ∪M 0 is a minimal model of FP and VM ∪M 0 is a model of Fsupset . Hence, we have |VM ∪M 0 | ≤ 2k by construction. Consequently, the maximum weight of the minimal model of FP is bounded by 2k. A Multiparametric View on Answer Set Programming 9 – #non-Hornr : Let h ≥ 0 be some integer and assume that #non-Hornr ≤ h. By construction Fsubset and Fsupset contain only Horn clauses. Moreover, a rule is not Horn if and only if the corresponding clause in Fmin is not Horn. Hence, h provides an upper bound for the number of non-Horn clauses of Fmin and thus of FP’ and Fsupset . We obtain membership for k-Brave Reasoning by the same arguments. Now we are ready to show new fixed-parameter tractability results. Theorem 7 (?) Let L ∈ {k-Consistency, k-Brave Reasoning}. Then L is fixed-parameter tractable when parameterized by at least one of the following combined parameters 1. k + #atB + + maxoccrH,B − + maxsizecB − + #atB − , and 2. #atB + + #non-Hornr + maxsizecB − + #atB − . In order to prove the theorem, we first establish the statement for a restricted version, namely, when the input is restricted to programs from NF+Cons. In fact, the problem Consistency is already Σ2P -complete when the input is restricted to programs from NF+Cons [16]. By definition, such programs have an empty negative body for non-constraint rules and hence the parameter #atB − is of value 0. Lemma 8 Let L ∈ {k-Consistency, k-Brave Reasoning}. If the in- put of L is restricted to programs from NF+Cons, then L is fixed- parameter tractable when parameterized by at least one of the follow- ing combined parameters (i) k + #atB + + maxoccrH,B − + maxsizecB − , and (ii) #atB + + #non-Hornr + maxsizecB − . To proof the lemma we need the following results. Proposition 9 ([13]) WMMSat is fixed-parameter tractable when parameter- ized by at least one of the following combined parameters (i) k + v − + p + d+π , and (ii) v − + h + d+π , where k is the maximum weight of the minimal model, h is the number of non-Horn clauses, p is the maximum number of positive occurrences of a variable in π, v − is the number of variables that occur as negative literals in π or in π, and d+ π maximum positive clause size in π. Proof of Lemma 8 (Idea). We give a reduction to WMMSat, which preserves all parameters considered in the statement. Let (P, k) be an instance of k-Consis- tency where P ∈ NF+Cons. We construct an instance (ϕ, π, k) of WMMSat as follows. The variables of the CNF formulas ϕ and π will consist of a vari- able for each atom of P . Then for a rule r ∈ P we let C(r) := { xa : a ∈ H(r) } ∪ { ¬xa : a ∈ B + (r) }. Further, we define ϕ := { C(r) : r ∈ P, H(r) 6= ∅ } and π := { C(r) : r ∈ P, H(r) = ∅ }. ϕ has a minimal model M of size at most k such that M is also a model of π if and only if P has an answer set of size at most k. Next, we observe that our reduction preserves the parameters: 10 Fichte et al. – k: directly corresponds to the maximum weight of a minimal model (k) – maxsizerH,B − : directly corresponds to the maximum positive clause size in ϕ (d+ ) – maxsizerB + : directly corresponds to the maximum negative clause size in ϕ (d− ) – #non-Hornr : directly corresponds to the number of non-horn clauses (h) – maxoccrH,B − : directly corresponds to the maximum number of positive oc- currences of a variable in ϕ (p) – #atB + : directly corresponds to the number of variables that occur as negative literals in ϕ or in π (v − ) – maxsizecB − : directly corresponds to the maximum positive clause size in π (d+π ). Before we are able to prove the theorem, we extend concepts from earlier work [7] and define the concept of a truth assignment reduct under sets M and N of atoms. Definition 10 Let P be a program, M ⊆ at(P ), and N ⊆ at(P ) \ M . The truth assignment reduct of P under (M, N ) is the logic program PM,N obtained from P by (i) removing all rules r with H(r) ∩ M = 6 ∅; (ii) removing all rules r with 6 ∅; (iii) removing all rules r with B − (r) ∩ M 6= ∅; (iv) removing B + (r) ∩ N = from the heads and negative bodies of the remaining rules all atoms a with a ∈ N ; (v) removing from the positive bodies of the remaining rules all atoms a with a ∈ M. Proof of Theorem 7 (Sketch). We give an fpt-reduct that constructs 2(#atB− +1) many programs that can be solved in fpt-time using results established inLemma 8. Let (P, `) be an instance of k-Consistency, N := ∪r∈P,H(r)6=∅ atB − ,r , τ ∈ 2N , M1 := τ −1 (1), and M0 := τ −1 (0). Further, we define PM c 1 ,M0 := { ⊥ ← ¬a : a ∈ M1 } ∪ { ← a : a ∈ M0 }, use PM1 ,M0 as defined in Definition 10, and let c P [τ ] := PM,N ∪ PM,N . Then, the program P has an answer set of size at most k if and only if at least one program P [τ ] has an answer set of size at most k. In this way, we give a reduction to 2(#atB− +1) many instances of k-Consistency that consists of 2(#atB− +1) many subprograms by constructing “partial” GL reducts under a set M1 , which consists of atoms that we have set to true, and a set M0 , which consists of atoms that we have set to false, together with constraints that enforce that any minimal model M of the GL reduct satisfies that atoms in M1 belong to M and atoms in M0 do not belong to M . It remains to observe that our reduction preserves the parameters. The reduction in the proof of Theorem 8 states that ASP and WMMSat are very related with respect to the considered reasoning problems. However, answer sets additionally require minimality with respect to the GL reduct of the given program. In consequence, we need to parameterize additionally in the number of negative atoms that occur in non-constraint rules of the given program. Particularly, we do not have a direct counterpart of the concept of a compact A Multiparametric View on Answer Set Programming 11 representation for atoms in the head (see the concept of SSMs in [13]) if the positive body is empty and the negative body is not empty. The next result states that a fixed-parameter tractability result for the Enum problem directly extends to a fixed-parameter tractability result with the same parameter for our considered ASP reasoning problems, where we are interested only in answer sets of size at most k. Proposition 11 (?) Let p be an ASP parameter. If the problem Enum is fixed- parameter tractable when parameterized by p, then for every problem L ∈ {k-Con- sistency, k-Brave Reasoning}, L is fixed-parameter tractable when parame- terized by p. Consequently, known results for backdoors [7] immediately apply to our problems in k-AspProblems . Corollary 12 Let C be an enumerable class of normal programs. Every prob- lem L ∈ {k-Consistency, k-Brave Reasoning} is fixed-parameter tractable when parameterized by the size of a strong C-backdoor. Remark 13 We would like to mention that the parameter incidence or primal treewidth [5] immediately provides fixed-parameter tractability for our problems in k-AspProblems , since the dynamic programming algorithms as presented in previous work can be trivially modified such that the computation stops at size at most k. 4 Hardness Results In this section, we present as already stated in Table 2 for ASP reasoning problems several hardness results. Observe that hardness for a combination of parameters trivially implies hardness for any subset of these parameters. Whereas the fpt results in the previous section imply fpt results for any superset of these parameters. Theorem 14 (?) Let L ∈ {k-Consistency, k-Brave Reasoning}. Then L is paraNP-hard when parameterized by the following parameters 1. maxsizerH,B + ,B − + maxsizerH,B − + maxsizerB + + #atB + + maxsizecB − + ||Pc ||, and 2. maxsizerH,B + ,B − + maxsizerH,B − + maxsizerB + + #atB − . Let L ∈ {k-Consistency, k-Brave Reasoning}. Then L is W[2]-hard when parameterized by the following parameters 3. k + maxsizerH,B + + maxoccrB + + maxsizecB + + maxsizecB − , 4. k + maxsizerB − + maxsizecB + + maxsizecB − , 5. k + maxsizerB + + #atB + + maxsizecB − + ||Pc ||, and 6. k + maxsizerB + + #non-Hornr + maxoccrH,B − + #atB + . Let L ∈ {k-Consistency, k-Brave Reasoning}. Then L is W[1]-hard when parameterized by the following parameters 7. k + maxsizerB + + #non-Hornr + maxoccrH,B − + maxsizecB − + ||Pc ||. 12 Fichte et al. Proof (Sketch). We proceed by a reduction from the problem WMMSat for Statements (1) and (5)–(7) and WSat for Statement (4). Statement (2) has already been established by Truszczyński [16]. Statement (3) is an immediate consequence from a reduction established by Lonc and Truszczyński [14][The. 4.4]. Note that according to results by Lackner and Pfandler [13] WMMSat is paraNP-hard when parameterized by the following combined parameter: (i) d + d+ + d− + p + v − + d+ π + ||π||; WMMSat is W[2]-hard when parame- terized by the following combined parameters (ii) k + d− + v − + d+ π + ||π|| and (iii) k + d− + h + p + v − ; WMMSat is W[1]-hard when parameterized by the following combined parameters (iv) k + d− + h + p + d+ π + ||π|| where k is the maximum weight of the minimal model, d is the maximum clause size, d+ , d− is the maximum positive or negative clause size, respectively in ϕ, h is the number of non-horn clauses in ϕ, b is the minimum size of strong Horn backdoor set in ϕ, p is the maximum number of positive occurrences of a variable in ϕ, v + , v − is the number of variables that occur as positive or negative literals in ϕ or in π, respectively, d+ π maximum positive clause size in π, ||π|| is the length of π, i.e., the total number of variable occurrences in π. Let (ϕ, π, k) be an instance of WMMSat. We assume w.l.o.g. that ϕ contains no clauses without positive literals, since otherwise we can shift such clauses into π without affecting the size of the models and hence the minimality.4 We now construct an instance (P, k) of k-Consistency as follows. For a clause C and i ∈ {0, 1} we define C i := { ai : xi ∈ C, x ∈ var (C) } where a is a fresh atom and a0 = ¬a and a1 = a. Now, let P min := { C 1 ← C 0 : C ∈ ϕ } and P cons := { ← ¬C 1 , C 0 : C ∈ π } and we define a program P := P min ∪ P cons . Next, we show that ϕ has a minimal model M of size at most k such that M is also a model of π if and only if P has an answer set of size at most k. Next, we can employ the construction and proofs from above to establish a reduction from an instance (ϕ, k) of WSat for Statement 4. Note that WSat is well known to be W[2]-hard, e.g., [3]. Therefore, observe that ϕ has a model M of size at most k if and only if P min has an answer set of size at most k. Finally, it remains to observe that our reduction preserves the parameters: – k: directly corresponds to the maximum weight of a minimal model (k) – maxsizerH,B + ,B − : directly corresponds to the maximum clause size in ϕ (d) – maxsizerH,B − : directly corresponds to the maximum positive clause size in ϕ (d+ ) – maxsizerB + : directly corresponds to the maximum negative clause size in ϕ (d− ) – #non-Hornr : directly corresponds to the number of non-horn clauses (h) – maxoccrH,B − : directly corresponds to the maximum number of positive oc- currences of a variable in ϕ (p) 4 Note that this has also no effect to the results we use for WMMSat, since the parameters used in the proofs for WMMSat remain unaffected (it only effects d and d− , however, there d− is already bounded by v − ; see the proofs of Theorems 16 and 17 in [13]). A Multiparametric View on Answer Set Programming 13 – #atB + : directly corresponds to the number of variables that occur as negative literals in ϕ or in π (v − ) – maxsizecB − : directly corresponds to the maximum positive clause size in π (d+π) – ||Pc ||: directly corresponds to the length of π, i.e., the total number of variable occurrences in π (kπk) The runtime follows from the results by Lackner and Pfandler [13] for WMMSat as stated above. Remark 15 Note that our reductions make certain concepts of parameters in the setting of answer set programming such as fpt-results for acyclicity-based backdoors [6] or bounded treewidth [5] directly accessible to WMMSat. 5 Conclusion We have identified several natural structural parameters of ASP instances (as summarized in Table 1) and carried out a fine-grained complexity analysis of the main reasoning problems in answer set programming when parameterized by various combinations of these parameters (see Table 2 for an overview). Our study also considers the parameterized complexity of the main ASP reasoning problems while taking the size of the answer set into account. Such a restriction is particularly interesting for applications that require small solutions. We have presented various hardness and membership results (see Table 1). Every hardness result of the reasoning problems when parameterized by a combined parameter also holds for any parameter that consists of a subset of the combination. Further, every fixed-parameter tractability result of the considered problems when param- eterized by a combined parameter also holds for any extension of the parameter by additional structural properties (superset of the parameter combination). In that way, we have improved on the theoretical understanding by providing a novel multi parametric view on the parameterized complexity of ASP, which allows us to draw a detailed map for various combined ASP parameters. Future Work. The results and concepts of this paper give rise to several research questions. For instance, it would be interesting to close the gap for the remain- ing parameter combinations. Therefore, we need to identify important corner cases. An interesting further research direction is to study how the parameters empirically distribute among ASP instances from the last ASP competitions, in particular, in random versus structured instances. Additionally, it would be interesting to conduct a parameterized analysis as well as considering multiple parameters in the non-ground setting. References 1. Cygan, M., Fomin, F.V., Kowalik, L., Lokshtanov, D., Dániel Marx, M.P., Pilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer Verlag (2015) 14 Fichte et al. 2. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming 1(3), 267–284 (1984) 3. Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. Texts in Computer Science, Springer Verlag, London, UK (2013) 4. Eiter, T., Gottlob, G.: On the computational cost of disjunctive logic programming: Propositional case. Ann. Math. Artif. Intell. 15(3–4), 289–323 (1995) 5. Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: Answer set solving with bounded treewidth revisited. In: Balduccini, M., Janhunen, T. (eds.) Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’17) (2017), to appear. Extended version https://arxiv.org/pdf/1702. 02890.pdf. 6. Fichte, J.K., Szeider, S.: Backdoors to normality for disjunctive logic programs. ACM Trans. Comput. Log. 17(1), 7 (Dec 2015) 7. Fichte, J.K., Szeider, S.: Backdoors to tractable answer-set programming. Artificial Intelligence 220(0), 64–103 (2015) 8. Fichte, J.K., Szeider, S.: Backdoor trees for answer set programming. In: Bogaerts, B., Harrison, A. (eds.) Informal Proceedings of the 10th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP’17) (2017), to appear. 9. Flum, J., Grohe, M.: Parameterized Complexity Theory, Theoretical Computer Science, vol. XIV. Springer Verlag, Berlin (2006) 10. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) Proceedings of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP’88). vol. 2, pp. 1070–1080. MIT Press, Seattle, WA, USA (August 1988) 11. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Comput. 9(3/4), 365–386 (1991) 12. Kronegger, M., Pfandler, A., Pichler, R.: Parameterized complexity of optimal planning: A detailed map. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13). pp. 954–961. The AAAI Press, Beijing, China (Aug 2013) 13. Lackner, M., Pfandler, A.: Fixed-parameter algorithms for finding minimal models. In: Eiter, T., McIlraith, S. (eds.) Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR’12). pp. 85–95. The AAAI Press, Rome, Italy (Jun 2012) 14. Lonc, Z., Truszczyński, M.: Fixed-parameter complexity of semantics for logic programs. ACM Trans. Comput. Log. 4(1), 91–119 (Jan 2003), http://doi.acm. org/10.1145/601775.601779 15. Marek, V.W., Truszczyński, M.: Stable models and an alternative logic programming paradigm. In: Apt, K.R., Marek, V.W., Truszczyński, M., Warren, D.S. (eds.) The Logic Programming Paradigm: a 25-Year Perspective, pp. 375–398. Artificial Intelligence, Springer Verlag (1999) 16. Truszczyński, M.: Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs. Theory Pract. Log. Program. 11, 881–904 (11 2011)