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)