Disjunctive answer set programming (ASP) is an important framework for declarative modeling and problem solving, where the computational 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 di erent approaches have been applied to nd tractable fragments of programs, in particular, 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 ndings for the problem WMMSAT and show several novel xed-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.
Answer set programming (ASP) is an important framework for declarative
modelling and problem solving [
consist of a combination of various structural properties, have also been established
for problems such as weighted minimal model satis ability (WMMSat) [
Contribution. In this paper, we study the computational complexity of
propositional disjunctive ASP using the framework of parameterized complexity
theory [
2
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 rules to sets of atoms such that for a rule r we have H(r) = fa1; : : : ; alg (the head of r), B+(r) = fb1; : : : ; bng (the positive body of r), and B (r) = fc1; : : : ; cmg (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 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 write occP (a) := f r 2 P : a 2 at(r) g. 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 negation-free if B (r) = ;, r is normal if jH(r)j 1, r is a constraint (integrity rule) if jH(r)j = 0, r is Horn if it is negation-free and normal or a constraint, r is de nite 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 de nite 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 2 P 0 there is some rule r 2 P with H(r0) H(r), B+(r0) B+(r), B (r0) B (r). Let P 2 Horn, we write Constr(P ) for the set of constrains of P and DH(P ) =
rules as Pr = f r 2 P : H(r) 6= ; g and constraints as Pc = P nPr. We occasionally
write ? as a head if H(r) = ;. If B+(r)[B (r) = ;, we simply write H(r) instead
of H(r) ;; ;. We also write H(P ) := Sr2P H(r), B (P ) := Sr2P B (r). A
set M of atoms satis es a rule r if (H(r) [ B (r)) \ M 6= ; or B+(r) n M 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 [
size at most k. k-Brave Reasoning: Given a program P , an atom a 2 at(P ), and an integer k decide whether P has an answer set M of size at most k such that a 2 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:
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 satis ability. A clause is a nite set of literals, a CNF formula is a nite set of clauses. The set of variables of a CNF formula F is denoted by var (F ). A truth assignment is a mapping : X ! f0; 1g de ned for a set X U of atoms. By 2X we denote the set of all truth assignments : X ! f0; 1g. For x 2 X we de ne (:x) = 1 (x). The truth assignment reduct of a CNF formula F with respect to 2 2X is the CNF formula F obtained from F by rst 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 . satis es F if F = ;, and F is satis able if it is satis ed 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;g F , which is obviously not satis able. The problem Weighted Minimal
WSat is de ned as follows. Weighted Satisfiability (WSat ): Given A
of cardinality jM j k.
Parameterized Complexity. We give some basic background on parameterized
complexity. For more detailed information we refer to other sources [
maxsize nH rH rB+ rB cB+ cB maxocc r r H B+ rB k jjPcjj H B+ rB r r c B+ cB
H B+ rB r r an instance (I; k) 2 N we call I the main part and k the parameter. L is xed-parameter tractable if there exist a computable function f and a constant c such that we can decide whether (I; k) 2 L in time O(f (k)kIkc) where kIk denotes the size of I. FPT is the class of all xed-parameter tractable decision problems. The Weft Hierarchy consists of parameterized complexity classes
problems under parameterized reductions. There is strong theoretical evidence
that parameterized problems that are hard for classes W[i] are not xed-parameter
tractable. It is well-known that di erent variations of WSat can be used to
de ne the W-hierarchy (see, e.g., the work of Flum and Grohe [
nite 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 2 we have (I; k) 2 L
if and only if r(I; k) = (I0; k0) 2 L0 such that k0 g(k) for a xed 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 [
maxsizeH maxsizerH;B maxsizerB maxsizecB jjPcjj maxoccrH;B #non-Hornr k
De nition 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 description, let P be a program and X fH; B+; B g where H, B+, and B are mappings de ned as in Section 2. We omit P if the program is clear from the context. Further, let atX;r := [f2X f (r), #atX := j [r2P atX;rj, maxsizerX := max Pf2X;r02P jf (r0)j : jH(r0)j > 0 , maxsizecX := max Pf2X;r02P jf (r0)j : jH(r0)j = 0 , #non-Hornr := jfr0 : r0 2 P; r0 not Horngj, and maxoccrX := max i : a 2 at(P ); i = Pf2X; r02P; jH(r0)j>0 jf a : a 2 f (r0) gj . 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 programming, 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 parameters 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 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 e ect the other considered parameters.
Observation 2 Let p be an ASP parameter, C be a parameterized complexity class, and L 2 fConsistency, Brave Reasoningg, 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 2 C when parameterized by p and p does not depend on k, then the problem L 2 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.
Next, we will see that if a decision problem in AspProblems is xed-parameter tractable when parameterized by some xed parameter p and p is not a ected by restricting the solution size to at most k, then the corresponding problem for answer sets of size at most k is xed-parameter tractable when parameterized by the combined parameter p + k where k is the size of the answer set. P [ f ? :c1;k+1 g [ f ci;j ci+1;j ; ai; ci;j ci+1;j : 1 k + 1 g [ f cn+1;0 > g where a1; : : : ; an are the atoms of P .
De nition 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 := i n; 0 j Proposition 4 (?3) Let p be a counter-preserving ASP parameter, C be a parameterized complexity class, L 2 fConsistency, Brave Reasoningg, 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
Observation 5 (?) For each problem L 2 fk-Consistency, k-Brave Reasoningg, we have L is xed-parameter tractable when parameterized by at least one of the following parameters (i) #atH or (ii) maxsizeH + jPrj. 3 Statements whose proofs are omitted due to space limitations are marked with \(?)".
to WMMSat.
Theorem 6 (?) Let L 2 fk-Consistency; k-Brave Reasoningg. Then, L is xed-parameter tractable when parameterized by at least one of the following combined parameters 1. k + maxsizer 2. #non-HornrH+;Bm,axosrizerH;B .
is xed-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 [
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 := fa0 j a 2 Xg. In Step (i) we set: P mmod := H(r); B (r) 0 B+(r) : r 2 P , P subset := a0 a : a 2 at(P ) , P supset := a a0 : a 2 at(P ) , and P * := P 0 [ P supset. Then in Step (ii) we construct a WMMSat instance by ' := Fmmod ^ Fsubset and := Fsupset. Where every 2 fmmod; subset; supsetg we construct formula F* from P * as follows: 0 v[a]A 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. { mmaaxxssiizzeerrHH;;BB : Let d 2 be some integer. Moreover, assume that 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 jM j k. By construction of FP', M at(P ) is an answer set of P if and only if VM[M0 is a minimal model of FP and VM[M0 is a model of Fsupset. Hence, we have jVM[M0 j 2k by construction. Consequently, the maximum weight of the minimal model of FP is bounded by 2k. { #non-Hornr: Let h 0 be some integer and assume that #non-Hornr h.
rule is not Horn if and only if the corresponding clause in Fmin is not Horn.
Theorem 7 (?) Let L 2 fk-Consistency; k-Brave Reasoningg. Then L is xed-parameter tractable when parameterized by at least one of the following combined parameters
+ maxsizecB + #atB , and 21.. k#+atB#+at+B+#+nomn-aHxoorcncrrH+;BmaxsizecB + #atB .
version, namely, when the input is restricted to programs from NF+Cons.
restricted to programs from NF+Cons [
Lemma 8 Let L 2 fk-Consistency; k-Brave Reasoningg. If the input of L is restricted to programs from NF+Cons, then L is xedparameter tractable when parameterized by at least one of the following combined parameters (i) k + #atB+ + maxoccrH;B + maxsizecB , and (ii) #atB+ + #non-Hornr + maxsizecB .
Proposition 9 ([
parameters considered in the statement. Let (P; k) be an instance of k-Consistency where P 2 NF+Cons. We construct an instance ('; ; k) of WMMSat as follows. The variables of the CNF formulas ' and will consist of a variable for each atom of P . Then for a rule r 2 P we let C(r) := f xa : a 2 H(r) g [ f :xa : a 2 B+(r) g. Further, we de ne ' := f C(r) : r 2 P; H(r) 6= ; g and := f C(r) : r 2 P; H(r) = ; g. ' 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: { 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 occurrences 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+).
work [
De nition 10 Let P be a program, M at(P ), and N at(P ) n 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 B+(r) \ N 6= ;; (iii) removing all rules r with B (r) \ M 6= ;; (iv) removing from the heads and negative bodies of the remaining rules all atoms a with a 2 N ; (v) removing from the positive bodies of the remaining rules all atoms a with a 2 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 in Lemma 8. Let (P; `) be an instance of k-Consistency, N := [r2P;H(r)6=; atB ;r , 2 2N , M1 := 1(1), and M0 := 1(0). Further, we de ne P Mc1;M0 := f ? :a : a 2
P [ ] := PM;N [ P Mc;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 satis es 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.
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.
representation for atoms in the head (see the concept of SSMs in [
Proposition 11 (?) Let p be an ASP parameter. If the problem Enum is xedparameter tractable when parameterized by p, then for every problem L 2 fk-Consistency, k-Brave Reasoningg, L is xed-parameter tractable when parameterized by p.
problems in k-AspProblems .
Corollary 12 Let C be an enumerable class of normal programs. Every problem L 2 fk-Consistency, k-Brave Reasoningg is xed-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 [
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 2 fk-Consistency; k-Brave Reasoningg. Then L is paraNP-hard when parameterized by the following parameters 1. maxsizerH;B+;B
and
+ maxsizerH;B + maxsizerB+ + #atB+ + maxsizecB + jjPcjj, + maxsizerH;B
+ maxsizerB+ + #atB .
Let L 2 fk-Consistency; k-Brave Reasoningg. Then L is W[
Let L 2 fk-Consistency; k-Brave Reasoningg. Then L is W[
already been established by Truszczynski [
no clauses without positive literals, since otherwise we can shift such clauses into without a ecting 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 2 f0; 1g we de ne Ci := f ai : xi 2 C; x 2 var (C) g where a is a fresh atom and a0 = :a and a1 = a. Now, let P min := f C1 C0 : C 2 ' g and P cons := f :C1; C0 : C 2 g and we de ne a program P := P min [ P cons.
also a model of if and only if P has an answer set of size at most k.
reduction from an instance ('; k) of WSat for Statement 4. Note that WSat is
well known to be W[
Finally, it remains to observe that our reduction preserves the parameters:
{ k: directly corresponds to the maximum weight of a minimal model (k)
{{ mmaaxxssiizzeerrHH;;BB+;:Bdir:edcitrleyctcloyrrceosrproenspdosntdostthoe tmheaxmimauximmupmosictliavuescelasuizsee isnize' i(nd)'
(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
occurrences of a variable in ' (p)
4 Note that this has also no e ect to the results we use for WMMSat, since the
parameters used in the proofs for WMMSat remain una ected (it only e ects d and
d , however, there d is already bounded by v ; see the proofs of Theorems 16 and
17 in [
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 [
We have identi ed several natural structural parameters of ASP instances (as summarized in Table 1) and carried out a ne-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 xed-parameter tractability result of the considered problems when parameterized 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 remaining 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.