Declarative and Computational Properties of Logic Programs with Aggregates

1 Introduction

The introduction of aggregates atoms [Kemp and Stuckey, 1991; Denecker et al., 2001; Gelfond, 2002; Simons et al., 2002; Dell'Armi et al., 2003; Pelov and Truszczy·nski, 2004; Pelov et al., 2004] is one of the major linguistic extensions to Answer Set Programming of the recent years.

While both semantic and computational properties of standard (aggregate-free) logic programs have been deeply investigated, only few works have focused on logic programs with aggregates; their behaviour, their semantic properties, and their computational features are still far from being fully clari�ed. A recent proposal for answer set semantics is receiving a consensus [Faber et al., 2004]. However, unfounded sets and the well-founded operator [Van Gelder et al., 1991], which are important for both the characterization and the computation of standard LPs [Leone et al., 1997; Simons et al., 2002; Calimeri et al., 2002; Koch et al., 2003; Pfeifer, 2004], have not been de�ned in a satisfactory manner for logic programs with aggregates. Moreover, the impact of aggregates on the computational complexity of the reasoning tasks has not been analyzed in depth.

∗This work was partially supported by the EC under projects IST2002-33570 INFOMIX and IST-2001-37004 WASP, and by FWF under projects P16536-N04 and P17212-N04.

† Funded by APART of the Austrian Academy of Sciences.

This paper makes a �rst step to overcome this de�ciency, improving the characterization of programs with aggregates, for both declarative and computational purposes. The main contributions of the paper are as follows.

• We de�ne the notion of unfounded set for logic programs with both monotone and antimonotone aggregates (LPAm,a programs). This notion is a sound generalization of the concept of unfounded sets previously given for programs without aggregates. We show that our de�nition coincides with the original de�nition of unfounded sets of [Van Gelder et al., 1991] on the class of normal (aggregate-free) programs, and shares its nice properties (like, e.g., the existence of the greatest unfounded set).
• We provide a declarative characterization of answer sets in terms of unfounded sets. In particular, answer sets are precisely unfounded-free models of an LPAm,a program.
• We de�ne a well-founded operator WP for logic programs with aggregates, which extends the classical well-founded operator [Van Gelder et al., 1991]. The total �xpoints of WP are exactly the answer sets of P, and its least �xpoint W ω P (∅) is contained in the intersection of all answer sets. Importantly, Wω P (∅) is polynomial-time computable.
• We analyze the complexity of logic programs with arbitrary (also nonmonotone) aggregates and fragments thereof. Both monotone and antimonotone aggregates do not affect the complexity of answer set semantics, which remains coNP-complete (for cautious reasoning). Nonmonotone aggregates, instead, do increase the complexity, jumping to the second level of the polynomial hierarchy (ΠP2 ).

For space limitations, some proofs are sketched.

2 Logic Programs with Aggregates

In this section, we recall syntax, semantics, and some basic properties of logic programs with aggregates.

2.1 Syntax

We assume that the reader is familiar with standard LP; we refer to atoms, literals, rules, and programs of LP, as standard atoms, standard literals, standard rules, and standard programs, respectively. Two literals are said to be complementary if they are of the form p and not p for some atom p. Given a literal L, ¬.L denotes its complementary literal. Accordingly, given a set A of literals, ¬.A denotes the set {¬.L | L ∈ A}. For further background, see [Baral, 2002; Gelfond and Lifschitz, 1991].

Set Terms. A (LPA) set term is either a symbolic set or a ground set. A symbolic set is a pair {Vars : Conj }, where Vars is a list of variables and Conj is a conjunction of standard atoms. 1 A ground set is a set of pairs of the form 〈t :Conj 〉, where t is a list of constants and Conj is a ground (variable free) conjunction of standard atoms.

Aggregate Functions. An aggregate function is of the form f(S), where S is a set term, and f is an aggregate function symbol. Intuitively, an aggregate function can be thought of as a (possibly partial) function mapping multisets of constants to a constant.

Example 1 (In the examples, we adopt the syntax of DLV to denote aggregates.) Aggregate functions currently supported by the DLV system are: #count (number of terms), #sum (sum of non-negative integers), #times (product of positive integers), #min (minimum term, unde�ned for empty set), #max (maximum term, unde�ned for empty set) 2 .

Aggregate Literals. An aggregate atom is f(S) ≺ T, where f(S) is an aggregate function, ≺∈ {=, <, ≤,>,≥} is a prede�ned comparison operator, and T is a term (variable or constant) referred to as guard.

Example 2 The following aggregate atoms in DLV notation, where the latter contains a ground set and could be a ground instance of the former:

#max{Z : r(Z), a(Z, V )} > Y #max{〈2 : r(2), a(2, k)〉, 〈2 : r(2), a(2, c)〉} > 1

An atom is either a standard (LP) atom or an aggregate atom. A literal L is an atom A or an atom A preceded by the default negation symbol not; if A is an aggregate atom, L is an aggregate literal.

LPA Programs. A (LPA) rule r is a construct

a :- b1, · · · , bk, not bk+1, · · · , not bm.

where a is a standard atom, b1, · · · , bm are atoms, and m ≥ k ≥ 0. The atom a is referred to as the head of r while the conjunction b1, ..., bk, not bk+1, ..., not bm is the body of r. We denote the head atom by H(r), and the set {b1, ..., bk, not bk+1, ..., not bm} of the body literals by B(r).

1 Intuitively, a symbolic set {X : a(X, Y ), p(Y )} stands for the set of X-values making a(X, Y ), p(Y ) true, i.e., {X |∃Y s.t . a(X, Y ), p(Y ) is true}.

2 The �rst two aggregates correspond, respectively, to the cardinality and weight constraint literals of Smodels.

A (LPA) program is a set of LPA rules. A global variable of a rule r is a variable appearing in a standard atom of r; all other variables are local variables.

Safety. A rule r is safe if the following conditions hold: (i) each global variable of r appears in a positive standard literal in the body of r; (ii) each local variable of r appearing in a symbolic set {Vars : Conj } appears in an atom of Conj ; (iii) each guard of an aggregate atom of r is a constant or a global variable. A program P is safe if all r ∈ P are safe. In the following we assume that LPA programs are safe.

2.2 Answer Set Semantics

Universe andBase. Given a LPA programP, let UP denote the set of constants appearing in P, and BP be the set of standard atoms constructible from the (standard) predicates of P with constants in UP. Given a set X, let 2X denote the set of all multisets over elements from X. Without loss of generality, we assume that aggregate functions map to I (the set of integers).

Example 3 #count is de�ned over 2UP, #sum over 2N, #times over 2N+, #min and #max are de�ned over 2N-{∅}.

Instantiation. A substitution is amapping froma set of variables to UP. A substitution from the set of global variables of a rule r (to UP) is a global substitution for r; a substitution from the set of local variables of a symbolic set S (to UP) is a local substitution for S. Given a symbolic set without global variables S = {Vars : Conj }, the instantiation of S is the following ground set of pairs inst(S):

{〈γ(Vars) : γ(Conj )〉 | γ is a local substitution for S}. 3 A ground instance of a rule r is obtained in two steps: (1) a global substitution σ for r is �rst applied over r; (2) every symbolic set S in σ(r) is replaced by its instantiation inst(S). The instantiation Ground(P) of a program P is the set of all possible instances of the rules of P.

Example 4 Consider the following programP1: q(1) ∨ p(2, 2). q(2) ∨ p(2, 1). t(X):-q(X),#sum{Y : p(X, Y )} > 1. The instantiation Ground(P1) is the following: q(1) ∨ p(2, 2).t(1):-q(1), #sum{〈1 : p(1, 1)〉, 〈2 : p(1, 2)〉}>1. q(2) ∨ p(2, 1).t(2):-q(2), #sum{〈1 : p(2, 1)〉, 〈2 : p(2, 2)〉}>1.

Interpretations. An interpretation for a LPA programP is a consistent set of standard ground literals, that is I ⊆ (BP ∪ ¬.BP) such that I ∩ ¬.I = ∅. A standard ground literal L is true (resp. false) w.r.t I if L ∈ I (resp. L ∈ ¬.I). If a standard ground literal is neither true or false w.r.t I then it is unde�ned w.r.t I. We denote by I + (resp. I -) the set of all standard positive (resp. negative) literals occurring in I. We also denote with ¯ I the set of unde�ned standard literals w.r.t I. An interpretation I is total if ¯ I is empty (i.e., I + ∪¬.I - = BP), otherwise I is partial.

3 Given a substitution σ and a LPA object Obj (rule, set, etc.), we denote by σ(Obj) the object obtained by replacing each variable X in Obj by σ(X).

An interpretation also provides a meaning for aggregate literals. Their truth value is �rst de�ned for total interpretations, and then induced for partial ones.

Let I be a total interpretation. A standard ground conjunction is true (resp. false) w.r.t I if all its literals are true. The meaning of a set, an aggregate function, and an aggregate atom under an interpretation, is a multiset, a value, and a truth-value, respectively. Let f(S) be a an aggregate function. The valuation I(S) of S w.r.t. I is the multiset of the �rst constant of the elements in S whose conjunction is true w.r.t. I. More precisely, let I(S) denote the multiset [t1 | 〈t1, ..., tn : Conj 〉 ∈S∧ Conj is true w.r.t. I ]. The valuation I(f(S)) of an aggregate function f(S) w.r.t. I is the result of the application of f on I(S). If the multiset I(S) is not in the domain of f, I(f(S)) = ⊥ (where ⊥ is a �xed symbol not occurring in P). 4

An instantiated aggregate atom A = f(S) ≺ k is true w.r.t. I if: (i) I(f(S)) ̸= ⊥, and, (ii) I(f(S)) ≺ k holds; otherwise, A is false. An instantiated aggregate literal not A = not f(S) ≺ k is true w.r.t. I if (i) I(f(S)) ̸= ⊥, and, (ii) I(f(S)) ≺ k does not hold; otherwise, A is false.

If I is a partial interpretation, an aggregate literal A is true (resp. false) w.r.t. I if it is true (resp. false) w.r.t. each total interpretation J extending I (i.e., ∀ J s.t. I ⊆ J, A is true w.r.t. J); otherwise it is unde�ned.

Example 5 Consider the atom A = #sum{〈1 : p(2, 1)〉, 〈2 : p(2, 2)〉} > 1 from Example 4. Let S be the ground set in A. For the interpretation I = {p(2, 2)}, each extending total interpretation contains either p(2, 1) or not p(2, 1). Therefore, either I(S) = [2] or I(S) = [1, 2] and the application of #sum yields either 2 > 1 or 3 > 1, hence A is true w.r.t. I.

MinimalModels. Given an interpretation I, a rule r is satis�ed w.r.t. I if the head atom is true w.r.t. I whenever all body literals are true w.r.t. I. A total interpretation M is a model of a LPA program P if all r ∈ Ground(P) are satis�ed w.r.t. M. A model M for P is (subset) minimal if no model N for P exists such that N + ⊂ M +. Note that, under these definitions, the word interpretation refers to a possibly partial interpretation, while a model is always a total interpretation.

Answer Sets. We now recall the generalization of the Gelfond-Lifschitz transformation for LPA programs from [Faber et al., 2004].

De�nition 1 ([Faber et al., 2004]) Given a ground LPA program P and a total interpretation I, let P I denote the transformed program obtained from P by deleting all rules in which a body literal is false w.r.t. I. I is an answer set of a program P if it is a minimal model of Ground(P)I .

Example 6 Consider the following two programs:

P1 : {p(a):-#count{X : p(X)} > 0.} P2 : {p(a):-#count{X : p(X)} < 1.}

Ground(P1) = {p(a):-#count{〈a : p(a)〉} > 0.} and Ground(P2) = {p(a):-#count{〈a : p(a)〉} < 1.}, and interpretation I1 = {p(a)}, I2 = ∅. Then, Ground(P1)I1 =

4 In this paper, we assume that the value of an aggregate function can be computed in time polynomial in the size of the input multiset.

Ground(P1), Ground(P1)I2 = ∅, and Ground(P2)I1 = ∅, Ground(P2)I2 = Ground(P2) hold.

I2 is the only answer set of P1 (because I1 is not a minimal model of Ground(P1)I1 ), while P2 admits no answer set (I1 is not a minimal model of Ground(P2)I1 , and I2 is not a model of Ground(P2) = Ground(P2)I2 ).

Note that any answer set A of P is also a model of P because Ground(P)A ⊆ Ground(P), and rules in Ground(P) - Ground(P)A are satis�ed w.r.t. A.

Monotonicity. Given two interpretations I and J we say that I ≤ J if I + ⊆ J + and J - ⊆ I -. A ground literal ℓ is monotone, if for all interpretations I, J, such that I ≤ J, we have that: (i) ℓ true w.r.t. I implies ℓ true w.r.t. J, and (ii) ℓ false w.r.t. J implies ℓ false w.r.t. I. A ground literal ℓ is antimonotone, if the opposite happens, that is, for all interpretations I, J, such that I ≤ J, we have that: (i) ℓ true w.r.t. J implies ℓ true w.r.t. I, and (ii) ℓ false w.r.t. I implies ℓ false w.r.t. J. A ground literal ℓ is nonmonotone, if it is neither monotone nor antimonotone.

Note that positive standard literals are monotone, whereas negative standard literals are antimonotone. Aggregate literals may be monotone, antimonotone or nonmonotone, regardless whether they are positive or negative. Nonmonotone literals include the sum over (possibly negative) integers and the average.

Example 7 All ground instances of #count{Z : r(Z)} > 1 and not #count{Z : r(Z)} < 1 are monotone, while for #count{Z : r(Z)} < 1, and not #count{Z : r(Z)} > 1 they are antimonotone.

We denote by LPAm (LPAa /LPAn ) the fragment of LPA where only monotone (antimonotone/nonmonotone) aggregates are allowed; LPAm,a allows for both monotone and antimonotone aggregates.

Remark 1 Observe that our de�nitions of interpretation and truth values preserve �knowledge monotonicity�. If an interpretation J extends I (i.e., I ⊆ J), then each literal which is true w.r.t. I is true w.r.t. J, and each literal which is false w.r.t. I is false w.r.t. J as well.

3 Unfounded Sets

In this section, we extend the notion of unfounded sets, given in [Van Gelder et al., 1991] for aggregate-free programs, to the framework of LPAa,m programs. Let us denote by S1 ˙∪ ¬.S2 the set (S1 - S2) ∪ ¬.S2, where S1 and S2 are sets of standard ground literals.

De�nition 2 (Unfounded Set) A set X of ground atoms is an unfounded set for an LPAa,m program P w.r.t. I if, for each rule r ∈ P having the head atom belonging to X, at least one of the following conditions holds: 1. some antimonotone body literal of r is false w.r.t. I, and 2. some monotone body literal of r is false w.r.t. I ˙∪ ¬.X.

Example 8 Consider the following program P:

• r1 : a(1):-#count{〈1:a(1)〉, 〈2:a(2)〉, 〈3:a(3)〉}>2.
• r2 : a(2).
• r3 : a(3):-#count{〈1:a(1)〉, 〈2:a(2)〉, 〈3:a(3)〉}>2.

and I = {a(1), a(2), a(3)}. Then X = {a(1)} is an unfounded set w.r.t. I,P, since condition 2 holds for r1. Also {a(3)}, and {a(1), a(3)} are unfounded.

We can show that De�nition 2 generalizes the one given in [Van Gelder et al., 1991] for aggregate-free programs.

Theorem 9 For an aggregate-free LPAa,m program P, De�- nition 2 is equivalent to the one of [Van Gelder et al., 1991].

Thus, De�nition 2 is an alternative characterization of unfounded sets for standards literals. In fact, while condition 1 of De�nition 2 does not exactly cover the �rst one in [Van Gelder et al., 1991], condition 2 catches all cases of the second in [Van Gelder et al., 1991] and those �lost� by condition 1. This separates positive and negative literals, allowing to distinguish between the behavior of monotone and antimonotone literals.

Theorem 10 If X1 and X2 are unfounded sets w.r.t. an interpretation I for a LPAa,m program P, then also X1 ∪X2 is an unfounded set w.r.t. I for P.

Proof sketch. For Condition 2 of Def. 2, observe that I ˙∪ ¬.(X1 ∪ X2) ≤ I ˙∪ ¬.X1. Therefore, if a monotone literal ℓ is false w.r.t. I ˙∪ ¬.X1, then it is false w.r.t. I ˙∪ ¬.(X1 ∪ X2). Symmetrically for X2. ✷

By virtue of Theorem 10, the union of all unfounded sets for P w.r.t. I is an unfounded set. We call it the Greatest Unfounded Set of P w.r.t. I, and denote it by GUSP(I).

Proposition 1 Let I and J be interpretations for an LPAa,m programP. If I ⊆ J, then GUSP(I) ⊆ GUSP(J).

Proof sketch. Follows from Remark 1, since I ˙∪ ¬.X ⊆ J ˙∪ ¬.X. ✷

4 Answer Sets and Unfounded Sets

In this section, we provide a couple of characterizations of answer sets in terms of unfounded sets.

De�nition 3 (Unfounded-free Interpretation) Let I be an interpretation for a programP. I is unfounded-free if I∩X = ∅ for each unfounded set X for P w.r.t. I.

The next lemma gives an equivalent characterization of the unfounded-free property for total interpretations.

Lemma 11 Let I be a total interpretation for a programP. I is unfounded-free iff no nonempty set of atoms contained in I is an unfounded set for P w.r.t.I.

Proof sketch. If I is not unfounded-free, an unfounded set X for P w.r.t. I s.t. X ∩ I ̸= ∅ exists. Then, X ∩ I is also an unfounded set. ✷

Theorem 12 A model M is an answer set of an LPAa,m program P if and only if M is unfounded-free.

Proof sketch. If M is a model and X ⊆ M is a non-empty unfounded set w.r.t. M, then it can be shown that M ˙∪ ¬.X is a model of P M , hence M is no answer set. On the other hand, if M is an unfounded-free model but not an answer set, a model N of P M s.t. N + ⊂ M + must exist. We can show that M + - N + is an unfounded set. ✷

Now we give another interesting characterization of answer sets. A total interpretation is an answer set if and only if its false literals are unfounded.

Lemma 13 A total interpretation M is a model for P iff ¬.M - is an unfounded set for P w.r.t. M.

Proof sketch. The result follows from the fact that M = M ˙∪ ¬.(¬.M -). ✷

Theorem 14 Let M be a total interpretation for a program P. M is an answer set iff ¬.M - = GUSP(M).

Proof sketch. Can be shown using Lemmata 13 and 11 and Theorem 12. ✷

5 Well-Founded Semantics

In this section we extend the WP de�ned in [Van Gelder et al., 1991] for aggregate-free programs to LPAa,m programs. Then, we show that the answer sets of an LPAa,m program P coincide exactly with the total �xpoints of WP.

We start by providing an extension to LPAa,m programs of the immediate consequence operator TP de�ned in [Van Gelder et al., 1991] for three-valued interpretations of standard logic programs.

De�nition 4 Let P be a LPAa,m program. De�ne the operators TP and WP from 2BP∪¬.BP to 2BP and 2BP∪¬.BP , respectively, as follows.

Theorem 15 Let M be a total interpretation for a program P. M is an answer set for P iff M is a �xpoint of WP.

Proof sketch. M - = ¬.GUSP(M) holds by virtue of Theorem 14, M + = TP(M) can be shown using Lemma 11 and De�nition 2. ✷

The WP operator is clearly monotone on a meet semilattice, and it therefore admits a least �xpoint [Tarski, 1955]. This �xpoint can be computed iteratively starting from the empty set, and approximates the intersection of all answer sets (if any).

Theorem 16 Given an LPAm,a program P, let {Wn}n∈N be the sequence whose n-th term is the n-fold application of the WP operator on the empty set (i.e., W0 = ∅, Wn = WP(Wn-1)). Then (a) {Wn}n∈N converges to a limit Wω P (∅), and (b) for each answer set M for P, M ⊇ Wω P (∅).

Proof sketch. (a) follows from the monotonicity of WP and the �niteness of BP. (b) holds since all atoms computed by TP belong to any answer set and because of Theorem 14. ✷ From Theorem 15 and 16, the following easily follows.

Corollary 17 IfWω P (∅) is a total interpretation, then it is the unique answer set of P.

The following proposition con�rms the intuition that Definition 4 extends the WP operator, as de�ned in [Van Gelder et al., 1991] for standard programs , to LPAm,a programs.

Proposition 2 Let P be an aggregate-free program. Then the WP operator of De�nition 4 exactly coincides with WP operator de�ned in [Van Gelder et al., 1991].

Corollary 18 On aggregate-free programs, W ω P (∅) coincides with the well-founded model of [Van Gelder et al., 1991].

Moreover, there are simple cases where W ω P (∅) captures the intended meaning of the program.

Example 19 Consider the following programP:

a(1) :-#sum{〈1 : a(1)〉, 〈2 : a(2)〉} > 1. b :- not a(1). a(2) :- b. b :- not c.

We have WP(∅) = {not c}, then WP({not c}) = {b, not c, not a(1)}, thenWP({b, not c, not a(1)}) = {b, not c, not a(1), a(2)} =Wω P (∅).

It is easy to verify that Wω P (∅) (which here is total) is an answer set for P.

6 Computational Complexity

We �rst show the tractability of the well-founded semantics for LPAm,a , and we then analyze the complexity of answer set semantics for general LPA programs. We consider the propositional case, hence, throughout this section we assume that programs are ground.

Theorem 20 Given a ground LPAm,a program P: 1. The greatest unfounded set GUSP(I) of P w.r.t. a given interpretation I is polynomial-time computable; 2. W ω P (∅) is polynomial-time computable.

Proof sketch. We de�ne an operator ΦI from BP to BP as follows: ΦI(Y ) = {a | ∃ r ∈ P with a = H(r) s.t. no antimonotone body literal of r false w.r.t. I ∧ all monotone body literals of r are true w.r.t. Y - ¬.I -}. The sequence φ0 = ∅, φk = ΦI(φk-1) is monotonically increasing and converges �nitely to a limit φλ, for which φλ = BP - GUSP(I) can be shown. Furthermore, each application of ΦI is polynomial in our setting 5 , and also λ is polynomial in |BP|. From this, the result follows. ✷

This result has a positive impact also for the computation of the answer set semantics of logic programs with aggregates. Indeed, as stated in Theorem 16, Wω P (∅) approximates the intersection of all answer sets from the bottom, and can be therefore used to ef�ciently prune the search space.

We next analyze the complexity of the answer set semantics of general LP A programs. In [Faber et al., 2004], the authors have shown that arbitrary (including nonmonotone) aggregates do not increase the complexity of disjunctive programs. However, nonmonotone aggregates do increase the complexity of reasoning on Or-free programs. 6

Theorem 21 Cautious reasoning over LPAm,a,n is ΠP2 - complete.

Proof. Membership follows directly from the results in [Faber et al., 2004]. Concerning hardness, we provide a reduction from 2QBF. Let Ψ = ∀x1, . . . , xm∃y1, . . . , yn : Φ, where w.l.o.g. Φ is a propositional formula in 3CNF format, over precisely the variables x1, . . . , xm, y1, . . . , yn. Observe that Ψ is equivalent to ¬∃x1, . . . , xm∀y1, . . . , yn : ¬Φ, and that ¬Φ is equivalent to a 3DNF where every literal has reversed polarity w.r.t. Φ. Let the LPAm,a,n program ΠΨ be:

5 Recall that we are dealing only with aggregates whose function is computable in polynomial time.

6 In [Ferraris, 2004] it was independently shown that deciding answer set existence for a program with weight constraints (possibly containing negative weights) is ΣP2 -complete.

t(xi, 1) : -#sum{V : t(xi, V )} >= 0. t(xi,-1) : -#sum{V : t(xi, V )} <= 0. t(yi, 1) : -#sum{V : t(yi, V )} >= 0. t(yi,-1) : -#sum{V : t(yi, V )} <= 0.

t(yi, 1) : -unsat. t(yi,-1) : -unsat.

For each clause ci = li,1 ∨ li,2 ∨ li,3 of the original Φ, we add: unsat : -µ(li,1), µ(li,2), µ(li,3), where µ(l) is t(l, -1) if l is positive, and t(l, 1) otherwise.

The query not unsat? holds for ΠΨ, iff Ψ is satis�able. ✷ Monotone and antimonotone aggregates, instead, behave as in the disjunctive case, not causing any complexity gap.

Theorem 22 Cautious reasoning over LPAm,a is co-NPcomplete.

Proof. Hardness follows from the co-NP-hardness of cautious reasoning over normal (aggregate-free) logic programs [Marek and Truszczy·nski, 1991; Schlipf, 1995]. For membership, we guess a total interpretationM, and check that: (i) A ∈ M, and (ii) ¬.M - = GUSP(M) (by Theorem 14 M is then an answer set). By Theorem 20, the checks are feasible in polynomial time. ✷

7 RelatedWork

To our knowledge, the only other work in which the notion of unfounded set has been de�ned for programs with aggregates is [Kemp and Stuckey, 1991]. However, their definition ignores aggregates in the second condition for unfounded sets. For the program a(1):-#count{X : a(X)} > 0. the well-founded model of [Kemp and Stuckey, 1991] is ∅, leaving a(1) unde�ned. Our well-founded model is {¬a(1)}. Most of the results reported in this paper do not hold for unfounded sets as de�ned in [Kemp and Stuckey, 1991].

There have been several attempts to de�ne well-founded semantics for programs with aggregates, not relying on unfounded sets. Several early approaches which are de�ned on a limited framework are discussed in [Kemp and Stuckey, 1991]. In [Van Gelder, 1992] a semantics is de�ned by compiling aggregates to rules with standard atoms. This approach was generalized in [Osorio and Jayaraman, 1999]. In any case, this strategy works only for certain classes of programs. In [Ross and Sagiv, 1997] an operator-based de�nition is given, which also works only on a restricted set of programs. In [Pelov, 2004] a well-founded semantics has been de�ned based on an approximating operator. Since this de�nition is substantially different from the one in this paper, we leave a comparison for future work.

Other works attempted to de�ne stronger notions of wellfounded semantics (also for programs with aggregates), among them the Ultimate Well-Founded Semantics of [Denecker et al., 2001] and WFS1 and WFS2 of [Dix and Osorio, 1997]. Whether a characterization in terms of unfounded sets can exist for these semantics is not clear, and even if such generalized unfounded sets would exist, it is likely that some of the theorems in this paper will no longer hold, given that these semantics assign truth or falsity for more atoms.

In [Ferraris, 2004] it was shown that the semantics of Smodels programs with positive weight constraints is equal to answer sets as de�ned in [Faber et al., 2004] on the respective fragment. Since by Theorem 16 Wω P (∅) approximates answer sets of [Faber et al., 2004], Wω P (∅) can be used also as an approximating operator for the respective Smodels programs. Indeed, we can show that the AtMost pruning operator of Smodels [Simons et al., 2002] is a special case of the ΦI operator (de�ned in the proof sketch for Theorem 20).

8 Applications and Conclusion

The semantics of logic programs with aggregates is not straightforward, especially in presence of recursive aggregates. The declarative and �xpoint characterizations of answer sets, provided in Sections 4 and 5, allow for a better understanding of the meaning of programs with aggregates, and provide a handle on effective methods for computing answer sets for programs with (recursive) aggregates. In particular, the operator Wω P (∅) can be used �rst to compute what must be in any answer set. Later in the computation, it can be used as a pruning operator and for answer set checking (as described in [Koch et al., 2003; Pfeifer, 2004]).

Furthermore, since loop formulas encode unfounded sets [Lee, 2004], our results should be adaptable also to SATbased ASP systems, all of which rely on loop formulas.

The complexity results make a clear demarcation between aggregates from the computational viewpoint, which is very useful to pick the appropriate techniques to be employed for the computation. The well-founded semantics of LPAm,a is ef�ciently computable. Answer set semantics is in co-NP for LPAm,a , while nonmonotone aggregates bring about a complexity gap, and cannot be easily accommodated in NP systems.

A main concern for future work is therefore the exploitation of our results for the implementation of recursive aggregates in ASP systems.