On Solution Correspondences in Answer-Set Programming

1 Introduction

With the availability of ef�cient implementations of the answer-set semantics [Gelfond and Lifschitz, 1991] for nonmonotonic logic programs, answer-set programming (ASP) has been recognized as a fruitful paradigm for declarative problem solving. In this approach, a problem is encoded as a logic program such that its models, called answer sets, correspond to the solutions of the problem, which can be easily extracted from them. Due to the availability of default negation, ASP has become an important host for solving many AI problems, including planning, diagnosis, information integration, and inheritance reasoning (cf. Gelfond and Leone [2002] for an overview on ASP).

To support engineering of ASP solutions, an important issue is determining equivalence of different encodings, given by two programs. To this end, various notions of equivalence between programs under the answer-set semantics have been studied in the recent past, viz. strong equivalence [Lifschitz et al., 2001], uniform equivalence [Eiter and Fink, 2003], and relativized notions thereof [Woltran, 2004], as well as update equivalence [Inoue and Sakama, 2004]. Informally, the former notions consider programs P and Q to be equivalent, if P ∪ R and Q ∪ R have always the same answer sets, where R is a set of rules from a particular collection of rules. Thus, if R is regarded as possible input, equivalent P and Q are guaranteed to compute always the same answer sets. Note that also open logic programs [Bonatti, 2001], in which part of the rules are to be added at runtime, �t within this scheme.

∗This work was supported by the Austrian Science Fund under grant P18019, and by the EC via projects FET-2001-37004 WASP, IST-2001-33570 INFOMIX, and IST-2001-33123 CologNeT.

However, none of these works have considered the practicably important setting of projected answer sets in ASP. Here, not a whole answer set of a program P is of interest, but only its intersection on a subset B ⊆ U of all letters; this includes, in particular, removal of auxiliary letters in computation. For a simple example, consider the programs

They should select, by means of sel , one element satisfying s in their answer sets. Here, an important issue is whether the programs are equivalent with respect to the �output� predicate sel, for all �inputs� s, where s may be de�ned by rules over predicates from a set A, say, or given by facts.

Another aspect is that, apart from equivalence, other relationships between the sets of answer sets of P and Q might be of interest. A natural example is inclusion, which means that each answer set of P is also an answer set of Q. Here Q can be viewed as an approximation of P , which is sound with respect to cautious reasoning from P.

Motivated by these observations, in this paper, we consider solution correspondences in ASP at a generic level. Our main contributions are brie�y summarized as follows.

1. We introduce a general framework for correspondences between the answer sets of programs P and Q, which are augmented by further rules from a context C of possible extensions, where the correspondence is determined by a binary relation ρ. Previous notions of equivalence and projected answer sets amount to particular instances of this framework.
2. We provide characterizations of inclusion correspondence and equivalence between programs under projected answer sets, in terms of novel semantical structures, called spoilers, which refute this property, and certi�cates, which

capture the essence of equivalence, similar as SE-models and UE-models do for strong and uniform equivalence, respectively. Based on these characterizations, we present interesting correspondence results on varying projection sets in ASP.

(3) We show how spoilers can be used to construct counterexamples to an inclusion resp. equivalence correspondence, consisting of a suitable interpretation M and a rule set R such that M is an answer set of exactly one of P ∪ R and Q ∪ R.

(4) Finally, we determine the computational complexity of correspondence checking for propositional disjunctive programs under projected answer sets. Our main result is that equivalence checking is ΠP4 -complete in general, and thus feasible in polynomial space as compared to a naive guessand-check procedure which requires exponential space. Furthermore, we show that for restricted settings, the complexity gradually decreases fromΠP4 to coNP.

The results presented in this paper signi�cantly advance the current state of equivalence testing in ASP towards highly relevant settings for practical applications, and provide novel insight into the structure of equivalent programs. Besides the papers quoted above, further related work mostly addresses semantic and complexity characterizations of equivalence [Lin, 2002; Turner, 2003], or describes implementation methods [Eiter et al., 2004; Oikarinen and Janhunen, 2004]. The recent work by Pearce and Valverde [2004] addresses strong equivalence of programs over disjoint alphabets which are synonymous under structurally de�ned mappings.

The characterizations we present are non-trivial and, as shown by our complexity results, necessarily involved in the sense that no �simple� criteria exist. Together with counterexamples, they provide a basis for powerful program optimization and debugging tools for ASP, which are lacking to date.

