Aggregate constructs are one of the major linguistic extensions to logic programming. In this paper, we focus on logic programming with monotone and antimonotone aggregate literals with the well-founded semantics defined in [1], which allows for aggregates occurring in recursive definitions. We formally show that computing this semantics is tractable and present a prototype system obtained by modifying DLV. To our knowledge, this is the only system supporting well-founded semantics for logic programs with recursive aggregates. While aggregates yield an obvious representational improvement, we also present experiments involving our prototype system and XSB, showing that aggregates are also beneficial from a computational point of view.
Logic Programming (LP) is a formalism widely used in various areas. In LP, problems are solved providing a declarative representation of the requirements to be achieved, instead of defining an ad-hoc algorithm. Several semantics for LP have been proposed, the well-founded semantics [2] is one of them, associating a three-valued model to every logic program.
Even if LP is a declarative programming language, standard LP does not allow for representing properties over sets of data in a natural way, a relevant aspect in several application domains. To overcome this lack, several syntactical extensions to LP have been proposed, the most important of which is the introduction of aggregate functions (LPA) [3, 4, 5, 6]. Among them, recursive definitions involving aggregate functions (i.e., aggregation in which aggregated data depend on the evaluation of the aggregate itself) are particularly relevant [7].
In this paper we focus on the fragment of LPA allowing for monotone and antimonotone aggregate literals (LPAm,a) [1]. LPAm,a programs have many interesting properties. Among them, we highlight similarities between monotone aggregate literals and positive standard literals, and between antimonotone aggregate literals and negative standard literals. In particular, this aspect is exploited for defining unfounded sets and well-founded semantics of LPAm,a programs. Another interesting property of LPAm,a programs is the tractability of literal evaluation w.r.t. partial interpretations.
The main contributions of the paper are as follows. • We work with unfounded sets and the well-founded operator WP for LPAm,a programs defined in [1], and formally prove that each fixpoint of WP is a (partial) model, that WP admits a least fixpoint (the well-founded model), that the well-founded model of a ground LPAm,a program is polynomialtime computable. For non-ground programs, the data-complexity remains polynomial, while the program complexity rises from P to EXPTIME as for aggregate-free programs. • We implement a prototype system supporting the well-founded semantics for LPAm,a programs. The prototype extends DLV and is the first system implementing a well-founded semantics for unrestricted LPAm,a programs. • We report on the results of the experimentation with the implemented prototype. Specifically, we define a problem having a natural representation in LPAm,a: Attacks, a variant of the classical Win-Lose problem.
The sequel of the paper is organized as follows. In Section 2 we recall the LPA language and its fragment LPAm,a, for which in Section 3 we recall the well-founded semantics and prove some of its properties, followed by a complexity analysis in Section 4. In Section 5 we discuss how some particular aggregates can be compiled away, which we used for some of the experiments reported in Section 6, in which we also overview the implemented prototype system. In Section 7, we discuss the literature, and draw our conclusions in Section 8. 2
In this section, we present the LPA language – an extension of Logic Programming (LP) by set-oriented functions (also called aggregate functions). Subsequently, we introduce the LPAm,a fragment, the language analyzed in this paper. For further background on LP, we refer to [8, 9]. 2.1
Syntax, Instantiations, Interpretations, and Models We assume sets of variables, constants, and predicates to be given. A term is either a variable or a constant. A standard atom is an expression p(t1, . . . , tn), where p is a predicate of arity n ≥ 0 and t1, . . . , tn are terms.
Aggregate Atoms. An aggregate function is of the form f (S), where f is an aggregate function symbol and S is a set term; a set term is a pair {Terms : Conj }, where Terms is a list of terms (variables or constants) and Conj is a conjunction of standard atoms. Finally, an aggregate atom is a structure of the form f (S) ≺ T , where f (S) is an aggregate function, ≺ ∈ {<, ≤, >, ≥} is a comparison operator, and T is a term (variable or constant). Literals. A literal is either (i) a standard atom, or (ii) a standard atom preceded by the negation as failure symbol not , or (iii) an aggregate atom. Two standard literals are complementary if they are of the form a and not a, for some standard atom a. For a standard literal ℓ, we denote by ¬.ℓ the complement of ℓ. Abusing of notation, if L is a set of standard literals, then ¬.L denotes the set {¬.ℓ | ℓ ∈ L}. Programs. A program is a set of rules r of the form a :− ℓ1, . . . , ℓm. , where a is a standard atom, ℓ1, . . . , ℓm are literals, and m ≥ 0. The atom a is referred to as the head of r, denoted H (r), while the conjunction ℓ1, . . . , ℓm is the body of r, denoted B(r). A structure (atom, literal, rule, or program) without variables is ground.
Safety. A local variable of a rule r is a variable appearing solely in sets terms of r; a variable of r which is not local is called global. A rule r is safe if both the following conditions hold: (i) each global variable appears in some positive standard literal of B(r); (ii) each local variable appearing in a set term {Terms : Conj } also appears in Conj . Finally, a program is safe if all its rules are safe. Instantiation. The universe of an LPA program P , denoted UP , is the set of constants appearing in P . The base of P , denoted BP , is the set of standard atoms constructible from predicates of P with constants in UP .
A substitution is a mapping from a set of variables to UP . Given a substitution σ and an LPA object obj (literal, rule, etc.), we denote by obj σ the object obtained by replacing each variable X in obj by σ(X ). A ground instance of a rule r is obtained in two steps: First, a substitution σ for the global variables of r is applied, and then every set term S in rσ is replaced by its instantiation inst(S) = {hTerms σ : Conj σi | σ is a local substitution for S}. The set of all instances of rules in a program P is denoted Ground(P ).
q(
Given an interpretation I , a standard literal ℓ is either (i) true if ℓ ∈ I , or (ii) false if ¬.ℓ ∈ I , or (iii) undefined otherwise. We denote by I + and I − the set of standard positive and negative literals occurring in I , respectively. An interpretation I is total if there are no undefined literals w.r.t. I , otherwise I is partial.
An interpretation also provides a meaning to set terms, aggregate functions and aggregate literals, namely a multiset, a value, and a truth value, respectively. We first consider a total interpretation I . The evaluation I (S) of a set term S w.r.t. I is the multiset I (S) defined as follows: Let SI = {ht1, ..., tni | ht1, ..., tn : Conj i ∈ S and all the atoms in Conj are true w.r.t. I}, then I(S) is the multiset obtained as the projection of the tuples of SI on their first constant, that is, I(S) = [t1 | ht1, ..., tni ∈ SI ]. The evaluation 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 fixed symbol not occurring in P). A ground aggregate atom f (S) ≺ k is true w.r.t. I if both (i) I(f (S)) 6= ⊥, and (ii) I(f (S)) ≺ k holds; otherwise, f (S) ≺ k is false.
We now consider a partial interpretation I and define extension of I an interpretation J such that I ⊆ J . If a ground aggregate literal ℓ is true (resp. false) w.r.t. each total interpretation J extending I, then ℓ is true (resp. false) w.r.t. I; otherwise ℓ is undefined.
Example 2. Let S1 be the set term in the literal ℓ1 = #sum{h1 : p(
Remark 1. Observe that our definitions 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.
Model. Given an interpretation I, a rule r is satisfied w.r.t. I if either (i) the head atom is true w.r.t. I, or (ii) some body literal is false w.r.t. I, or (iii) both the head atom and some body literal are undefined w.r.t. I. An interpretation M is a model of an LPA program P if all the rules in Ground(P) are satisfied w.r.t. M . 2.2
In this section, we present the LPAm,a fragment of LPA.
Monotonicity. Given two interpretations I and J , we say that I ≤ J if I+ ⊆ J + and I− ⊇ J −. 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 ℓ is neither monotone nor antimonotone.
Positive standard literals are monotone, while negative standard literals are antimonotone. Aggregate literals may be monotone, antimonotone or nonmonotone.
We denote by LPAm,a the fragment allowing only monotone and antimonotone aggregates. For an LPAm,a rule r, the set of its monotone and antimonotone body literals are denoted by Bm(r) and Ba(r), respectively.
Unfounded Sets and Well-Founded Semantics In this section, we recall the notion of unfounded set for LPAm,a programs defined in [1]. We then exploit unfounded sets for extending the well-founded semantics defined in [2] for aggregate-free programs to the LPAm,a framework. A complexity analysis of the well-founded semantics herein defined will be presented in Section 4.
In the following we deal with ground programs, so we will usually denote
by P a ground program. We will also exploit the notation L ∪˙ ¬.L′ for the set
(L \ L′) ∪ ¬.L′, where L and L′ are sets of standard ground literals.
Definition 1 (Unfounded Set [1]). A set X ⊆ BP of ground atoms is an unfounded
set for an LPAm,a program P w.r.t. a (partial) interpretation I if and only if, for each
rule r ∈ P having H(r) ∈ X, either (
Intuitively, each rule having the head atom belonging to some unfounded set is
either already satisfied w.r.t. I (in case condition (
r2 :
a(
r3 :
a(
The union of all the unfounded sets for a program P w.r.t. an interpretation I is an unfounded set as well; it is called the greatest unfounded set for P w.r.t. I and denoted GU SP (I), cf. [1].
Definition 2 ([1]). Let P be an LPAm,a program. The immediate logical consequence operator TP : IP → 2BP and the well-founded operator WP : IP → 2BP ∪¬.BP are defined as follows:
TP (I) = {ℓ ∈ BP | ∃r ∈ P such that H(r) = ℓ
and all the literals in B(r) are true w.r.t. I}
WP (I) = TP (I) ∪ ¬.GU SP (I).
Both TP and GU SP are monotone operators, and so WP is monotone as well. Moreover, on aggregate-free programs, the well-founded operator of Definition 2 exactly coincides with the well-founded operator defined in [2].
We next show that a fixpoint of WP is a (partial) model. Theorem 1. Let P be an LPAm,a program and M a (partial) interpretation. If M is a fixpoint of WP , then M is a (partial) model of P.
Proof. Let assume WP (M ) = M and consider a rule r ∈ P. If all the literals in B(r) are true w.r.t. M , then H(r) ∈ TP (M ) ⊆ M . If H(r) is false w.r.t. M , then H(r) ∈ GU SP (M ). Since GU SP (M ) is an unfounded set for P w.r.t. M , either some literal in Ba(r) is false w.r.t. M , or some literal in Bm(r) is false w.r.t. M ∪˙ ¬.GU SP (M ) = M . We can then conclude that r is satisfied by M .
We can then prove that the sequence W0 = ∅, Wn+1 = WP (Wn) is welldefined, that is, each element of the sequence is an interpretation.
Theorem 2. Let P be an LPAm,a program. The sequence W0 = ∅, Wn+1 = WP (Wn) is well-defined.
Proof. We use strong induction. The base case is trivial, since W0 = ∅. In order to
prove the consistency of Wn+1, we assume the consistency of every Wm such that
m ≤ n. We have to show that GU SP (Wn) ∩ Wn+1 = ∅. To this end, we show that
if a set X of atoms is such that X ∩Wn+1 6= ∅, then X is not an unfounded set for P
w.r.t. Wn. Let Wm+1 be the first element of the sequence such that X ∩ Wm+1 6= ∅
(note that m ≤ n). Consider any atom ℓ ∈ X ∩ Wm+1. By definition of TP , there
is a rule r ∈ P having H(r) = ℓ and such that all the literals in B(r) are true
w.r.t. Wm. Note that no atom in Wm can belong to X (for the way Wm+1 has been
chosen). Thus, by Remark 1, all the literals in B(r) are true w.r.t. both Wn and
Wn ∪˙ ¬.X (we recall that Wn ⊇ Wm because WP is monotone). This ends the
proof, as neither condition (
The theorem above and the monotonicity of WP imply that WP admits a least fixpoint WPω(∅) (as a consequence of Tarski’s fixed point theorem [10]). The wellfounded semantics of an LPAm,a program P is exactly given by the least fixpoint of WP , called the well-founded model of P. 4
The Complexity of the Well-Founded Semantics For the complexity analysis carried out in this section, we consider ground programs and polynomial-time computable aggregate functions (note that all sample aggregate functions appearing in this paper fall into this class).
We start by stating an important property of monotone and antimonotone aggregates, from which the tractability of the evaluation of LPAm,a literals w.r.t. partial interpretations immediately follows.
Lemma 3. Let I be a partial interpretation for an LPAm,a program P, A a ground aggregate literal occurring in P, Imin and Imax two total interpretations such that Imin = I ∪ ¬.(BP \ I) and Imax = I ∪ (BP \ ¬.I).
1. If A is a monotone literal, then A is true (resp. false) w.r.t. I if and only if A is true w.r.t. Imin (resp. false w.r.t. Imax).
Proof. We start by noting that Imin (resp. Imax) is a total interpretation extending I and such that all the standard atoms which are undefined w.r.t. I are false w.r.t. Imin (resp. true w.r.t. Imax). Thus, we have (∗) Imin ≤ I ≤ Imax. If A is monotone and true w.r.t. Imin (resp. false w.r.t. Imax), then A is true (resp. false) w.r.t. I because of (∗). If A is antimonotone and true w.r.t. Imax (resp. false w.r.t. Imin), then A is true (resp. false) w.r.t. I because of (∗). We end the proof by observing that if A is true (resp. false) w.r.t. I, then A is true (resp. false) w.r.t. Imin and Imax by definition.
We now define an operator which can be used for computing BP \ GU SP (I), and thus GU SP (I) itself.
Definition 3. Let I be a partial interpretation for an LPAm,a program P, and Y ⊆ BP , let φI (Y ) = {ℓ ∈ BP | ∃ r ∈ P with H(r) = ℓ such that no (antimonotone) literal in Ba(r) is false w.r.t. I, and all the (monotone) literals in Bm(r) are true w.r.t. Y \ ¬.I−} Proposition 1. For a partial interpretation I for an LPAm,a program P, the least fixpoint φIω(∅) coincides with the set BP \ GU SP (I).
We can now prove the tractability of the well-founded semantics.
Theorem 4. Given an LPAm,a program P, WPω(∅) is polynomial-time computable. Proof. Both φIω(∅) and WPω(∅) are obtainable by at most |BP | application of φ and WP , respectively.
Well-founded semantics is also hard for polynomial-time. In particular, deciding whether a (ground) atom is true w.r.t. the well-founded semantics is Pcomplete, as this task is P-hard even for aggregate-free programs [11]. 5
Compilation into Standard Logic Programming We now briefly present a strategy for representing #count, #sum and #times1 with standard constructs. The compilation is in the spirit of the one introduced for #min and #max in [12] and defines a subprogram computing the value of a (recursive) aggregate exploiting monotone/antimonotone peculiarities of the specific aggregate function. For these reasons, the compilation is referred to as monotone/antimonotone encoding (mae encoding).
1Since we are considering only monotone and antimonotone aggregate literals, the domains of #sum and #times are assumed to be N and N+, respectively.
The monotone/antimonotone encoding of an LPAm,a program P is obtained by replacing each aggregate literal A = f (S) ≺ T by a new predicate symbol f≺ whose definition is a compilation of A into standard LP. In the compilation we exploit a total order < on the elements of UP ∪ {⊥}, where ⊥ is a symbol not occurring in P and such that ⊥ < u for each u ∈ UP . We further assume the presence of a “built-in” relation < (Y , Y ′), where Y = Y1, . . . , Yn and Y ′ = Y1′, . . . , Yn′ are lists of terms, defining those pairs of tuples y, y′ such that y precedes y′ in the lexicographical order induced by <.
For simplicity, we consider an aggregate literal f ({Y : p(Y , Z)}) ≺ k having only local variables. We introduce a new predicate symbol faux of arity |Y | + 1. Intuitively, an atom faux(y, s) is intended for representing that there are at least s tuples y′ such that y does not precede y′ and p(y′, z) is true, for some tuple z. For this purpose, we first evaluate the aggregate function on the empty set, and then opportunely increase its evaluation for greater sets. For guaranteeing that each element in the set term is never taken twice, we exploit the lexicographical order induced by <. The two rules below encode this monotonically increasing evaluation: faux(⊥, α). faux(Y ′, β) :− faux(Y , S), p(Y ′, Z), <(Y , Y ′).
α = 0, β = S + 1, if f = #count where α = 0, β = S + Y1′, if f = #sum
α = 1, β = S × Y1′, if f = #times
In case ≺∈ {≥, >}, the aggregate is definitely true if some faux(y, s) with s ≺ k is true: f≥ :− faux(Y , S), S ≥ k.
f> :− faux(Y , S), S > k.
For ≺∈ {≤, <}, to conclude the truth of the aggregate we have to be sure that no faux(y, s) with s ⊀ k is true. We can model this aspect by means of the following rules: f≤ :− not f>.
f< :− not f≥.
Extending the technique to aggregate literals with global variables is quite simple: Global variables are added to the arguments of all the atoms used in the compilation, and a new predicate fgroup−by is used for collecting their possible substitutions. 6 Implementation and Experimental Results The well-founded semantics for LPAm,a programs has been implemented in the DLV [13] system. In this section, we give a very rough description of the implementation and discuss the results of our experimentation aimed at assessing the efficiency of the prototype. 6.1
System Architecture and Usage We have developed a prototype system by implementing our well-founded operator in the core of DLV. Both the intelligent grounding module and the model generator module of DLV have been modified for the implementation of the wellfounded semantics for LPAm,a programs. In particular, in the grounding module, we extended the technique for aggregate literal instantiation to correctly deal with aggregate atoms occurring recursively, while in the model generator we implemented a polynomial time algorithm for computing the least fixpoint of the operator φ introduced in Section 4.
In our prototype, the well-founded semantics is adopted when the user invokes DLV with -wf or --well-founded. If none of these two options are specified, then the stable model semantics is adopted as usual. In both cases, the system exploits the well-founded operator WP introduced in Section 3. For the stable model semantics, the well-founded model is profitably used for search space pruning after each non-deterministic choice. For the well-founded semantics, instead, the wellfounded model is yielded immediately after the least fixpoint of the well-founded operator is computed; in this case, the system outputs two sets, representing true and undefined (standard) atoms w.r.t. the well-founded model.
An executable of the DLV system supporting well-founded semantics for LPAm,a programs is available at http://www.dlvsystem.com/dlvRecAggr/. 6.2
Experimental Results To our knowledge, the implemented prototype is currently the only system supporting a well-founded semantics for logic programs with recursive aggregates. In particular, one of the major systems supporting the well-founded semantics, XSB, has some support for aggregates, but (apart from #min and #max) not when they occur in recursive definitions. Therefore, our experiments have been designed for evidencing the computational advantages of aggregate constructs w.r.t. equivalent encodings without aggregates.
The experiments have been performed on a 3GHz Intel R Xeon R processor system with 4GB RAM under the Debian 4.0 operating system with GNU/Linux 2.6.23 kernel. The tested systems have been compiled with GCC 4.4.1. For every instance, we have allowed a maximum running time of 600 seconds (10 minutes) and a maximum memory usage of 3GB.
For the benchmark, we have defined the Attacks problem, a problem similar to the classic Win-Lose problem often used as an example for the well-founded semantics of standard logic programs (see for instance [9]). In the Attacks problem, a set of p players, each one attacking n other players, and a positive integer m are given. A player wins if no more than m winners attack it.
Example 4. An instance of the Attacks problem in which p = 6, n = 2 and m = 1 could be the one represented by the following directed graph:
clude that d is a winner. Similarly for e.
Therefore, f is a loser because f is attacked by d and e, which are winners. For the other players, namely a, b and c, it is not possible to determine whether they are winners or losers.
The encodings used in our experiments are reported below, where max, player and attacks are EDB predicates representing the parameter m, the set of players and the attacks done by the players, respectively.
Aggregate-Based Encoding:
win(X) :− max(M ), player(X), #count{Y : attacks(Y, X), win(Y )} ≤ M. This encoding exploits aggregate constructs and is a natural representation of the Attacks problem.
Join-Based Encoding:
win(X) :− player(X), not lose(X).
lose(X) :− max(
attacks(Y2, X), win(Y2), Y1 < Y2.
lose(X) :− max(
lose(X) :− max(
In this encoding there is a rule for each possible value of the m parameter. However, the presence of the predicate max in the body of these rules assures that the solvers considered in our experiments automatically disregard rule instances that do not match the given max.
Mae-Based Encoding (from monotone/antimonotone encoding): win(X) :− player(X), not lose(X). lose(X) :− count(X, Y, S), max(M ), S > M. count(X, Y, 1) :− aux(X, Y ). count(X, Y ′, S + 1) :− count(X, Y, S), aux(X, Y ′), Y < Y ′.
aux(X, Y ) :− attacks(Y, X), win(Y ).
This is an encoding in the spirit of [12] substantially obtained by applying the compilation presented in Section 5 (with some minor simplifications). Intuitively, an atom count(x, y, s) stands for “there are at least s constants y′ such that y′ ≤ y and attacks(y′, x), win(y′) is true”. The definition of count exploits the natural order of integers for guaranteeing that no y′ is counted twice.
Example 5. The EDB representing the instance in Example 4 is the following:
player(a). player(d). attacks(a, b). attacks(c, a). attacks(e, c).
player(b). player(e). attacks(a, c). attacks(c, b). attacks(e, f ).
player(c). player(f ). attacks(b, a). attacks(d, b). attacks(f, d).
max(
For all the encodings, the well-founded model restricted to the win predicate is {win(d), win(e), not win(f )}. Note that win(a), win(b) and win(c) are undefined. 30 25 20 15 10 5 600 500 400 300 200 100
DLV-join
DLVA
We performed an intensive experimentation for the Attacks problem, varying the parameters p, m and n. For each combination of these parameters, we measured the average execution time of DLV and XSB on 3 randomly generated instances. The results of our experimentation are reported in figures 1–4. In the graphs, DLVA is the implemented prototype with the aggregate-based encoding, DLVjoin and DLV-mae the implemented prototype with the aggregate-free encodings, XSB-join and XSB-mae the XSB system with the aggregate-free encodings (as mentioned earlier, XSB does not support recursive aggregates). For the XSB system, we explicitly set indexes and tabled predicates for optimizing its computation.
For each graph, the number of players is fixed, while parameters m (x-axis) and n (y-axis) vary. Therefore, the size of the instances grows moving from left to right along the y-axis, while is invariant w.r.t. the x-axis. However, the number of joins required by the join-based encoding depends on the parameter m. As a matter of fact, we can observe in the graphs in figures 1–2 that the average execution time of the join-based encoding increases along both the x- and y-axis (for both DLV and XSB). Instead, for the encoding exploiting aggregates, and for the mae encoding, the average execution time depends only on instance size, as shown in the graphs in Figures 3–4.
For the join-based encoding, XSB is generally faster than DLV, but consumes much more memory. Indeed, in Figure 2, we can observe that XSB terminates its computation in a few seconds for the smaller instances, but rapidly runs out of memory on slightly larger instances. 8 7 6 5 4 3 2 1
Considering the mae-based encoding, we can observe significant performance gains for both DLV and XSB (see figures 3–4). Indeed, both systems complete their computation in the allowed time and memory on larger instances. Computational advantages of the mae-based encoding w.r.t. the join-based encoding are particularly evident for XSB, which can solve all instances of the benchmark with this encoding. However, also XSB with the mae-based encoding is outperformed by DLV with native support for aggregate constructs (see Figure 4).
In sum, the experimental results highlight that the presence of aggregate constructs can significantly speed-up the computation. Indeed, the encoding exploiting recursive aggregates outperforms the aggregate-free encodings in all the instances. 7
The definition of well-founded semantics for LPA has been a challenge of major interest in the last years. The first attempts, not relying on a notion of unfounded set, have been defined on a limited framework. Some of these are discussed in [3].
A first attempt to define a well-founded semantics for LPA without restriction has been done in [3]. Even if the semantics defined in [3] has the advantage of being based on a notion of unfounded set, it often leaves too many undefined literals.
Our work is particularly related to [14], where D˜-well-founded semantics has been defined. D˜-well-founded semantics is based on approximating operators, not on unfounded sets, and the semantics depends on the adopted approximating ag0 1 2 3 x4 5 6 7 8 9 1 2 3 4 5 6 7 8 y9 10 (i) 1600 players gregate relation; the authors discuss trivial, bound and ultimate approximating aggregate relations. Semantics relying on trivial approximating aggregates is very imprecise, but it is still suitable for the class of stratified aggregate programs. Both trivial and bound approximations have polynomial complexity, while ultimate has been proved to be intractable for nonmonotone aggregate functions [4]. For LPAm,a programs, the D˜-well-founded semantics under ultimate and bound approximations coincide with the well-founded semantics presented in this paper.
Other works attempted to define stronger notions of well-founded semantics (also for programs with aggregates), like the Ultimate Well-Founded Semantics of [5], or WFS1 and WFS2 of [6]. Whether a characterization in terms of unfounded sets exists for these semantics is an open problem.
Programs with aggregates are related to abstract constraint programs [15], for which no well-founded semantics has been defined to our knowledge. The definitions in this paper can be easily adapted to cover abstract constraints. 8
In this paper we analyzed LPAm,a programs under well-founded semantics. We showed that computing this semantics is a tractable problem. Indeed, the semantics is given by the least fixpoint of the well-founded operator WP . The fixpoint is 3.5 3 2.5 2 1.5 1 0.5 60 50 40 30 20 10 reached in a polynomial number of applications of WP (w.r.t. the size of the input program), each of them requiring polynomial time. For showing that an application of WP is polynomial-time feasible, we have proved that evaluating monotone and antimonotone aggregate literals remains polynomial-time doable also for partial interpretations, since in this case only one of the possibly exponential extensions must be checked. For a monotone aggregate literal, this extension is obtained by falsifying each undefined literal, while for an antimonotone aggregate literal, each undefined literal is taken as true in the extension.
Motivated by these positive theoretical results, we have implemented the first system supporting a well-founded semantics for unrestricted LPAm,a. Allowing for using monotone and antimonotone aggregate literals, the implemented prototype is ready for experimenting with the LPAm,a framework. The experiments conducted on the Attacks benchmark highlight the computational gains of a native implementation of aggregate constructs w.r.t. equivalent encodings in standard LP.
This research has been partly supported by Regione Calabria and EU under POR Calabria FESR 2007-2013 within the PIA project of DLVSYSTEM s.r.l., and by MIUR under the PRIN project LoDeN.