Fixed-parameter complexity of semantics for logic programs.
A decision problem is called parameterized if its input is a pair of strings. One of these strings is referred to as a parameter. The following problem is an example of a parameterized decision problem with k serving as a parameter: given a propositional logic program P and a nonnegative integer k, decide whether P has a stable model of size no more than k. Parameterized problems that are NP-complete often become solvable in polynomial time if the parameter is fixed. The problem to decide whether a program P has a stable model of size no more than k, where k is fixed and not a part of input, can be solved in time O(mnk), where m is the size of P and n is the number of atoms in P. Thus, this problem is in the class P. However, algorithms with the running time given by a polynomial of order k are not satisfactory even for relatively small values of k.The key question then is whether significantly better algorithms (with the degree of the polynomial not dependent on exist. To tackle it, we use the framework of fixed-parameter complexity. We establish the fixed-parameter complexity for several parameterized decision problems involving models, supported models, and stable models of logic programs. We also establish the fixed-parameter complexity for variants of these problems resulting from restricting attention to definite Horn programs and to purely negative programs. Most of the problems considered in the paper have high fixed-parameter complexity. Thus, it is unlikely that fixing bounds on models (supported models, stable models) will lead to fast algorithms to decide the existence of such models.
Introduction
In this paper we study the complexity of parameterized decision problems concerning
models, supported models and stable models of logic programs. In our
investigations, we use the framework of the fixed-parameter complexity introduced
by Downey and Fellows [DF97]. This framework was previously used to
study the problem of the existence of stable models of logic programs in [Tru01].
Our present work extends results obtained there. First, in addition to the class of
all finite propositional logic programs, we consider its two important subclasses:
the class of Horn programs and the class of purely negative programs. Second,
in addition to stable models of logic programs, we also study supported models
and arbitrary models.
A decision problem is parameterized if its inputs are pairs of items. The second
item in a pair is referred to as a parameter. The problems to decide, given a logic
program P and an integer k, whether P has a model, supported model or a stable
model, respectively, with at most k atoms are examples of parameterized decision
problems. These problems are NP-complete. However, fixing k (that is, k is no
longer regarded as a part of input) makes each of the problems simpler. They
become solvable in polynomial time. The following straightforward algorithm
works: for every subset M ' At(P ) of cardinality at most k, check whether M
On leave from Faculty of Mathematics and Information Science, Warsaw University
of Technology.
?? The second author was partially supported by the NSF grants CDA-9502645, IRI-
9619233 and EPS-9874764.
is a model, supported model or stable model, respectively, of P . The check can
be implemented to run in linear time in the size of the program. Since there are
sets to be tested, the overall running time of this algorithm is O(mn k ),
where m is the size of the input program P and n is the number of atoms in P .
The problem is that algorithms with running times given by O(mn k ) are not
practical even for quite small values of k. The question then arises whether better
algorithms can be found, for instance, algorithms whose running-time estimate
would be given by a polynomial of the order that does not depend on k. Such
algorithms, if they existed, could be practical for a wide range of values of k and
could find applications in computing stable models of logic programs.
This question is the subject of our work. We also consider similar questions
concerning related problems of deciding the existence of models, supported models
and stable models of cardinality exactly k and at least k. We refer to all
these problems as small-bound problems since k, when fixed, can be regarded
as "small". In addition, we study problems of existence of models, supported
models and stable models of cardinality at most jAt(P )j \Gamma k, exactly jAt(P
and at least jAt(P )j \Gamma k. We refer to these problems as large-bound problems,
since jAt(P )j \Gamma k, for a fixed k, can be informally thought of as "large".
We address these questions using the framework of fixed-parameter complexity
[DF97]. Most of our results are negative. They provide strong evidence that
for many parameterized problems considered in the paper there are no algorithms
whose running time could be estimated by a polynomial of order independent of
k.
Formally, a parameterized decision problem is a set L ' \Sigma   \Theta \Sigma   , where
\Sigma is a fixed alphabet. By selecting a concrete value ff 2 \Sigma   of the parameter,
a parameterized decision problem L gives rise to an associated fixed-parameter
problem Lg.
A parameterized problem L ' \Sigma   \Theta \Sigma   is fixed-parameter tractable if there
exist a constant t, an integer function f and an algorithm A such that A determines
whether (x; y) 2 L in time f(jyj)jxj t (jzj stands for the length of a string
z 2 \Sigma   ). We denote the class of fixed-parameter tractable problems by FPT.
Clearly, if a parameterized problem L is in FPT, then each of the associated
fixed-parameter problems L y is solvable in polynomial time by an algorithm
whose exponent does not depend on the value of the parameter y. Parameterized
problems that are not fixed-parameter tractable are called fixed-parameter
intractable.
To study and compare the complexity of parameterized problems Downey
and Fellows proposed the following notion of fixed-parameter reducibility (or,
simply, reducibility).
Definition 1. A parameterized problem L can be reduced to a parameterized
problem L 0 if there exist a constant p, an integer function q, and an algorithm
A such that:
1. A assigns to each instance (x; y) of L an instance
2. A runs in time O(q(jyj)jxj p ),
3. x 0 depends upon x and y, and y 0 depends upon y only,
4. (x; y) 2 L if and only if
We will use this notion of reducibility throughout the paper. If for two parameterized
problems L 1 and L 2 , L 1 can be reduced to L 2 and conversely, we say
that L 1 and L 2 are fixed-parameter equivalent or, simply, equivalent.
Downey and Fellows [DF97] defined a hierarchy of complexity classes called
the W hierarchy:
The classes W[t] can be described in terms of problems that are complete for
them (a problem D is complete for a complexity class E if D 2 E and every
problem in this class can be reduced to D). Let us call a Boolean formula t-
normalized if it is a conjunction-of-disjunctions-of-conjunctions . of literals,
with t being the number of conjunctions-of, disjunctions-of expressions in this
definition. For example, 2-normalized formulas are conjunctions of disjunctions
of literals. Thus, the class of 2-normalized formulas is precisely the class of CNF
formulas. We define the weighted t-normalized satisfiability problem as:
Given a t-normalized formula \Phi and a non-negative integer k, decide
whether there is a model of \Phi with exactly k atoms (or, alternatively, decide
whether there is a satisfying valuation for \Phi which assigns the logical value
true to exactly k atoms).
Downey and Fellows show that for every t - 2, the problem WS(t) is complete
for the class W[t]. They also show that a restricted version of the problem WS(2):
Given a 2-normalized formula \Phi with each clause consisting of at most
two literals, and an integer k, decide whether there is a model of \Phi with
exactly k atoms
is complete for the class W[1]. There is strong evidence suggesting that all the
implications in (1) are proper. Thus, proving that a parameterized problem is
complete for a class W[t], t - 1, is a strong indication that the problem is not
fixed-parameter tractable.
As we stated earlier, in the paper we study the complexity of parameterized
problems related to logic programming. All these problems ask whether an input
program P has a model, supported model or a stable model satisfying some
cardinality constraints involving another input parameter, an integer k. They
can be categorized into two general families: small-bound problems and large-
bound problems. In the formal definitions given below, C denotes a class of logic
programs, D represents a class of models of interest and \Delta stands for one of the
three arithmetic relations: "-", "=" and "-".
Given a logic program P from class C and an integer k, decide whether
P has a model M from class D such that jM j \Delta k.
Given a logic program P from class C and an integer k, decide whether
P has a model M from class D such that (jAt(P )j \Gamma
In the paper, we consider three classes of programs: the class of Horn programs
H, the class of purely negative programs N , and the class of all programs
A. We also consider three classes of models: the class of all models M, the class
of supported models SP and the class of stable models ST .
Thus, for example, the problem SP- (N ) asks whether a purely negative logic
program P has a supported model M with no more than k atoms (jM j - k). The
problem ST 0
asks whether a logic program P (with no syntactic restrictions)
has a stable model M in which at most k atoms are false (jAt(P
Similarly, the problem M 0
- (H) asks whether a Horn program P has a model M
in which at least k atoms are false (jAt(P
In the three examples given above and, in general, for all problems D \Delta (C)
and D 0
(C), the input instance consists of a logic program P from the class C
and of an integer k. We will regard these problems as parameterized with k.
Fixing k (that is, k is no longer a part of input but an element of the problem
description) leads to the fixed-parameter versions of these problems. We will
denote them D \Delta (C;
In the paper, for all but three problems D \Delta (C) and D 0
(C), we establish their
fixed-parameter complexities. Our results are summarized in Tables 1 - 3.

Table

1. The complexities of the problems D- (C) and D 0
(C).
In

Table

1, we list the complexities of all problems in which
bound problems of this type ask about the existence of models of a program P
that contain at least k atoms. Large-bound problems in this group are concerned
with the existence of models that contain at most jAt(P )j \Gamma k atoms (the number
of false atoms in these models is at least k). From the point of view of the fixed-
parameter complexity, these problems are not very interesting. Several of them
remain NP-complete even when k is fixed. In other words, fixing k does not
simplify them enough to make them tractable. For this reason, all the entries in

Table

1, listing the complexity as NP-complete (denoted by NP-c in the table),
refer to fixed-parameter versions D- (C;
of problems D- (C) and
(C). The problem M 0
is NP-complete for every fixed k - 1. All other
fixed-parameter problems in Table 1 that are marked NP-complete are NP-complete
for every value k - 0.
On the other hand, many problems D- (C) and D 0
- (C) are "easy". They are
fixed-parameter tractable in a strong sense. They can be solved in polynomial
time even without fixing k. This is indicated by marking the corresponding entries
in

Table

(for the class P) rather than with FPT. There is only one
exception, the problem M 0
(N ), which is W[1]-complete.
Small-bound problems for the cases when or "-" can be viewed as
problems of deciding the existence of "small" models (that is, models containing
exactly k or at most k atoms). The fixed-parameter complexities of these
problems are summarized in Table 2.
in W[2]

Table

2. The complexities of the problem of computing small models (small-bound
problems, the cases of
The problems involving the class of all purely negative programs and the
class of all programs are W[2]-complete. This is a strong indication that they are
fixed-parameter intractable. All problems of the form D- (H) are fixed-parameter
tractable. In fact, they are solvable in polynomial time even without fixing the
parameter k. We indicate this by marking the corresponding entries with P.
Similarly, the problem ST = (H) of deciding whether a Horn logic program P has
a stable model of size exactly k is in P. However, perhaps somewhat surprisingly,
the remaining two problems involving Horn logic programs and are
harder. We proved that the problem M= (H) is W[1]-complete and that the
problem SP= (H) is W[1]-hard. Thus, they most likely are not fixed-parameter
tractable. We also showed that the problem SP= (H) is in the class W[2]. The
exact fixed-parameter complexity of SP= (H) remains unresolved.
Large-bound problems for the cases when or "-" can be viewed
as problems of deciding the existence of "large" models, that is, models with
a small number of false atoms - equal to k or less than or equal to k. The
fixed-parameter complexities of these problems are summarized in Table 3.

Table

3. The complexities of the problems of computing large models (large-bound
problems, the cases of
The problems specified by concerning the existence of models
are in P. Similarly, the problems specified by involving Horn
programs are solvable in polynomial time. Lastly, the problem ST 0
= (H) is in
as well. These problems are in P even without fixing k and eliminating it
from input. All other problems in this group have higher complexity and, in
all likelihood, are fixed-parameter intractable. One of the problems, M 0
W[1]-complete. Most of the remaining problems are W[2]-complete. Surprisingly,
some problems are even harder. Three problems concerning supported models are
W[3]-complete. For two problems involving stable models, ST 0
we could only prove that they are W[3]-hard. For these two problems we did not
succeed in establishing any upper bound on their fixed-parameter complexities.
The study of fixed-parameter tractability of problems occurring in the area
of nonmonotonic reasoning is a relatively new research topic. The only two other
papers we are aware of are [Tru01] and [GSS99]. The first of these two papers
provided a direct motivation for our work here (we discussed it earlier). In the
second one, the authors focused on parameters describing structural properties
of programs. They showed that under some choices of the parameters decision
problems for nonmonotonic reasoning become fixed-parameter tractable.
Our results concerning computing stable and supported models for logic programs
are mostly negative. Parameterizing basic decision problems by constraining
the size of models of interest does not lead (in most cases) to fixed-parameter
tractability.
There are, however, several interesting aspects to our work. First, we identified
some problems that are W[3]-complete or W[3]-hard. Relatively few problems
from these classes were known up to now [DF97]. Second, in the context
of the polynomial hierarchy, there is no distinction between the problem
of existence of models of specified sizes of clausal propositional theories and
similar problems concerning models, supported models and stable models of
logic programs. All these problems are NP-complete. However, when we look
at the complexity of these problems in a more detailed way, from the perspective
of fixed-parameter complexity, the equivalence is lost. Some problems are
W[3]-hard, while problems concerning existence of models of 2-normalized formulas
are W[2]-complete or easier. Third, our results show that in the context of
fixed-parameter tractability, several problems involving models and supported
models are hard even for the class of Horn programs. Finally, our work leaves
three problems unresolved. While we obtained some bounds for the problems
(A), we did not succeed in establishing their precise
fixed-parameter complexities.
The rest of our paper is organized as follows. In the next section, we review
relevant concepts in logic programming. After that, we present several useful
fixed-parameter complexity results for problems of the existence of models for
propositional theories of certain special types. In the last section we give proofs
of some of our complexity results.
Preliminaries
In the paper, we consider only the propositional case. A logic program clause
(or rule) is any expression r of the form
where are propositional atoms. We call the atom p the head of r and
we denote it by h(r). Further, we call the set of atoms fq
the body of r and we denote it by b(r). We distinguish the positive body of r,
in symbols), and the negative body of r, fs
in symbols).
A logic program is a collection of clauses. For a logic program P , by At(P )
we denote the set of atoms that appear in P . If every clause in a logic program
P has an empty negative body, we call P a Horn program. If every clause in P
has an empty positive body, we call P a purely negative program.
A clause r, given by (2), has a propositional interpretation as an implication
Given a logic program P , by a propositional interpretation of P we mean the
propositional formula
We say that a set of atoms M is a model of a clause (2) if M is a (propositional)
model of the clause pr(r). As usual, atoms in M are interpreted as true, all
other atoms are interpreted as false. A set of atoms M ' At(P ) is a model of a
program P if it is a model of the formula pr(P ). We emphasize the requirement
In this paper, given a program P , we are interested only in the
truth values of atoms that actually occur in P .
It is well known that every Horn program P has a least model (with respect
to set inclusion). We will denote this model by lm(P ).
Let P be a logic program. Following [Cla78], for every atom p 2 At(P ) we
define a propositional formula comp(p) by
where
f:s:
If for an atom p 2 At(P ) there are no rules with p in the head, we get an empty
disjunction in the definition of comp(p), which we interpret as a contradiction.
We define the program completion [Cla78] of P as the propositional theory
A set of atoms M ' At(P ) is a supported model of P if it is a model of the
completion of P . It is easy to see that if p does not appear as the head of a rule
in P , p is false in every supported model of P . It is also easy to see that each
supported model of a program P is a model of P (the converse is not true in
general).
Given a logic program P and a set of atoms M , we define the reduct of P
with respect to M (P M , in symbols) to be the logic program obtained from P
by
1. removing from P each clause r such that call such clauses
blocked by M ),
2. removing all negated atoms from the bodies of all the rules that remain (that
is, those rules that are not blocked by M ).
The reduct P M is a Horn program. Thus, it has a least model. We say that
is a stable model of P if Both the notion of the reduct and that
of a stable model were introduced in [GL88].
It is known that every stable model of a program P is a supported model
of P . The converse does not hold in general. However, if a program P is purely
negative, then stable and supported models of P coincide [Fag94].
In our arguments we use fixed-parameter complexity results on problems
to decide the existence of models of prescribed sizes for propositional formulas
from some special classes. To describe these problems we introduce additional
terminology. First, given a propositional theory \Phi, by At(\Phi) we denote the set
of atoms occurring in \Phi. As in the case of logic programming, we consider as
models of a propositional theory \Phi only those sets of atoms that are subsets of
At(\Phi). Next, we define the following classes of formulas:
tN: the class of t-normalized formulas (if are simply CNF formulas)
the class of all 2-normalized formulas whose every clause is a disjunction
of at most three literals (clearly, 2N 3 is a subclass of the class 2N)
tNM: the class of monotone t-normalized formulas, that is, t-normalized formulas
in which there are no occurrences of the negation operator
tNA: the class of antimonotone t-normalized formulas, that is, t-normalized formulas
in which every atom is directly preceded by the negation operator.
Finally, we extend the notation M \Delta (C) and M 0
\Delta (C), to the case when C stands
for a class of propositional formulas. In this terminology, M 0
(3NM) denotes the
problem to decide whether a monotone 3-normalized formula \Phi has a model in
which exactly k atoms are false. Similarly, M= (tN) is simply another notation for
the problem WS[t] that we discussed above. The following theorem establishes
several complexity results that we will use later in the paper.
Theorem 1. (i) The problems M= (2N) and M= (2NM) are W[2]-complete.
(ii) The problems M= (2N 3 ) and M= (2NA) are W[1]-complete.
(iii) The problem M 0
- (3N) is W [3]-complete.
Proof: The statements (i) and (ii) are proved in [DF97]. To prove the statement
(iii), we use the fact that the problem M- (3N) is W [3]-complete [DF97]. We
reduce M- (3N) to M 0
- (3N) and conversely. Let us consider a 3-normalized
are literals. We observe
that \Phi has a model of cardinality at most k if and only if a related formula
obtained from \Phi by replacing every negative literal
:x by a new atom -
x and every positive literal x by a negated atom :-x, has a
model of cardinality at least jAt( -
construction defines a reduction
of M- (3N) to M 0
- (3N). It is easy to see that this reduction satisfies all the
requirements of the definition of fixed-parameter reducibility.
A reduction of M 0
- (3N) to M- (3N) can be constructed in a similar way.
Since the problem M- (3N) is W[3]-complete, so is the problem M 0
(3N). 2
In the proof of part (iii) of Theorem 1, we observed that the reduction we
described there satisfies all the requirements specified in Definition 1 of fixed-
parameter reducibility. Throughout the paper we prove our complexity results
by constructing reductions from one problem to another. In most cases, we only
verify the condition (4) of the definition which, usually, is the only non-trivial
part of the proof. Checking that the remaining conditions hold is straightforward
and we leave these details out.
3 Some proofs
In this section we present some typical proofs of fixed-parameter complexity
results for problems involving existence of models, supported models and stable
models of logic programs. Our goal is to introduce key proof techniques that we
used when proving the results discussed in the introduction.
Theorem 2. The problems M 0
are W[2]-complete.
Proof: Both problems are clearly in W[2] (models of a logic program P are models
of the corresponding 2-normalized formula pr(P )). Since H ' A, to complete
the proof it is enough to show that the problem M 0
= (H) is W[2]-hard. To this
end, we will reduce the problem M= (2NM) to M 0
(H).
Let \Phi be a monotone 2-normalized formula and let k - 0. Let fx
be the set of atoms of \Phi. We define a Horn program P \Phi corresponding to \Phi as
follows. We choose an atom a not occurring in \Phi and include in P \Phi all rules of
the form x i / a, Next, for each clause
of \Phi
we include in P \Phi the rule
We will show that \Phi has a model of size k if and only if P \Phi has a model of size
Let M be a model of \Phi of size k. We define M . The set
M 0 has us consider any clause r C 2 P \Phi of the form given
above. Since M satisfies C, there is
is a model of r C . Since a =
clauses x i / a. Hence, M 0 is a
model of P \Phi .
Conversely, let M 0 be a model of P \Phi of size exactly n \Gamma k. If a 2 M 0 then
Consequently, we obtain that a =
all clauses in \Phi. Indeed, let us assume that there
is a clause C such that no atom of C is in M . Then, all atoms of C are in M 0 .
contradiction. Now, the assertion follows by
Theorem 1. 2
Theorem 3. The problem M= (H) is W[1]-complete.
Proof: We will first prove the hardness part. To this end, we will reduce the problem
M= (2NA) to the problem M= (H). Let \Phi be an antimonotone 2-normalized
formula and let k be a non-negative integer. Let a different
atoms not occurring in \Phi. For each clause of \Phi we define a
logic program rule r C by
We then define P \Phi by
Let us assume that M is a model of size k of the program P \Phi . If for some i,
consequently,
contradiction. Thus, M does not contain any of the atoms a i . Since M satisfies
all rules r C and since it consists of atoms of \Phi only, M is a model of \Phi (indeed,
the body of each rule r C must be false so, consequently, each clause C must be
true). Similarly, one can show that if M is a model of \Phi then it is a model of
P \Phi . Thus, W[1]-hardness follows by Theorem 1.
To prove that the problem M= (H) is in the class W[1], we will reduce it to
the problem M= (2N 3 ). To this end, for every Horn program P we will describe
a 2-normalized formula \Phi P , with each clause consisting of no more than three
literals, and such that P has a model of size k if and only if \Phi P has a model of
k. Moreover, we will show that \Phi P can be constructed in time
bounded by a polynomial in the size of P (with the degree not depending on k).
First, let us observe that without loss of generality we may restrict our attention
to Horn programs whose rules do not contain multiple occurrences of
the same atom in the body. Such occurrences can be eliminated in time linear
in the size of the program. Next, let us note that under this restriction, a Horn
program P has a model of size k if and only if the program P 0 , obtained from
P by removing all clauses with bodies consisting of more than k atoms, has a
model of size k. The program P 0 can be constructed in time linear in the size of
P and k.
Thus, we will describe the construction of the formula \Phi P only for Horn
programs P in which the body of every rule consists of no more than k atoms.
Let P be such a program. We define
For every set B 2 B we introduce a new variable u[B]. Further, for every atom
x in P we introduce 2 k new atoms x[i],
We will now define several families of formulas. First, for every x 2 At(P )
and, for each set B 2 B and for each x 2 B, we define
Next, for each set B 2 B and for each x 2 B we define
Finally, for each rule r in P we introduce a formula
We define \Phi P to be the conjunction of all these formulas (more precisely, of
their 2-normalized representations given in the parentheses) and of the formula
u[;]. Clearly, \Phi P is a formula from the class 2N 3 . Further, since the body of each
rule in P has at most k elements, the set B has no more than jP j2 k elements, each
of them of size at most k (jP j denotes the cardinality of P , that is, the number
of rules in P ). Thus, \Phi P can be constructed in time bounded by a polynomial
in the size of P , whose degree does not depend on k.
Let us consider a model M of P such that jM k. We define
The set M 0 satisfies all formulas D(x; i), x 2 At(P In addition,
the formula u[;] is also satisfied by M 0
Let us consider a formula E(B;x), for some us assume
that x - u[B n fxg] is true in M 0 . Then,
Moreover, since u[B n It follows that B ' M and,
consequently, that u[B] 2 M 0 . Thus, M 0 satisfies all "E-formulas" in \Phi P .
Next, let us consider a formula F (B; x), where
us assume that M 0 satisfies u[B]. It follows that B ' M . Consequently, x 2 M .
Lastly, let us look at a formula G(r), where r 2 P . Let us assume that
Since r is a Horn clause and since M is a model
of P , it follows that h(r) 2 M . Consequently, h(r) 2 M 0 . Thus, M 0 is a model
of G(r).
We proved that M 0 is a model of \Phi P . Moreover, it is easy to see that jM
Conversely, let us assume that M 0 is a model of \Phi P and that jM 0
k. We set First, we will show that M is a model of P .
Let us consider an arbitrary clause r 2 P , say
where h and b i , are atoms. Let us assume that fb We
need to show that h 2 M .
b(r), the set fb and all its subsets belong to B.
Thus, \Phi P contains formulas
these formulas are satisfied by M 0 . We also have u[;] 2 \Phi P .
Consequently, u[;] is satisfied by M 0 , as well. Since all atoms b i , are
also satisfied by M 0 (since
by M 0 .
The formula belongs to \Phi P . Thus, it is satisfied
by M 0 . It follows that Thus, M is a model of
r and, consequently, of the program P .
To complete the proof we have to show that jM is a model of
contains all atoms x[i], 1
then
So, we will assume that jM j ! k. Let us consider an atom u[B], where B 2 B,
such that u[B] 2 M 0 . For every x 2 B, \Phi P contains the rule F (B; x). The set M 0
is a model of F (B; x). Thus, x 2 M 0 and, since x 2 At(P ), we have that x 2 M .
It follows that B ' M . It is now easy to see that the number of atoms of the form
u[B] that are true in M 0 is smaller than 2 k . Thus, jM
again a contradiction. Consequently, jM
It follows that the problem M= (H) can be reduced to the problem M= (2N 3 ).
Thus, by Theorem 1, the problem M= (H) is in the class W[1]. This completes
our argument. 2
Theorem 4. The problem SP= (A) is in W [2].
Proof: We will show a reduction of SP= (A) to M= (2N), which is in W [2] by
Theorem 1. Let P be a logic program with atoms x . We can identify
supported models of P with models of its completion comp(P ). The completion
is of the form comp(P
are literals. It can be constructed in linear time in the
size of the program P .
We will use comp(P ) to define a formula \Phi P . The atoms of \Phi P are x
and u[i; j],
I
The formula \Phi P is a conjunction of the formulas written above (of the formulas
given in the parentheses, to be precise). Clearly, \Phi P is a 2-normalized
formula. We will show that comp(P ) has a model of size k (or equivalently, that
P has a supported model of size if and only if \Phi P has a model of size 2k.
be a model of comp(P ). Then, for each
there is is a model of Vm ij
(this is because
M is a model of every formula \Phi i ). We denote one such j (an arbitrary one) by
We claim that
is a model of \Phi P . Clearly, G i is true in M 0 for every
i is satisfied by M 0 . Since for each i,
there is at most one j such that u[i; j] 2 M 0 , it follows that every
. By the definition of j i , if u[i;
M 0 is a model of Vm ij
I i is satisfied by M 0 . Finally, all formulas
clearly true in M 0 . Thus, M 0 is a model of \Phi P of size 2k.
Conversely, let M 0 be a model of \Phi P such that jM us assume that
contains exactly s atoms u[i; j]. The clauses H i ensure that for each i, M 0
contains at most one atom u[i; j]. Therefore, the set M 0 "fu[i; j]:
is of the form fu[p ps
Since the conjunction of G i and G 0
i is equivalent to x i
follows that exactly s atoms x i belong to M 0 . Thus, jM
It is now easy to see that M 0 is of the form fx
We will now prove that for every
is true in M 0 . To this end, let us assume that x i is true in M 0 . Then, there is
, for some t,
k). Since the formula I i is true in M 0 , the formula
in M 0 . Thus, the formula
is true in M 0 , too.
Since for every i, 1 - i - n, the formula J i is true in M 0 , it follows that
all formulas \Phi i are true in M 0 . Since the only atoms of M 0 that appear in the
are the atoms x is a
model of comp(P
Thus, the problem SP= (A) can be reduced to the problem M= (2N), which
completes the proof. 2
For the problem SP= (A) we also established the hardness result - we proved
that it is W[2]-hard (we omit the proof due to space restrictions). Thus, we found
the exact location of this problem in the W-hierarchy. For the problem ST 0
that we are about to consider now, we only succeeded in establishing the lower
bound on its complexity. We proved it to be W[3]-hard. We did not succeed in
obtaining any non-trivial upper estimate on its complexity.
Theorem 5. The problem ST 0
Proof: We will reduce the problem M 0
- (3N) to the problem ST 0
(A). Let
be a 3-normalized formula, where x[i; j; '] are literals. Let
v[2k+1] be new atoms not occurring in \Phi. For each atom x 2 At(\Phi), we introduce
new atoms x[s],
Let P \Phi be a logic program with the following rules:
where
ae
Clearly, jAt(P \Phi We will show
that \Phi has a model of cardinality at least n \Gamma k if and only if P \Phi has a stable
model of cardinality at least jAt(P \Phi
be a model of \Phi, where x are some
atoms from At(\Phi) that are not necessarily distinct. We claim that M
is a stable model of P \Phi .
Let us notice that a rule A(x; y; s) is not blocked by M 0 if and only if
Hence, the program P M 0
\Phi consists of the rules:
and of some of the rules with heads u[i]. Let us suppose that every rule of P \Phi
with head u[i] contains either a negated atom x 2 M or a non-negated atom
. Then, for every
either x[i; j; Thus, M is not
a model of the formula
consequently, M is not a model
of \Phi, a contradiction. Hence, for every there is a rule with head
u[i] containing neither a negated atom x 2 M nor a non-negated atom x 62 M .
These rules also contribute to the reduct P M 0
\Phi .
All atoms x[s] are facts in P M 0
\Phi . Thus, they belong
to lm(P M 0
Conversely, if x[s] 2 lm(P M 0
Moreover, it is evident by rules B(x) that x 2 lm(P M 0
only if x 6=
Hence, by the observations in the previous paragraph, u[i] 2
\Phi ), for each Finally, v[q] 2 lm(P M 0
because the rules D(q) belong to the reduct P M 0
\Phi . Hence, M
is a stable model of P \Phi and its cardinality is at least n(k
Conversely, let M 0 be a stable model of P \Phi of size at least jAt(P \Phi )j \Gamma 2k.
all atoms v[q], must be members of M 0 and, conse-
quently, m. Hence, for each there is a rule
in P \Phi
such that x 0 [i;
Thus, M 0 is a model of the formula
Therefore is a model of \Phi.
It is a routine task to check that rules A(x; imply that all
stable models of P \Phi are of the form
are not necessarily distinct). Hence, jM
We have reduced the problem M 0
- (3N) to the problem ST 0
(A). Thus, the
assertion follows by Theorem 1. 2



--R

Negation as failure.
Parameterized Complexity.
Consistency of Clark's completion and existence of stable models.
The stable semantics for logic programs.
Fixed parameter complexity in AI and nonmonotonic reasoning.
Computing large and small stable models.
--TR
Foundations of logic programming
Logic programming
Autoepistemic logic
Contributions to the Theory of Logic Programming
Fixed-Parameter Complexity in AI and Nonmonotonic Reasoning

--CTR
Zbigniew Lonc , Mirosaw Truszczyski, Computing stable models: worst-case performance estimates, Theory and Practice of Logic Programming, v.4 n.2, p.193-231, January 2004
stable models;normal logic programs;fixed-parameter complexity;supported models