2 Preliminaries

We deal with propositional disjunctive logic programs, which are �nite sets of rules of form

a1 ∨ · · · ∨ al ← al+1, . . . , am, not am+1, . . . , not an, (1) n≥m≥l≥0, where all ai are propositional atoms and not denotes default negation; for n = l = 1, we usually identify the rule with the atom a1. If all atoms occurring in a program P are from a given set A of atoms, we say that P is a program over A. The set of all programs over A is denoted by PA. We call a rule (resp., program) normal iff it contains no disjunction ∨. A program is unary if it contains only rules of the form a ← b or a ←; P un A denotes the set of all unary programs over A. For a set of atoms A = {a1, . . . , am}, not A denotes the set {not a1, . . . , not am}. Accordingly, rules of form (1) will also be written as a1 ∨ · · · ∨ al ← B1, not B2, where B1 = {al+1, . . . , am} and B2 = {am+1, . . . , not an}.

Following Gelfond and Lifschitz [1991], an interpretation I, i.e., a set of atoms, is an answer set of a program P iff it is a minimal model of the reduct P I , which results from P by (i) deleting all rules containing default negated atoms not a such that a ∈ I and (ii) deleting all default negated atoms in the remaining rules. The set of all answer sets of a program P is denoted by AS(P). The relation I |= P between an interpretation I and a program P is de�ned as usual.

Under the answer-set semantics, two programs P and Q are regarded as (ordinarily) equivalent iff AS(P) = AS(Q). The more restrictive forms of strong equivalence [Lifschitz et al., 2001] and uniform equivalence [Eiter and Fink, 2003] have recently been generalized as follows [Woltran, 2004]: Let P, Q be programs over U, and let A ⊆ U. Then, P and Q are strongly (resp., uniformly) equivalent relative to A iff, for any R ∈ PA (resp., R ⊆ A), AS(P ∪ R) = AS(Q ∪ R).

If A=U, strong (resp., uniform) equivalence relative to A reduces to strong (resp., uniform) equivalence simpliciter; if A=∅, ordinary equivalence results in either case.

We use the following notation. For an interpretation I and a set S of (pairs of) interpretations, we write S|I = {Y ∩ I | Y ∈ S} (S|I = {(X∩I, Y ∩I) | (X, Y ) ∈ S}). If S = {s}, we write s|I instead of S|I , if convenient.

For any A ⊆ U and any Y ⊆ U, a pair (X, Y ) of interpretations is an A-SE-interpretation (over U) iff either X = Y or X ⊂ Y |A. (X, Y ) is an A-SE-model of a program P iff

A pair (X, Y ) is total iff X = Y , and non-total otherwise. The set of all A-SE-models of P is denoted by SE A(P).

For A = U, A-SE-interpretations (resp., A-SE-models) are simply called SE-interpretations (resp., SE-models), coinciding with the notions de�ned by Turner [2003], and we write SE(P) instead of SE U (P).

Proposition 1 ([Woltran, 2004]) Two programs P and Q are strongly equivalent relative to A iff SE A(P ) = SE A(Q).

Example 1 Consider the following two programs, P1 and P2, which we shall use as a running example:

Hence, P1 and P2 are not strongly equivalent. On the other hand, AS(P1) = AS(P2) = ∅, i.e., P1 and P2 are (ordinarily) equivalent. Moreover, P1 and P2 are strongly equivalent relative to A iff A ∩ {a, b} = ∅. For A = {a, b}, we get

3 General Framework

In order to deal with differing notions of program equivalence in a uniform manner, taking in particular the currently existing notions of equivalence, as presented above, as well as equivalence notions based on the projection of answer sets into account, we introduce a general framework for expressing solution correspondences between logic programs. In this framework, we parameterize, on the one hand, the set R of rules to be added to the programs P and Q, and, on the other hand, the relation that has to hold between the collection of answer sets of P ∪ R and Q ∪ R. Concerning the latter parameter, besides equality, other comparison relations like setinclusion may be used. This leads to the following notion:

1 We write abc instead of {a, b, c}, a instead of {a}, etc.

De�nition 1 By a correspondence frame, or simply frame, F, we understand a triple (U, C, ρ), where (i) U is a set of atoms, called the universe of F, (ii) C ⊆ PU, called the context programs of F, or simply the context, and (iii) ρ ⊆ 22U ×22U .

