=Paper=
{{Paper
|id=None
|storemode=property
|title=Complexity of Super-Coherence Problems in Answer Set Programming
|pdfUrl=https://ceur-ws.org/Vol-810/paper-l08.pdf
|volume=Vol-810
|dblpUrl=https://dblp.org/rec/conf/cilc/AlvianoFW11
}}
==Complexity of Super-Coherence Problems in Answer Set Programming==
https://ceur-ws.org/Vol-810/paper-l08.pdf
Complexity of Super-Coherence Problems in ASP ⋆
Mario Alviano1 , Wolfgang Faber1 , and Stefan Woltran2
1
University of Calabria, Italy
{alviano,faber}@mat.unical.it
2
Vienna University of Technology, Austria
woltran@dbai.tuwien.ac.at
Abstract. Adapting techniques from database theory in order to optimize An-
swer Set Programming (ASP) systems, and in particular the grounding compo-
nents of ASP systems, is an important topic in ASP. In recent years, the Magic Set
method has received some interest in this setting, and a variant of it, called DMS,
has been proposed for ASP. However, this technique has a caveat, because it is not
correct (in the sense of being query-equivalent) for all ASP programs. In recent
work, a large fragment of ASP programs, referred to as super-coherent programs,
has been identified, for which DMS is correct. An open question remained: How
complex is it to determine whether a given program is super-coherent? This ques-
tion turned out to be quite difficult to answer precisely. In this paper, we formally
prove that deciding whether a propositional program is super-coherent is Π3P -
complete in the disjunctive case, while it is Π2P -complete for normal programs.
The hardness proofs are the difficult part in this endeavor: We proceed by charac-
terizing the reductions by the models and reduct models which the ASP programs
should have, and then provide instantiations that meet the given specifications.
1 Introduction
Answer Set Programming (ASP) is a powerful formalism for knowledge representation
and common sense reasoning [5]. Allowing disjunction in rule heads and nonmono-
tonic negation in bodies, ASP can express every query belonging to the complexity
NP
class ΣP2 (NP ). Encouraged by the availability of efficient inference engines, such
as DLV [17], GnT [15], Cmodels [18], or ClaspD [8], ASP has found several prac-
tical applications in various domains, including data integration [16], semantic-based
information extraction [20, 21], e-tourism [24], workforce management [25], and many
more. As a matter of fact, these ASP systems are continuously enhanced to support
novel optimization strategies, enabling them to be effective over increasingly larger ap-
plication domains.
Frequently, optimization techniques are inspired by methods that had been proposed
in other fields, for example database theory, satisfiability solving, or constraint satisfac-
tion. Among techniques adapted to ASP from database theory, Magic Sets [26, 4, 6]
⋆
This work will also be presented at the ASPOCP 2011 workshop. Partly supported by Re-
gione Calabria and EU under POR Calabria FESR 2007-2013 and within the PIA project of
DLVSYSTEM s.r.l., and by MIUR under the PRIN project LoDeN. We also thank the anony-
mous reviewers for their valuable comments.
have recently achieved a lot of attention. Following some earlier work [14, 7], recently
an adapted method called DMS has been proposed for ASP in [3]. However, this tech-
nique has a caveat, because it is not correct (in the sense of being query-equivalent) for
all ASP programs. In recent work [2, 1], a large fragment of ASP programs, referred
to as super-coherent programs (ASPsc ), has been identified, for which DMS can be
proved to be correct.
While our main motivation for studying ASPsc stemmed from the applicability of
DMS, this class actually has many more important motivations. Indeed, it can be viewed
as the class of non-constraining programs: Adding extensional information to these
programs will always result in answer sets. One important implication of this property
is for modular evaluation. For instance, when using the splitting set theorem of [19], if a
top part of a split program is an ASPsc program, then any answer set of the bottom part
will give rise to at least one answer set of the full program—so for determining answer
set existence, there would be no need to evaluate the top part.
On a more abstract level, one of the main criticisms of ASP (being voiced espe-
cially in database theory) is that there are programs which do not admit any answer set
(traditionally this has been considered a more serious problem than the related nondeter-
minism in the form of multiple answer sets, cf. [23]). From this perspective, programs
which guarantee coherence (existence of an answer set) have been of interest for quite
some time. In particular, if one considers a fixed program and a variable “database,”
one arrives naturally at the class ASPsc when requiring existence of an answer set. This
also indicates that deciding super-coherence of programs is related to some problems
from the area of equivalence checking in ASP [13, 10, 22]. For instance, when deciding
whether, for a given arbitrary program P , there is a uniformly equivalent definite pos-
itive (or definite Horn) program, super-coherence of P is a necessary condition—this
is straightforward to see because definite Horn programs have exactly one answer set,
so a non-super-coherent program cannot be uniformly equivalent to any definite Horn
program.
Since the property of being super-coherent is a semantic one, a natural question
arises: How difficult is it to decide whether a given program belongs to ASPsc ? It turns
out that the precise complexity is rather difficult to establish. Some bounds have been
given in [2], in particular showing decidability, but especially hardness results seemed
quite hard to obtain.
In order to focus on the essentials of this problem, in this paper we deal with propo-
sitional programs and show the precise complexity (in terms of completeness) for de-
ciding whether a given propositional ASP program belongs to ASPsc . In Section 2 we
first define some terminology needed later on. In Section 3 we formulate the problem
that we analyze and state the results. The remainder of the paper contains the proofs —
in Section 4 for disjunctive programs and in Section 5 for normal programs — and in
Section 6 we briefly discuss the relation to equivalence problems before concluding the
work in Section 7.
2 Preliminaries
In this paper we consider propositional programs, so an atom p is a member of a count-
able set U . A literal is either an atom p (a positive literal), or an atom preceded by the
negation as failure symbol not (a negative literal). A rule r is of the form
p1 ∨ · · · ∨ pn ← q1 , . . . , qj , not qj+1 , . . . , not qm
where p1 , . . . , pn , q1 , . . . , qm are atoms and n ≥ 0, m ≥ j ≥ 0. The disjunction p1 ∨
· · · ∨ pn is the head of r, while the conjunction q1 , . . . , qj , not qj+1 , . . . , not qm is
the body of r. Moreover, H(r) denotes the set of head atoms, while B(r) denotes the set
of body literals. We also use B + (r) and B − (r) for denoting the set of atoms appearing
in positive and negative body literals, respectively, and At(r) for the set H(r)∪B + (r)∪
B − (r). A rule r is normal (or disjunction-free) if |H(r)| = 1 or |H(r)| = 0 (in this
case r is also referred to as a constraint), positive (or negation-free) if B − (r) = ∅, a
fact if both B(r) = ∅ and |H(r)| = 1.
A program P is a finite set of rules; if all rules in it are positive (resp. normal),
then P is a positive (resp. normal) program. Odd-cycle-free and stratified programs
constitute two other interesting classes of programs. An atom p appearing in the head
of a rule r depends on each atom q that belongs to B(r); if q belongs to B + (r), p
depends positively on q, otherwise negatively. A program without constraints is odd-
cycle-free if there is no cycle of dependencies involving an odd number of negative
dependencies, while it is stratified if each cycle of dependencies involves only positive
dependencies. Programs containing constraints have been excluded by the definition of
odd-cycle-free and stratified programs. In fact, constraints intrinsically introduce odd-
cycles in programs as a constraint of the form
← q1 , . . . , qj , not qj+1 , . . . , not qm
can be replaced by the following equivalent rule:
co ← q1 , . . . , qj , not qj+1 , . . . , not qm , not co,
where co is a fresh atom (i.e., an atom that does not occur elsewhere in the program).
Given Sa program P , let At(P ) denote the set of atoms that occur in it, that is, let
At(P ) = r∈P At(r). An interpretation I for a program P is a subset of At(P ). An
atom p is true w.r.t. an interpretation I if p ∈ I; otherwise, it is false. A negative literal
not p is true w.r.t. I if and only if p is false w.r.t. I. The body of a rule r is true w.r.t. I if
and only if all the body literals of r are true w.r.t. I, that is, if and only if B + (r) ⊆ I and
B − (r) ∩ I = ∅. An interpretation I satisfies a rule r ∈ P if at least one atom in H(r)
is true w.r.t. I whenever the body of r is true w.r.t. I. An interpretation I is a model of
a program P if I satisfies all the rules in P .
Given an interpretation I for a program P , the reduct of P w.r.t. I, denoted by P I , is
obtained by deleting from P all the rules r with B − (r) ∩ I 6= ∅, and then by removing
all the negative literals from the remaining rules. The semantics of a program P is given
by the set AS(P ) of the answer sets of P , where an interpretation M is an answer set
for P if and only if M is a subset-minimal model of P M .
In the subsequent sections, we will use the following properties that the models and
models of reducts of programs satisfy (see, e.g. [9, 13]):
(P1) for any disjunctive program P and interpretations I ⊆ J ⊆ K, if I satisfies P J ,
then I also satisfies P K ;
(P2) for any normal program P and interpretations I, J ⊆ K, if I and J both satisfy
P K , then also (I ∩ J) satisfies P K .
We now introduce super-coherent ASP programs (ASPsc programs), the main class
of programs studied in this paper.
Definition 1 (ASPsc programs [1, 2]). A program P is super-coherent if, for every set
of facts F , AS(P ∪ F ) 6= ∅. Let ASPsc denote the set of all super-coherent programs.
Note that ASPsc programs include all odd-cycle-free programs (and therefore also
all stratified programs). Indeed, every odd-cycle-free program admits at least one an-
swer set and remains odd-cycle-free even if an arbitrary set of facts is added to its rules.
On the other hand, there are programs having odd-cycles that are in ASPsc , cf. [2].
An important question regards whether ASPsc programs are as expressive as ASP
programs. Of course, checking coherence (existence of answer sets) is a trivial task for
ASPsc programs. But when considering query answering, it turns out that expressivity
is not lowered. Indeed, all expressivity results of [12] hold for disjunctive programs
with stratified negation (examining the proofs, actually for disjunctive programs with
input negation, that is, having at most two strata), which guarantee super-coherence
and are a proper subset of ASPsc . It therefore follows that all properties in Σ2P or Π2P
are expressible by ASPsc programs using a query under brave or cautious reasoning,
respectively. The picture is less clear for nondisjunctive ASPsc programs.
However, we should point out that many (probably most) existing ASP programs
follow a “Guess&Check” or “Generate&Test” methodology, which usually relies on
integrity constraints, the presence of which usually contradicts super-coherence. As
an alternative, violated integrity constraints can derive a special atom, on which the
query atom should depend negatively. If the Guess/Generate part involves non-stratified
negation, it depends on how this construct is used in the encoding. If it just encodes a
choice, this can often be easily converted to a disjunction, while for encodings that
entangle guess and check using unstratified negation, an automated conversion to an
ASPsc program seems less straightforward. In general, however, we feel that for ob-
taining computationally efficient ASPsc encodings, different encoding methodologies
should be developed.
3 Problem Statement and Main Theorems
In this paper, we study the complexity of the following natural problem.
– Given a program P , is P super-coherent, i.e. does AS(P ∪ F ) 6= ∅ hold for any set
F of facts.
We will study the complexity for this problem for the case of disjunctive logic pro-
grams and non-disjunctive (normal) logic programs. We first have a look at a similar
problem, which turns out to be rather trivial to decide.
Proposition 1. The problem of deciding whether, for a given disjunctive program P ,
there is a set F of facts such that AS(P ∪ F ) 6= ∅ is NP-complete; NP-hardness holds
already for normal programs.
Proof. We start by observing that there is F such that AS(P ∪ F ) 6= ∅ if and only if P
has at least one classical model. Indeed, if M is a model of P , then P ∪ M has M as its
answer set. On the other hand, if P has no model, then no addition of facts F will yield
an answer set for P ∪ F . It is well known that deciding whether a program has at least
one (classical) model is NP-complete for both disjunctive and normal programs. 2
In contrast, the complexity for deciding super-coherence is surprisingly high, which
we shall show next. To start, we give a straight-forward observation.
Proposition 2. A program P is super-coherent if and only if for each set F ⊆ At(P ),
AS(P ∪ F ) 6= ∅.
Proof. The only-if direction is by definition. For the if-direction, let F be any set of
facts. F can be partitioned into F ′ = F ∩ At(P ) and F ′′ = F \ F ′ . By assumption,
P ∪ F ′ is coherent. Let M be an answer set of P ∪ F ′ . We shall show that M ∪ F ′′ is
an answer set of P ∪ F = P ∪ F ′ ∪ F ′′ . This is in fact a consequence of the splitting
set theorem [19], as the atoms in F ′′ are only defined by facts not occurring in P ∪ F ′ .
2
Our main results are as follows. The proofs are contained in the subsequent sections.
Theorem 1. The problem of deciding super-coherence for disjunctive programs is Π3P -
complete.
Theorem 2. The problem of deciding super-coherence for normal programs is Π2P -
complete.
4 Proof of Theorem 1
Membership follows by the following straight-forward nondeterministic algorithm for
the complementary problem, i.e. given a program P , does there exist a set F of facts
such that AS(P ∪ F ) = ∅: we guess a set F ⊆ At(P ) and check AS(P ∪ F ) = ∅ via
an oracle-call. Restricting the guess to At(P ) can be done by Proposition 2. Checking
AS(P ∪ F ) = ∅ is known to be in Π2P [11]. This shows Π3P -membership.
For the hardness we reduce the Π3P -complete problem of deciding whether QBFs
of the form ∀X∃Y ∀Zφ are true to the problem of super-coherence. Without loss of
generality, we can consider φ to be in DNF and, indeed, X 6= ∅, Y 6= ∅, and Z 6= ∅. We
also assume that each disjunct of Φ contains at least one variable from X, one from Y
and one from Z. More precisely, we shall construct for each such QBF Φ a program PΦ
such that Φ is true iff PΦ is super-coherent. Before showing how to actually construct
PΦ from Φ in polynomial time, we give the required properties for PΦ . We then show
that for programs PΦ satisfying these properties, the desired relation (Φ is true iff PΦ is
super-coherent) holds, and finally we provide the construction of PΦ .
Definition 2. Let Φ = ∀X∃Y ∀Zφ be a QBF with φ in DNF. We call any program P
satisfying the following properties a Φ-reduction:
1. P is given over atoms U = X ∪ Y ∪ Z ∪ X ∪ Y ∪ Z ∪ {u, v, w}, where all atoms
in sets S = {s | s ∈ S} and {u, v, w} are fresh and mutually disjoint;
2. P has the following models:
– U
– for each I ⊆ X, J ⊆ Y ,
M [I, J] = I ∪ (X \ I) ∪ J ∪ (Y \ J) ∪ Z ∪ Z ∪ {u, v}
and
M ′ [I, J] = I ∪ (X \ I) ∪ J ∪ (Y \ J) ∪ Z ∪ Z ∪ {v, w};
3. for each I ⊆ X, J ⊆ Y , the models3 of the reduct P M [I,J] are M [I, J] and
O[I] = I ∪ (X \ I);
′
4. for each I ⊆ X, J ⊆ Y , the models of the reduct P M [I,J] are M ′ [I, J] and
– for each K ⊆ Z such that I ∪ J ∪ K 6|= φ,
N [I, J, K] = I ∪ (X \ I) ∪ J ∪ (Y \ J) ∪ K ∪ (Z \ K) ∪ {v};
5. the models of the reduct P U are given only by the models already mentioned above,
i.e. U itself, M [I, J], M ′ [I, J], and O[I], for each I ⊆ X, J ⊆ Y , and N [I, J, K]
for each I ⊆ X, J ⊆ Y , K ⊆ Z, such that I ∪ J ∪ K 6|= φ.
The structure of models of Φ-reductions and the “countermodels” (see below what
we mean by this term) of the relevant reducts is sketched in Figure 1. The center of the
diagram contains the models of the Φ-reduction and their subset relationship. For each
of the model the respective box lists the “countermodels,” by which we mean those
reduct models which can serve as counterexamples for the original model being an
answer set, that is, those reduct models which are proper subsets of the original model.
We just note at this point that the models of the reduct P U given in Item 5 are not
specified for particular purposes, but are required to allow for a realization via disjunc-
tive programs. In fact, these models are just an effect of property (P1) mentioned in Sec-
tion 2. However, before showing a program satisfying the properties of a Φ-reduction,
we first show the rationale behind the concept of Φ-reductions.
Lemma 1. For any QBF Φ = ∀X∃Y ∀Zφ with φ in DNF, a Φ-reduction is super-
coherent iff Φ is true.
Proof. Suppose that Φ is false. Hence, there exists an I ⊆ X such that, for all J ⊆ Y ,
there is a KY ⊆ Z with I ∪ J ∪ KY 6|= φ. Now let P be any Φ-reduction and FI =
I ∪ (X \ I). We show that AS(P ∪ FI ) = ∅, thus P is not super-coherent. Let M be a
model of P ∪ FI . Since P is a Φ-reduction, the only candidates for M are U , M [I, J],
and M ′ [I, J], where J ⊆ Y . Indeed, for each I 6= I, M [I, J] and M ′ [I, J] cannot be
models of P ∪ FI because FI 6⊆ M [I, J], resp. FI 6⊆ M ′ [I, J]. We now analyze these
three types of potential candidates:
3
Here and below, for a reduct P M we only list models of the form N ⊆ M , since those are the
relevant ones for our purposes. Recall that N = M is always a model of P M in case M is a
model of P .
M [I0 , J0 ] · · · M [Im , Jn ] M ′ [I0 , J0 ] · · · M ′ [Im , Jn ]
N [I0 , J0 , K] s.t. N [Im , Jn , K] s.t.
O[I0 ] · · · O[Im ] ···
I0 ∪ J0 ∪ K 6|= φ Im ∪ Jn ∪ K 6|= φ
PU
U
⊂ ⊂
⊂ ⊂
··· ···
M [I0 , J0 ] ··· M [Im , Jn ] M ′ [I0 , J0 ] ··· M ′ [Im , Jn ]
′ ′
P M [I0 ,J0 ] P M [Im ,Jn ] P M [I0 ,J0 ] P M [Im ,Jn ]
N [I0 , J0 , K] s.t. N [Im , Jn , K] s.t.
O[I0 ] ··· O[Im ] ···
I0 ∪ J0 ∪ K 6|= φ Im ∪ Jn ∪ K 6|= φ
Fig. 1. Models and reduct “countermodels” of Φ-reductions
– M = U : Then, for instance, M [I, J] ⊂ U is a model of (P ∪ FI )M = P M ∪ FI
for any J ⊆ Y . Thus, M ∈ / AS(P ∪ FI ).
– M = M [I, J] for some J ⊆ Y . Then, by the properties of Φ-reductions, O[I] ⊂
M is a model of (P ∪ FI )M = P M ∪ FI . Thus, M ∈ / AS(P ∪ FI ).
– M = M ′ [I, J] for some J ⊆ Y . By the initial assumption, there exists a KY ⊆ Z
with I ∪ J ∪ KY 6|= φ. Then, by the properties of Φ-reductions, N [I, J, K] ⊂ M
is a model of P M . Thus, M ∈/ AS(P ∪ FI ).
In each of the cases we have obtained M ∈
/ AS(P ∪ FI ), hence AS(P ∪ FI ) = ∅
and P is not super-coherent.
Suppose that Φ is true. It is sufficient to show that for each F ⊆ U , AS(P ∪ F ) 6= ∅.
We have the following cases:
If {s, s} ⊆ F for some s ∈ X ∪ Y or {u, w} ⊆ F . Then U ∈ AS(P ∪ F ) since
U is a model of P ∪ F and each potential model M ⊂ U of the reduct P U (see the
properties of Φ-reductions) does not satisfy F ⊆ M ; thus each such M is not a model
of P U ∪ F = (P ∪ F )U .
Otherwise, we have F ⊆ M [I, J] or F ⊆ M ′ [I, J] for some I ⊆ X, J ⊆ Y . In
case F ⊆ M [I, J] and F 6⊆ O[I], we observe that M [I, J] ∈ AS(P ∪ F ) since O[I]
is the only model of the reduct P M [I,J] . Thus for each such F there cannot be a model
M ⊂ M [I, J] of P M [I,J] ∪ F = (P ∪ F )M [I,J] . As well, in case F ⊆ M ′ [I, J], where
w ∈ F , M ′ [I, J] can be shown to be an answer set of P ∪ F . Indeed, in this case no
′
M ⊂ M ′ [I, J] is a model of P M [I,J] because Φ is true.
It remains to consider the case F ⊆ O[I] for each I ⊆ X. We show that M ′ [I, J]
is an answer set of P ∪ F , for some J ⊆ Y . Since Φ is true, we know that, for each
I ⊆ X, there exists a JI ⊆ Y such that, for all K ⊆ Z, I ∪ JI ∪ K |= φ. As can
be verified by the properties of Φ-reductions, then there is no model M ⊂ M ′ [I, JI ]
′ ′
of P M [I,JI ] . Consequently, there is also no such model of (P ∪ F )M [I,JI ] , and thus
M ′ [I, JI ] ∈ AS(P ∪ F ).
So in each of these cases AS(P ∪ F ) 6= ∅ and since these cases cover all possible
F ⊆ U , we obtain that P is supercoherent.
In total we have shown that Φ being false implies that any Φ-reduction P is not
super-coherent, while Φ being true implies that any Φ-reduction is super-coherent,
which proves the lemma.
2
It remains to show that for any QBF of the desired form, a Φ-reduction can be
obtained in polynomial time (w.r.t. the size of Φ). For the construction below, let us
denote a negated atom a in the propositional part of the QBF Φ as a.
Wn
Definition 3. For any QBF Φ = ∀X∃Y ∀Zφ with φ = i=1 li,1 ∧ · · · ∧ li,mi a DNF
(i.e., a disjunction of conjunctions over literals), we define
PΦ = {x ∨ x ←; u ← x, x; w ← x, x; x ← u, w; x ← u, w | x ∈ X} ∪ (1)
{y ∨ y ← v; u ← y, y; w ← y, y; y ← u, w;
y ← u, w; v ← y; v ← y | y ∈ Y } ∪ (2)
{z ∨ z ← v; u ← z, not w; u ← z, not w; v ← z; v ← z;
z ← w; z ← w; z ← u; z ← u; w ∨ u ← z, z | z ∈ Z} ∪ (3)
{w ∨ u ← li,1 , . . . , li,mi | 1 ≤ i ≤ n} (4)
{v ← w; v ← u; v ← not u}. (5)
Obviously, the program from above definition can be constructed in polynomial
time in the size of the reduced QBF. To conclude the proof of Theorem 1 it is thus
sufficient to show the following relation.
Lemma 2. For any QBF Φ = ∀X∃Y ∀Zφ, the program PΦ is a Φ-reduction.
Proof. Obviously, At(PΦ ) contains the atoms as required in 1) of Definition 2. We
continue to show 2). To see that U is a model of PΦ is obvious. We next show that the
remaining models M are all of the form M [I, J] or M ′ [I, J]. First we have v ∈ M
because of the rules v ← u and v ← not u in (5). In case w ∈ M , Z ∪ Z ⊆ M by
the rules in (3). In case w ∈
/ M , we have K ∪ (Z \ K) ⊆ M for some K ⊆ Z, since
v ∈ M and by (3). But then, since w ∈ / M , u ∈ M holds (rules u ← z, not w resp.
u ← z, not w). Hence, also here Z ∪ Z ⊆ M . In both cases, we observe that by (1)
and (2), I ∪ (X \ U ) ∪ J ∪ (Y \ J) ⊆ M , for some I ⊆ X and J ⊆ Y . This yields
the desired models, M [I, J], M ′ [I, J]. It can be checked that no other model exists by
showing that for N 6⊆ M [I, J], resp. N 6⊆ M ′ [I, J], N = U follows.
′
We next show that, for each I ⊆ X and J ⊆ Y , P M [I,J] and P M [I,J] possess the
M [I,J]
required models. Let us start by showing that O[I] is a model of P . In fact, it can
be observed that all of the rules of the form x ∨ x ← in (1) are satisfied because either
x or x belong to O[I], while all of the other rules in P M [I,J] are satisfied because of a
false body literal. We also note that each strict subset of O[I] does not satisfy some rule
of the form x ∨ x ←, and thus it is not a model of P M [I,J] . Similarly, any interpretation
W such that O[I] ⊂ W ⊂ M [I, J] does not satisfy some rule in P M [I,J] (note that
rules of the form u ← z and u ← z occur in P M [I,J] because w 6∈ M [I, J]; such rules
are obtained by rules in (3)).
′
Let us now consider P M [I,J] and let W ⊆ M ′ [I, J] be one of its models. We
shall show that either W = M ′ [I, J], or W = N [I, J, K] for some K ⊆ Z such that
′
I ∪ J ∪ Z 6|= φ. Note that v is a fact in P M [I,J] , hence v must belong to W . By (1)
and (2), since v ∈ W and W ⊆ M ′ [I, J], we can conclude that all of the atoms in
I ∪ (X \ I) ∪ J ∪ (Y \ J) belong to W . Consider now the atom w. If w belongs to
W , by the rules in (3) we conclude that all of the atoms in Z ∪ Z belong to W , and
thus W = M ′ [I, J]. Otherwise, if w 6∈ W , by the rules of the form z ∨ z ← v in (3),
there must be a set K ⊆ Z such that K ∪ (Z \ K) is contained in W . Note that no other
atoms in Z ∪Z can belong to W because of the last rule in (3). Hence, W = N [I, J, K].
Moreover, w 6∈ W and u 6∈ W imply that I ∪ J ∪ K 6|= φ holds because of (4).
Finally, one can show that P U does not yield additional models as those which are
already present by other models. Let W ⊆ U be a model of P U . By (1), O[I] ⊆ W
must hold for some I ⊆ X. Consider now the atom v. If v 6∈ W , we conclude that the
model W is actually O[I]. We can thus consider the other case, i.e. v ∈ W . By (2),
J ∪ (Y \ J) ⊆ W must hold for some J ⊆ Y . Consider now the atom u. If u ∈ W , we
have Z ∪ Z ⊆ W because of (3). If no other atom belongs to W , then W = M [I, J]
holds. Otherwise, if any other atom belongs to W , it can be checked that W must be
equal to U . We can then consider the case in which u 6∈ W , and the atom w. Again, we
have two possibilities. If w belongs to W , by (3) we conclude that all of the atoms in
Z ∪Z belong to W , and thus either W = M ′ [I, J] or W = U . Otherwise, if w 6∈ W , by
the rules of the form z ∨z ← v in (3), there must be a set K ⊆ Z such that K ∪(Z \ K)
is contained in W . Note that no other atoms in Z ∪ Z can belong to W because of the
last rule in (3). Hence, W = N [I, J, K]. Moreover, because of (4), w 6∈ W and u 6∈ W
imply that I ∪ J ∪ K 6|= φ holds. 2
Note that the program from Definition 3 does not contain constraints. As a conse-
quence, the Π3P -hardness result presented in this section also holds if we only consider
disjunctive ASP programs without constraints.
5 Proof of Theorem 2
Membership follows by the straight-forward nondeterministic algorithm for the com-
plementary problem presented in the previous section. We have just to note that a
co − NP oracle can be used for checking the consistency of a normal program. Thus,
Π2P -membership is established.
For the hardness we reduce the Π2P -complete problem of deciding whether QBFs of
the form ∀X∃Y φ are true to the problem of super-coherence. Without loss of generality,
we can consider φ to be in CNF and, indeed, X 6= ∅, and Y 6= ∅. We also assume that
each clause of Φ contains at least one variable from X and one from Y . More precisely,
we shall adapt the notion of Φ-reduction to normal programs. In particular, we have to
take into account a fundamental difference between disjunctive and normal programs:
while disjunctive programs allow for using disjunctive rules for guessing a subset of
atoms, such a guess can be achieved only by means of unstratified negation within a
normal program. For example, one atom in a set {x, y} can be guessed by means of the
following disjunctive rule: x ∨ y ←. Within a normal program, the same result can be
obtained by means of the following rules: x ← not y and y ← not x. However, these
last rules would be deleted in the reduced program associated with a model containing
both x and y, which would allow for an arbitrary subset of {x, y} to be part of a model
of the reduct. More generally speaking, we have to take Property (P2), as introduced
in Section 2, into account. This makes the following definition a bit more cumbersome
compared to Definition 2.
Definition 4. Let Φ = ∀X∃Y φ be a QBF with φ in CNF. We call any program P
satisfying the following properties a Φ-norm-reduction:
1. P is given over atoms U = X ∪ Y ∪ X ∪ Y ∪ {v, w}, where all atoms in sets
S = {s | s ∈ S} and {v, w} are fresh and mutually disjoint;
2. P has the following models:
– for each J ⊆ Y , and for each J ∗ such that J ∪ (Y \ J) ⊆ J ∗ ⊆ Y ∪ Y
O[J ∗ ] = X ∪ X ∪ J ∗ ∪ {v, w};
– for each I ⊆ X,
M [I] = I ∪ (X \ I) ∪ {v};
– for each I ⊆ X, J ⊆ Y , such that I ∪ J |= φ,
N [I, J] = I ∪ (X \ I) ∪ J ∪ (Y \ J) ∪ {w};
3. the only models of a reduct P M [I] are M [I] and M [I] \ {v}; the only model of a
reduct P N [I,J] is N [I, J];
∗
4. each model M of a reduct P O[J ] satisfies the following properties:
(a) for each y ∈ Y such that y ∈ O[J ∗ ] and y 6∈ O[J ∗ ], if w ∈ M , then y ∈ M ;
(b) for each y ∈ Y such that y ∈ O[J ∗ ] and y 6∈ O[J ∗ ], if w ∈ M , then y ∈ M ;
(c) if (Y ∪ Y ) ∩ M 6= ∅, then w ∈ M ;
(d) if there is a clause li,1 ∨ · · · ∨ li,mi of φ such that {li,1 , . . . , li,mi } ⊆ M , then
v ∈ M;
(e) if there is an x ∈ X such that {x, x} ⊆ M , or there is a y ∈ Y such that
{y, y} ⊆ M , or {v, w} ⊆ M , then it must hold that X ∪ X ∪ {v, w} ⊆ M .
Lemma 3. For any QBF Φ = ∀X∃Y φ with φ in CNF, a Φ-norm-reduction is super-
coherent iff Φ is true.
Proof. Suppose that Φ is false. Hence, there exists an I ⊆ X such that, for all J ⊆ Y ,
I ∪ J 6|= φ. Now, let P be any Φ-norm-reduction and FI = I ∪ (X \ I). We show that
AS(P ∪ FI ) = ∅, thus P is not super-coherent. Let M be a model of P ∪ FI . Since
P is a Φ-norm-reduction, the only candidates for M are O[J ∗ ] for some J ⊆ Y and
J ∗ such that J ∪ (Y \ J) ⊆ J ∗ ⊆ Y ∪ Y , M [I], and N [I, J ′ ], where J ′ ⊆ Y satisfies
I ∪ J ′ |= φ. However, from our assumption (for all J ⊆ Y , I ∪ J 6|= φ), no such
N [I, J ′ ] exists. Thus, it remains to consider O[J ∗ ] and M [I]. By the properties of Φ-
norm-reductions, M [I]\{v} is a model of P M [I] , and hence M [I]\{v} is also a model
of P M [I] ∪FI = (P ∪FI )M [I] . Thus, M [I] is not an answer set of P ∪FI . On the other
∗ ∗
hand, it can be checked that M [I] \ {v} is a model of P O[J ] ∪ FI = (P ∪ FI )O[J ] ,
for any O[J ∗ ], and so none of these O[J ∗ ] are answer sets of P ∪ FI either. Since this
means that no model of P ∪ FI is an answer set, we conclude AS(P ∪ FI ) = ∅, and
hence P is not super-coherent.
Suppose that Φ is true. It is sufficient to show that, for each F ⊆ U , AS(P ∪ F ) 6= ∅.
We distinguish the following cases for F ⊆ U :
F ⊆ I ∪ (X \ I) ∪ {v} for some I ⊆ X: If v ∈ F , then M [I] is the unique model
of P M [I] ∪ F = (P ∪ F )M [I] , and thus M [I] ∈ AS(P ∪ F ). Otherwise, if v ∈ / F,
since Φ is true, there exists a J ⊆ Y such that I ∪ J |= φ. Thus, N [I, J] is a model of
P ∪ F , and since no subset of N [I, J] is a model of (P ∪ F )N [I,J] (by property 3 of
Φ-norm-reductions), N [I, J] ∈ AS(P ∪ F ).
I ∪ (X \ I) ⊂ F ⊆ N [I, J] for some I ⊆ X and J ⊆ Y such that I ∪ J |= φ: In
this case N [I, J] is a model of P ∪ F and, by property 3 of Φ-norm-reductions, N [I, J]
is also the unique model of P N [I,J] ∪ F = (P ∪ F )N [I,J] .
I ∪ (X \ I) ⊂ F ⊆ N [I, J] for some I ⊆ X and J ⊆ Y such that I ∪ J 6|= φ:
We shall show that O[J] is an answer set of P ∪ F in this case. Let M be a model
of P O[J] ∪ F = (P ∪ F )O[J] . Since I ∪ (X \ I) ⊂ F ⊆ N [I, J], either w ∈ F or
(Y ∪ Y ) ∩ F 6= ∅. Clearly, F ⊆ M and so w ∈ M in the first case. Note that w ∈ M
holds also in the second case because of property 4(c) of Φ-norm-reductions. Thus, as
a consequence of properties 4(a) and 4(b) of Φ-norm-reductions, J ∪ (Y \ J) ⊆ M
holds. Since I ∪ J 6|= φ and because of property 4(d) of Φ-norm-reductions, v ∈ M
holds. Finally, since {v, w} ⊆ M and because of property 4(e) of Φ-norm-reductions,
X ∪ X ⊆ M holds and, thus, M = O[I].
In all other cases, either {v, w} ⊆ F , or there is an x ∈ X such that {x, x} ⊆ F ,
or there is a y ∈ Y such that {y, y} ⊆ F . We shall show that in such cases there is an
O[J ∗ ] which is an answer set of P ∪ F . Let O[J ∗ ] be such that J ∗ = F ∩ (Y ∪ Y ) and
∗ ∗
let M be a model of P O[J ] ∪ F = (P ∪ F )O[J ] such that M ⊆ O[J ∗ ]. We shall show
that O[J ∗ ] ⊆ M holds, which would imply that O[J ∗ ] = M is an answer set of P ∪ F .
Clearly, F ⊆ M holds. By property 4(e) of Φ-norm-reductions, X ∪ X ∪ {v, w} ⊆ M
holds. Thus, by property 4(a) of Φ-norm-reductions and because w ∈ M , it holds that
y ∈ M for each y ∈ Y such that y ∈ O[J ∗ ] and y ∈ / O[J ∗ ]. Similarly, by property
4(b) of Φ-norm-reductions and because w ∈ M , it holds that y ∈ M for each y ∈ Y
such that y ∈ O[J ∗ ] and y ∈ / O[J ∗ ]. Moreover, for all y ∈ Y such that {y, y} ⊆ O[J ∗ ],
it holds that {y, y} ⊆ F ⊆ M . Therefore, O[J ∗ ] ⊆ M holds and, consequently,
O[J ∗ ] ∈ AS(P ∪ F ).
So in each of these cases AS(P ∪ F ) 6= ∅ and since these cases cover all possible
F ⊆ U , we obtain that P is supercoherent.
Summarizing, we have shown that Φ being false implies that any Φ-norm-reduction
P is not super-coherent, while Φ being true implies that any Φ-norm-reduction is super-
coherent, which proves the lemma.
2
Vn
Definition 5. For any QBF Φ = ∀X∃Y φ with φ = i=1 li,1 ∨ · · · ∨ li,mi in CNF, we
define
NΦ = {x ← not x; x ← not x | x ∈ X} ∪ (6)
{y ← not y, w; y ← not y, w; w ← y; w ← y | y ∈ Y } ∪ (7)
{z ← v, w; z ← x, x; z ← y, y | z ∈ X ∪ X ∪ {v, w},
x ∈ X, y ∈ Y } ∪ (8)
{v ← li,1 , . . . , li,mi | 1 ≤ i ≤ n} ∪ (9)
{w ← not v}. (10)
Again, the program from the above definition can be constructed in polynomial time
in the size of the reduced QBF. To conclude the proof, it is thus sufficient to show the
following relation.
Lemma 4. For any QBF Φ = ∀X∃Y φ with φ in CNF, the program NΦ is a Φ-norm-
reduction.
Proof. We shall first show that NΦ has the requested models. Let M be a model of NΦ .
Let us consider the atoms v and w. Because of the rule w ← not v in (10), three cases
are possible:
1. {v, w} ⊆ M . Thus, X ∪ X ⊆ M holds because of (8). Moreover, there exists
J ⊆ Y such that J ∪ (Y \ J) ⊆ M because of (7). Note that any other atom in U
could belong to M . These are the models O[J ∗ ].
2. v ∈ M and w ∈ / M . Thus, there exists I ⊆ X such that I ∪ (X \ I) ⊆ M because
of (6). Moreover, no atoms in Y ∪ Y belong to M because of (7) and w ∈ / M by
assumption. Thus, M = M [I] in this case.
3. v ∈
/ M and w ∈ M . Thus, there exist I ⊆ X and J ⊆ Y such that I ∪(X \ I) ⊆ M
and J ∪ (Y \ J) ⊆ M because of (6) and (7). Hence, in this case M = N [I, J]
and, because of (9), it holds that I ∪ J |= φ.
Let us consider a reduct P M [I] and one of its models M ⊆ M [I]. First of all,
note that P M [I] contains a fact for each atom in I ∪ (X \ I). Thus, I ∪ (X \ I) ⊆ M
holds. Note also that, since each clause of φ contains at least one variable from Y , all
of the rules of (9) have at least one false body literal. Hence, either M = M [I] or
M = M [I] \ {v}, as required by Φ-norm-reductions.
For a reduct P N [I,J] such that I ∪ J |= φ it is enough to note that P N [I,J] contains
a fact for each atom of N [I, J].
∗
Let us consider a reduct P O[J ] and one of its models M ⊆ O[J ∗ ]. The first obser-
∗
vation is that for each y ∈ Y such that y ∈ O[J ∗ ] and y ∈ / O[J ∗ ], the reduct P O[J ]
contains a rule of the form y ← w (obtained by some rule in (7)). Similarly, for each
∗
y ∈ Y such that y ∈ O[J ∗ ] and y ∈ / O[J ∗ ], the reduct P O[J ] contains a rule of the
form y ← w (obtained by some rule in (7)). Hence, M must satisfy properties 4(a) and
4(b) of Φ-norm-reductions. Property 4(c) is a consequence of (7), property 4(d) follows
from (9) and, finally, property 4(e) must hold because of (8). 2
Note that the program from Definition 5 does not contain constraints. As a conse-
quence, the Π2P -hardness result presented in this section also holds if we only consider
normal ASP programs without constraints.
6 Some Implications
In [22] the following problem has been studied under the name “uniform equivalence
with projection:”
Given two programs P and Q, and two sets A, B of atoms, P ≡A
B Q iff for each
set F ⊆ A of facts, {I ∩ B | I ∈ AS(P ∪ F )} = {I ∩ B | I ∈ AS(Q ∪ F )}.
Let us call A the context alphabet and B the projection alphabet. As is easily verified
the following relation holds.
Proposition 3. A program P over atoms U is super-coherent iff P ≡U
∅ Q, where Q is
an arbitrary definite Horn program.
Note that P ≡U∅ Q means {I ∩ ∅ | I ∈ AS(P ∪ F )} = {I ∩ ∅ | I ∈ AS(Q ∪ F )}
for all sets F ⊆ U . Now observe that for any F ⊆ U , both of these sets are either
empty or contain the empty set, depending on whether the programs (extended by F )
have answer sets.
∅ iff AS(P ∪ F ) = ∅
{I ∩ ∅ | I ∈ AS(P ∪ F )} =
{∅} iff AS(P ∪ F ) 6= ∅
∅ iff AS(Q ∪ F ) = ∅
{I ∩ ∅ | I ∈ AS(Q ∪ F )} =
{∅} iff AS(Q ∪ F ) 6= ∅
If Q is a definite Horn program, then AS(Q ∪ F ) 6= ∅ for all F ⊆ U , and therefore
the statement of Proposition 3 becomes equivalent to checking whether AS(P ∪F ) 6= ∅
for all F ⊆ U , and thus whether P is super-coherent.
In [22], the complexity of the problem of deciding uniform equivalence with pro-
jection has also been investigated, reporting Π3P -completeness for disjunctive programs
and Π2P -completeness for normal programs. However, these hardness results use bound
context alphabets A ⊂ U (where U are all atoms from the compared programs). Our
results thus strengthen the observations in [22]. Using Proposition 3 and the main re-
sults in this paper, we obtain Π3P -hardness (resp. Π2P -hardness in the case of normal
programs) for uniform equivalence with projection even for the particular parameteri-
zation where the context alphabet is unrestricted, the projection set is empty, and one of
the compared programs are of a very simple structure (in fact, even the empty program
is sufficient for Q in Proposition 3).
7 Conclusion
Many recent advances in ASP rely on the adaptions of technologies from other ar-
eas. One important example is the Magic Set method, which stems from the area of
databases and is used in state-of-the-art ASP grounders. Recent work showed that a
particular variant of this technique only applies to a certain class of programs called
super-coherent [2]. Super-coherent programs are those which possess at least one an-
swer set, no matter which set of facts is added to them. We believe that this class of
programs is interesting of its own (for instance, since there is a certain relation to some
problems in equivalence checking) and thus studied here the exact complexity of recog-
nizing the property of super-coherence for disjunctive and normal programs. Our results
show that the problems are surprisingly hard, viz. complete for Π3P and resp. Π2P . One
direction of future work is to search for methods to turn arbitrary programs into super-
coherent ones with minimal changes. Our proofs might provide valuable foundations
for such methods. That said, for using super-coherent programs efficiently for applica-
tions, we believe that an approach that uses a methodology different from the currently
prevailing “Guess&Check” or “Generate&Test” should be developed.
References
1. Alviano, M., Faber, W.: Dynamic magic sets for super-consistent answer set programs. In:
Balduccini, M., Woltran, S. (eds.) Proceedings of the 3rd Workshop on Answer Set Program-
ming and Other Computing Paradigms (ASPOCP 2010) (Jul 2010)
2. Alviano, M., Faber, W.: Dynamic magic sets and super-coherent answer set programs. AI
Communications 24(2), 125–145 (2011)
3. Alviano, M., Faber, W., Greco, G., Leone, N.: Magic sets for disjunctive datalog programs.
Tech. Rep. 09/2009, Dipartimento di Matematica, Università della Calabria, Italy (2009),
http://www.wfaber.com/research/papers/TRMAT092009.pdf
4. Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.D.: Magic Sets and Other Strange Ways to Im-
plement Logic Programs. In: Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium
on Principles of Database Systems. pp. 1–15. Cambridge, Massachusetts (1986)
5. Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cam-
bridge University Press (2003)
6. Beeri, C., Ramakrishnan, R.: On the power of magic. Journal of Logic Programming 10(1–
4), 255–259 (1991)
7. Cumbo, C., Faber, W., Greco, G., Leone, N.: Enhancing the magic-set method for disjunc-
tive datalog programs. In: Proceedings of the the 20th International Conference on Logic
Programming – ICLP’04. LNCS, vol. 3132, pp. 371–385 (2004)
8. Drescher, C., Gebser, M., Grote, T., Kaufmann, B., König, A., Ostrowski, M., Schaub, T.:
Conflict-Driven Disjunctive Answer Set Solving. In: Brewka, G., Lang, J. (eds.) Proceedings
of the Eleventh International Conference on Principles of Knowledge Representation and
Reasoning (KR 2008). pp. 422–432. AAAI Press, Sydney, Australia (2008)
9. Eiter, T., Fink, M., Tompits, H., Woltran, S.: On eliminating disjunctions in stable logic pro-
gramming. In: Proceedings of the 9th International Conference on Principles of Knowledge
Representation and Reasoning (KR 2004). pp. 447–458. AAAI Press (2004)
10. Eiter, T., Fink, M., Woltran, S.: Semantical Characterizations and Complexity of Equiva-
lences in Stable Logic Programming. ACM Transactions on Computational Logic 8(3), 1–53
(2007)
11. Eiter, T., Gottlob, G.: On the computational cost of disjunctive logic programming: Proposi-
tional case. Annals of Mathematics and Artificial Intelligence 15(3-4), 289–323 (1995)
12. Eiter, T., Gottlob, G., Mannila, H.: Disjunctive Datalog. ACM Transactions on Database
Systems 22(3), 364–418 (Sep 1997)
13. Eiter, T., Tompits, H., Woltran, S.: On Solution Correspondences in Answer Set Program-
ming. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proceedings of the 19th International Joint Con-
ference on Artificial Intelligence (IJCAI’05). pp. 97–102. Professional Book Center (2005)
14. Greco, S.: Binding Propagation Techniques for the Optimization of Bound Disjunc-
tive Queries. IEEE Transactions on Knowledge and Data Engineering 15(2), 368–385
(March/April 2003)
15. Janhunen, T., Niemelä, I., Seipel, D., Simons, P., You, J.H.: Unfolding Partiality and Disjunc-
tions in Stable Model Semantics. ACM Transactions on Computational Logic 7(1), 1–37 (Jan
2006)
16. Leone, N., Gottlob, G., Rosati, R., Eiter, T., Faber, W., Fink, M., Greco, G., Ianni, G., Kałka,
E., Lembo, D., Lenzerini, M., Lio, V., Nowicki, B., Ruzzi, M., Staniszkis, W., Terracina, G.:
The INFOMIX System for Advanced Integration of Incomplete and Inconsistent Data. In:
Proceedings of the 24th ACM SIGMOD International Conference on Management of Data
(SIGMOD 2005). pp. 915–917. ACM Press, Baltimore, Maryland, USA (Jun 2005)
17. Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV
System for Knowledge Representation and Reasoning. ACM Transactions on Computational
Logic 7(3), 499–562 (Jul 2006)
18. Lierler, Y.: Disjunctive Answer Set Programming via Satisfiability. In: Baral, C., Greco,
G., Leone, N., Terracina, G. (eds.) Logic Programming and Nonmonotonic Reasoning —
8th International Conference, LPNMR’05, Diamante, Italy, September 2005, Proceedings.
LNCS, vol. 3662, pp. 447–451. Springer Verlag (Sep 2005)
19. Lifschitz, V., Turner, H.: Splitting a Logic Program. In: Van Hentenryck, P. (ed.) Proceedings
of the 11th International Conference on Logic Programming (ICLP’94). pp. 23–37. MIT
Press, Santa Margherita Ligure, Italy (Jun 1994)
20. Manna, M., Ruffolo, M., Oro, E., Alviano, M., Leone, N.: The HiLeX System for Semantic
Information Extraction. Transactions on Large-Scale Data and Knowledge-Centered Sys-
tems (2011), to appear
21. Manna, M., Scarcello, F., Leone, N.: On the complexity of regular-grammars with integer
attributes. Journal of Computer and System Sciences (JCSS) 77(2), 393–421 (2011)
22. Oetsch, J., Tompits, H., Woltran, S.: Facts do not cease to exist because they are ignored:
Relativised uniform equivalence with answer-set projection. In: Proceedings of the 22nd
National Conference on Artificial Intelligence (AAAI’07). pp. 458–464. AAAI Press (2007)
23. Papadimitriou, C.H., Yannakakis, M.: Tie-breaking semantics and structural totality. Journal
of Computer and System Sciences 54(1), 48–60 (1997)
24. Ricca, F., Alviano, M., Dimasi, A., Grasso, G., Ielpa, S.M., Iiritano, S., Manna, M., Leone,
N.: A Logic-Based System for e-Tourism. Fundamenta Informaticae 105(1–2), 35–55 (2010)
25. Ricca, F., Grasso, G., Alviano, M., Manna, M., Lio, V., Iiritano, S., Leone, N.: Team-building
with answer set programming in the Gioia-Tauro seaport. Theory and Practice of Logic Pro-
gramming (2011), to appear, doi:10.1017/S147106841100007X
26. Ullman, J.D.: Principles of Database and Knowledge Base Systems. Computer Science Press
(1989)