policies [Son and Lobo, 2001], wire routing problems [Erdem *et al.*, 2000] and phylogeny reconstruction problems [Erdem *et al.*, 2003].

The stable models of a logic program are found by systems called *answer set* solvers. Answer set solvers can be considered the equivalent of SAT solvers —
systems used to find the models of propositional formulas - in logic programming.

On the other hand, it is much easier to express, in logic programming, recursive definitions (such as reachability in a graph) and defaults. Several answer set solvers have been developed so far, with SMODELS1and DLV2among the most popular.

As in the case of SAT solvers, answer set solver competitions - where answer set solvers are compared to each others in terms of performance - are planned to be held regularly.3 An important construct in ASP are aggregates. Aggregates allow, for instance, to perform set operations such as counting the number of atoms in a set that are true, or summing weights the weights of the atoms that are true. We can, for instance, express that a node in a graph has exactly one color by the following cardinality constraint:
1 ≤ {c(node, color1), . . . , c(node, colorm)} ≤ 1.

As another example, a weight constraint of the form

$$3\leq\{p=1,q=2,r=3\}$$
3 ≤ {p = 1, q = 2, r = 3} (1)
intuitively says that the sum of the weights (the numbers after the "=" sign) of the atoms from the list p, q, r that are true is at least 3.

Aggregates are a hot topic in ASP not only because of their importance, but also because there is no standard understanding of the concept of an aggregate. In fact, different answer set solvers implement different definitions of aggregates: for instance, SMODELS implements cardinality and weight constraints [Niemel¨a and Simons, 2000],
while DLV implements aggregates as defined by Faber, Leone and Pfeifer (2005)
(we call them FLP-aggregates). Unfortunately, constructs that are intuitively equivalent to each other may actually lead to different stable models. In some sense, no current definition of an aggregate can be considered fully satisfactory, as each of them seems to have properties that look unintuitive. For instance, it is somehow puzzling that, as noticed in [Ferraris and Lifschitz, 2005b], weight constraints 0 ≤ {p = 2, p = −1} and 0 ≤ {p = 1}
are semantically different from each other (may lead to different stable models).

Part of this problem is probably related to the lack of mathematical tools for study-1http://www.tcs.hut.fi/Software/smodels/
2http://www.dbai.tuwien.ac.at/proj/dlv/ 3http://asparagus.cs.uni-potsdam.de/contest/