For all programs P,Q ∈ PU, we say that P and Q are F-corresponding, symbolically P ≃F Q, iff, for all R ∈ C, (AS(P ∪ R), AS(Q ∪ R)) ∈ ρ.

Intuitively, in a correspondence frame F = (U, C, ρ), U determines the general alphabet under consideration, C determines the kind of rules used for comparison, and ρ is the speci�c operation used for checking the correspondence of two programs.

It is quite obvious that the equivalence notions discussed above are special cases of F-correspondence. Indeed, for any universe U and any A ⊆ U, we have that strong equivalence relative to A coincides with (U, PA, =)-correspondence, and uniform equivalence relative to A coincides with (U, 2A, =)- correspondence. Consequently, it holds that (i) strong equivalence coincides with (U,PU,=)-correspondence, (ii) uniform equivalence coincides with (U, 2U , =)-correspondence, and (iii) ordinary equivalence coincides with (U, {∅},=)- correspondence.

In this paper, we are mainly concerned with correspondence frames of form (U,PA,⊆B) and (U,PA,=B), where A ⊆ U is some set of atoms, and ⊆B and =B are projections of the standard subset and set-equality relation, respectively, to a set B ⊆ U, de�ned as follows: for sets S, S ′ of interpretations,

• S ⊆B S ′ iff S|B ⊆ S ′ |B, and
• S =B S ′ iff S|B = S ′ |B.

In particular, =B amounts to answer-set existence if B = ∅, and to correspondence between answer sets if B = U.

In what follows, if F is of the form (U, C,=B), we refer to F also as an equivalence frame, and, accordingly, to Fcorrespondence also as F-equivalence. As well, a frame of the form (U, C, ⊆B) is also referred to as an inclusion frame.

For later purposes, we also introduce the following notion: A correspondence problem, Π, over U, is a quadruple (P,Q, C, ρ), where P,Q ∈ PU and (U, C, ρ) is a frame. We say that Π holds iff P ≃(U,C,ρ) Q holds. In accord with the above designations, we call Π an equivalence problem if (U, C, ρ) is an equivalence frame and an inclusion problem if (U, C, ρ) is an inclusion frame.

For a correspondence problem Π = (P,Q, C, ρ) over U, we usually leave U implicit, assuming that it consists of all atoms occurring in P , Q, and C.

We next list some basic properties of F-equivalence.

Proposition 2 Let (U, C,=B) be an equivalence frame and P, Q ∈ PU . Then, the following conditions hold:

1. If P ≃(U,C,=B) Q, then P ≃(U,C′ ,=B′ ) Q, for all C ′ ⊆ C and all B′ ⊆ B.

We recall an important result due to Woltran [2004], extending an analogous result by Lifschitz et al. [2001].

Proposition 3 Consider a frame (U, PA, =), for A ⊆ U, and let P, Q ∈ PU . Then, P ≃(U,PA,=) Q iff P ≃(U,P un

A ,=) Q. Example 2 We have already seen that for P1, P2 from Ex-

ample 1, P1 ̸≃(U,PA,=) P2 holds, for A = {a, b} and U = {a, b, c, d}. Hence, by Proposition 3, P1 ̸≃(U,P un A ,=) P2. This is witnessed by the fact that, e.g., AS(P1∪{a}) = {abc, abd} while AS(P2 ∪ {a}) = {abc}.

The relevance of Proposition 3 is that it allows to drastically reduce the number of required rules for equivalence checking. However, the proposition does not generalize to projections of answer sets.

Theorem 1 For any equivalence frame (U,PA,=B) with A,B ⊆ U, and any P,Q ∈ PU, if P ≃(U,PA,=B) Q, then P ≃(U,P un A ,=B) Q, but the converse does not hold in general. Proof. That P≃(U,PA,=B)Q implies P≃(U,P un A ,=B)Q is immediate from Part 1 of Proposition 2. Our running example shows the failure of the converse: P1 ≃(U,P un A ,=B) P2 holds, where U ={a, b, c, d} and A = B = {a, b}, but P1̸≃(U,PA,=B)P2. The latter holds in view of AS(P1 ∪ {a∨b ←}) = {abc, abd} but AS(P2 ∪ {a∨b ←}) = ∅, as easily shown. ✷

