=Paper=
{{Paper
|id=Vol-1868/p8
|storemode=property
|title=A Multiparametric View on Answer Set
Programming
|pdfUrl=https://ceur-ws.org/Vol-1868/p8.pdf
|volume=Vol-1868
|authors=Johannes K. Fichte,Martin Kronegger,Stefan Woltran
|dblpUrl=https://dblp.org/rec/conf/lpnmr/FichteKW17
}}
==A Multiparametric View on Answer Set
Programming==
https://ceur-ws.org/Vol-1868/p8.pdf
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)