The above theorem also holds if the set P un A is substituted by the class of all normal programs over A. Indeed, programs P1 and P2 of our running example are corresponding with respect to a frame using normal programs over A = {a, b} as context, because in each stable model of P1 ∪R resp. P2 ∪R, both a and b must be true. Thus, rules in R (⊆ PA) with negative literals in the body are immaterial.

Theorem 1 indicates that equivalence for projected answer sets is more involved. The same holds for inclusion, since as an easy corollary to Theorem 1, P ≃(U,PA,⊆B) Q implies P ≃(U,P un A ,⊆B) Q, but not vice versa. In fact, the next result shows that, in general, a smallest extension R violating inclusion has exponential size.

Theorem 2 There exists a family of problems Π = (P,Q, PA, ⊆A) such that each R ⊆ PA witnessing AS(P ∪R)|A ̸⊆ AS(Q∪R)|A is exponential in the size of P and Q.

Proof (Sketch). The idea is to encode a propositional CNF φ = ∧ni=1 Ci over atoms V , for Ci = ci,1 ∨ · · · ∨ ci,ki , into Π = (P,Q,PA,⊆A) such that, for any R ∈ PA, AS(P ∪ R)|A ̸⊆ AS(Q ∪ R)|A and ¬ ˜R must include a DNF for φ, where ˜R is the result of interpreting R as a classical formula.

Let ¯ V = {¯ v | v ∈ V }, V ′ = {v′ | v ∈ V }, ¯ V ′ = {¯ v′ | v ∈ V }, and G = {g1, . . . , gn} be sets of new atoms. We de�ne

where C ∗ i = c∗i,1 , . . . , c∗i,ki , v∗ = ¯ v, and (¬v)∗ = v, and

with ̂ v=v′ and ̂ ¬v = ¯ v′ . Let A = V ∪ ¯ V . Informally, P ∪R only admits answer sets containing A, and indeed it holds that (A, A) ∈ SE(P ∪R)|A\SE(Q∪R)|A, for some R. For any such R, the SE-models (X, A) with X ⊂ A must be precisely those where X is a countermodel of φ. This means that ˜RA is a CNF for ¬φ, and thus ¬ ˜RA amounts to a DNF for φ. This proves the claim. Now, as well-known, the smallest DNF for a CNF φ can be exponential in φ, which proves the result. ✷

We can similarly construct a family of problems showing that a smallest extension R violating equivalence has exponential size. Hence, a naive guess and check algorithm to disprove inclusion or equivalence needs exponential space. For a better algorithm, we have to develop suitable semantical characterizations, which must take disjunctive extensions into account.

4 Characterizations

In this section, we �rst present some characteristic structures associated with inclusion and equivalence problems under projections of answer sets, termed spoilers and certi�cates. Based on them, we then discuss some interesting invariance results.

We start with some general properties.

De�nition 2 A set S of SE-interpretations is complete iff, for each (X, Y ) ∈ S, also (Y, Y ) ∈ S as well as (X, Z) ∈ S, for any Y ⊆ Z with (Z, Z) ∈ S.

It can be shown that the set SE(P) of all SE-models of a program P is always complete.

The following guarantees that a complete set S of SEinterpretations can be represented by some program P .

Proposition 4 Let S be a complete set of SE-interpretations, and let A be a set of atoms. Then, there exists a program PS,A ∈ PA such that SE(PS,A)|A = S|A.

One possibility to obtain PS,A from S is as follows: take rules ← Y, not (A \ Y ), for each Y ⊆ A such that (Y, Y ) /∈ S|A, and rules ∨p∈(Y \X) p ← X, not (A\ Y ), for each X ⊂ Y such that (X, Y ) /∈ S|A and (Y, Y ) ∈ S|A.

4.1 Spoilers

The �rst class of characteristic structures associated with program correspondence we are dealing with are of such a nature that their existence prevents the equivalence of programs under projected answer sets.

We need the following auxiliary notation: Let S be a set of SE-interpretations and Y , C sets of atoms. Then, σC Y (S) = {(X, Z) ∈ S | Z|C = Y |C}.

De�nition 3 Let Π = (P, Q, PA, ⊆B) be an inclusion problem over U, let Y ⊆ U be an interpretation, and consider S ⊆ σA∪B Y (SE A(Q)). The pair (Y, S) is a spoiler for Π iff

• (i) (Y, Y ) ∈ SE A(P),
• (ii) for each (Z,Z) ∈ S, some non-total (X,Z) ∈ S exists,

Intuitively, in a spoiler (Y, S), the interpretation Y is an answer set of P ∪R but not of Q∪R, for some R, which is semantically given by S.

Example 3 For P1 and P2 from our running example and A = {a, b}, (Y1, S) and (Y2, S) are the only spoilers for (P1, P2,PA,⊆A), where Y1 = {abc}, Y2 = {abd}, and S = {(a, abd), (b, abc), (abc, abc), (abd, abd)}, with the latter being a subset of σA Y1 (SE A(P2)) = σA Y2 (SE A(P2)) = S ∪ {(∅,abc), (∅,abd)}, as required in De�nition 3.

The central property of spoilers is as follows:

Theorem 3 Let F = (U, PA, ⊆B) be a frame. Then, for any P, Q∈PU , P ≃F Q iff there is no spoiler for (P, Q, PA, ⊆B).

An immediate consequence of this theorem, together with Part 2 of Proposition 2, is the following result:

Corollary 1 Let F = (U, PA, =B) be an equivalence frame and P,Q ∈ PU. Then, P ≃F Q iff neither (P,Q,PA,⊆B) nor (Q, P, PA, ⊆B) has a spoiler.

As discussed later on, spoilers provide a semantical basis for counterexample generation.

4.2 Certi�cates

After having introduced structures which disprove program correspondence, we now discuss structures which prove program correspondence. Roughly speaking, the structures introduced below express the essence of a program P , with respect to program equivalence, in terms of a semantic condition on P alone.

De�nition 4 Let C be a set of atoms and S a set of SEinterpretations. A pair (X, Y ), where X is a set of interpretations and Y ⊆ C, is a C-projection of S iff there exists some set Z such that (i) (Z,Z) ∈ S, (ii) Z|C = Y |C, and (iii) X = {X | (X, Z) ∈ S,X⊂Z}.

For a program P, we call an (A ∪ B)-projection of SE A(P ) an (A, B)-certi�cate of P .

The following lemma can be shown by means of spoilers, and expresses that programs are corresponding with respect to inclusion frames iff their certi�cates satisfy a certain containment relation.

Lemma 1 Correspondence of (P,Q,PA,⊆B) holds, iff for each (A,B)-certi�cate (X, Y ) of P, an (A,B)-certi�cate (X ′ , Y ) of Q exists with X ′ ⊆ X .

The next result expresses the central property of certi�- cates. Towards its formulation, we require a further concept: An (A,B)-certi�cate (X,Y ) of a program P is minimal iff, for any (A,B)-certi�cate (Z,Y ) of P , Z⊆X implies Z=X .

Theorem 4 Let F = (U, PA, =B) be an equivalence frame. Then, for any P,Q ∈ PU, P ≃F Q iff the minimal (A,B)- certi�cates of P and Q coincide.

Note that this result is the pendant to Proposition 1, which deals with a model-theoretic characterization of relativized strong equivalence. Indeed, two programs P,Q ∈ PU are strongly equivalent relative to A iff their minimal (A, U)- certi�cates coincide. Some further relations between program correspondence and relativized and non-relativized strong equivalence, respectively, are given in the next subsection.

Example 4 In our running example with A = B = {a, b}, we get that P1 has a single (A,A)-certi�cate, ({∅}, {ab}), while P2 has two (A,A)-certi�cates, ({∅, {a}}, {ab}) and ({∅, {b}}, {ab}), all of them minimal. Since they do not coincide, we obtain that P1 and P2 are not (U,PA,=A)- equivalent, as expected.

4.3 Invariance Results

Theorem 4 allows us to derive some interesting invariance results with respect to varying projection sets B.

Theorem 5 Let U be a set of atoms and A, B ⊆ U. Then, for any P, Q ∈ PU , P ≃(U,PA,=B) Q iff P ≃(U,PA,=A∪B) Q.

This result follows immediately from Theorem 4 and De�- nition 4, by observing that (A, B)-certi�cates of a program P and (A, A∪B)-certi�cates of P are actually identical objects, since (A∪B)-projections of SE A(P) trivially coincide with (A ∪ (A ∪ B))-projections of SE A(P ).

Theorem 5 has several interesting consequences.

Corollary 2 For programs P,Q and any set A of atoms, (P,Q,PA,=∅) holds iff (P,Q,PA,=A) holds.

That is, answer-set existence (which is relevant regarding Boolean properties) relative to additions from PA is tantamount to relativized strong equivalence under projection to A.

Corollary 3 Let U be a set of atoms. Then, for any programs P, Q ∈ PU and any set B ⊆ U of atoms, P ≃(U,PU ,=B) Q iff P and Q are strongly equivalent.

This result is quite striking as it shows that strong equivalence corresponds to (U,PU,=B)-equivalence, for any projection set B. It is derived from the fact that, for any B, the (U,B)- certi�cates of a program P are in a one-to-one correspondence to the SE-models of P as follows: ({X1, . . . , Xm}, Y ) is a (U, B)-certi�cate of P iff (X1, Y ), . . . , (Xm, Y ), (Y, Y ) are all the SE-models of P with �xed second component Y .

In particular, consistency under answer-set semantics (i.e., if B = ∅) coincides with strong equivalence. More generally:

Corollary 4 Let U be a set of atoms. Then, for all programs P,Q ∈ PU and all sets A and B of atoms such that A ∪ B = U, P ≃(U,PA,=B) Q iff P and Q are strongly equivalent relative to A.

In fact, in this setting, a correspondence between A-SEmodels of a program and its (A,B)-certi�cates is analogously established as above.

5 Counterexamples

Given that a correspondence problem Π = (P,Q,PA,⊆B) does not hold, it is interesting to know why this is the case. We de�ne a counterexample for Π as a pair (R,M), where

• R ∈ PA such that AS(P ∪R) ̸⊆BAS(Q∪R), and
• M ∈ AS(P ∪ R) and M|B /∈ AS(Q ∪ R)|B.

Furthermore, a counterexample for an equivalence problem (P,Q,PA,=B) is any counterexample for either (P,Q, PA, ⊆B) or (Q, P, PA, ⊆B).

Our notion of a spoiler from De�nition 3 provides a basis for such counterexamples.

Theorem 6 Suppose (Y, S) is a spoiler for a correspondence problem Π = (P,Q,PA,⊆B). Then, (PS,A, Y ) is a counterexample for Π, where PS,A is as in Proposition 4.

This result follows from Theorem 3 and Proposition 4 by the fact that S|A is complete for any spoiler (Y, S).

Example 5 For our example and the sketched construction after Proposition 4, we derive counterexamples (R, {abc}) and (R, {abd}), where R = {a ∨ b ← ; ← not a;← not b; ← not a, not b}; obviously, the last rule is redundant.

Note that if an inclusion problem (P,Q,PA,⊆B) fails, some counterexample as in Theorem 6 does exist.

We observe that the programs in the counterexamples of Theorem 6 may contain redundant clauses, as succinctness is not a concern of spoilers. For instance, in our example, R′ = {a ∨ b ←} would yield a simpler counterexample. In fact, spoilers are not geared towards providing minimal counterexamples with respect to particular syntactic subclasses of contexts.

Towards facilitating special counterexamples, we may extend the notion of a spoiler to pairs (Y, S), where S ̸⊆ σA∪B Y (SE A(Q)) is admitted for complete S, by replacing in De�nition 3 the set S in (ii) with S ∩ σB Y (SE A(Q)) and in (iii) and (iv) with S ∩ σA∪B Y (SE A(Q)), calling the result an extended spoiler.

Example 6 In our running example, Π=(P1, P2,PA,⊆A) has spoilers ({abc}, S) and ({abd}, S), with S = {(a, abd), (b, abc), (abc, abc), (abd, abd)}. Since both (ab, ab) ̸∈ SE A(P2) and (abcd, abcd) ̸∈ SE A(P2), one can verify that any complete superset S ′ of S not containing any (∅,Z), with Z|A = {ab}, yields extended spoilers ({abc}, S ′ ) and ({abd}, S ′ ). In particular, we may set S ′ = S ∪ {(a, a), (b, b)}. Note that S ′ |A = {(a, a), (a, ab), (b, b), (b, ab), (ab, ab)}. Now, the simpler program R′ = {a ∨ b ←} ful�lls SE(R′ )|A = S ′ |A; thus, (R′ , {abc}) and (R′ , {abd}) are counterexamples for Π.

Theorems 3 and 6 generalize to extended spoilers. More counterexamples can be constructed using such spoilers in general, which may include a counterexample of particular form. In our example, adding {(a, a), (b, b)} to an ordinary spoiler allowed us to give a counterexample program which is positive. On the other hand, we can show that no counterexample program which is normal exists (as no (∅, Z) with Z|A = {ab} can be added). An elaboration of this issue remains for further work.

6 Computational Complexity

Our �rst result is concerned with recognizing whether an interpretation is a discriminating answer set for the extended programs P ∪ R and Q ∪ R, i.e., a �partial� spoiler.

Lemma 2 Given programs P and Q, sets A and B of atoms,

and an interpretation Y , deciding whether (P,Q,PA,⊆B) has some spoiler whose �rst component is Y is ΠP3 -complete. Proof (Sketch). We show ΣP3 -membership of deciding that no spoiler of form (Y, S) exists. By De�nition 3, it suf�ces to check whether (a) (Y, Y ) /∈ SE A(P) or (b) whether there exists a (Z,Z) ∈ σA∪B Y (SE A(Q)) such that each non-total (X,Z) ∈ SE A(Q) implies (X, Y ) ∈ SE A(P). Part (a) is feasible in polynomial time with an NP oracle. For Part (b), note that given Y and Z, checking whether, for each nontotal (X,Z) ∈ SE A(Q) also (X, Y ) ∈ SE A(P), is in ΠP2 . Therefore, Part (b) is in ΣP3 , and the entire test is in ΣP3 .

The ΠP3 -hardness is shown by a sophisticated reduction from suitable quanti�ed Boolean formulas (QBFs), using machinery from the exponential counterexample construction which was used for showing Theorem 2. ✷

From this result, we can easily derive the membership part of our main complexity result given below; its hardness part is again shown by an encoding of QBFs.

Theorem 7 Given programs P and Q and sets A and B of atoms, deciding whether (P,Q,PA,⊆B) holds is ΠP4 -complete. Moreover, ΠP4 -hardness holds even for B = ∅, i.e., for answer-set existence.

For the particular case where B = A, which constitutes the setting where auxiliary letters are used in logic programs, we obtain in combination with Theorem 5 the same complexity.

Notice that the �partial� spoiler of Lemma 2 avoids a naive guess of a (possibly exponentially large) full spoiler (Y, S) which proves the failure of (P, Q, PA, ⊆B), at the expense of checking involved conditions on SE A(P) and SE A(Q).

The above results for inclusion problems carry over to equivalence problems, since they are polynomially intertranslatable, as seen by Part 2 of Proposition 2 and the following fact:

Proposition 5 P ≃(U,PA,⊆B) Q iff Q ≃(U,PA,=B) LP,Q, where LP,Q = {gP ∨ gQ ←; ← gP , gQ} ∪ {H ← gR, B | R ∈ {P, Q}, H ← B ∈ R} and gP , gQ are new atoms.

This holds by virtue of Lemma 1 and Theorem 4, and the fact that the (A, B)-certi�cates of LP,Q are those of P and Q.

If the size of each program in the context C is polynomially bound by the size of the compared programs P and Q (as is the case for ordinary and uniform equivalence), the complexity is lower. Let us call such problems (P, Q, C, ρ) bound.

Theorem 8 Given programs P and Q, a context C, a set B of atoms, such that Π = (P,Q, C,⊆B) is bound, deciding whether Π holds is ΠP3 -complete. ΠP3 -hardness holds even for C = {∅}, i.e., for ordinary equivalence with projection.

For other instances of the framework, the complexity is even lower.

Theorem 9 Given programs P and Q over U and sets A and B of atoms, deciding whether (P,Q,PA,=B) holds is (i) coNP-complete if A = U, and (ii) ΠP2 -complete if (A ∪ B) = U.

This result follows from the invariance results in Section 4.2 and complexity results due to Woltran [2004].

7 Conclusion and FurtherWork

We have presented a general framework for expressing solution correspondences between nonmonotonic logic programs, and have then developed semantic characterizations of inclusion and equivalence problems under projected answer sets within a context of possible changes. As we have shown, they match the intrinsic complexity of the problem.

Our results provide a semantical basis for developing optimization and debugging techniques, which are lacking at present but vital for further enhancements of ASP as a programming paradigm.

Several issues remain for future work. One is to extend our study to different classes of contexts and compared programs, and to provide suitable semantical and complexity characterizations. Another issue concerns the construction of �good� counterexamples, according to their possible form. Finally, exploring other notions of correspondences than =B and ⊆B in the general framework is an intriguing issue.