-

Evaluating Answer Set Programming with Non-Convex Recursive Aggregates

Mario Alviano

alviano@mat.unical.it 0 0 Department of Mathematics and Computer Science, University of Calabria , 87036 Rende (CS) , Italy

Aggregation functions are widely used in answer set programming (ASP) for representing and reasoning on knowledge involving sets of objects collectively. These sets may also depend recursively on the results of the aggregation functions, even if so far the support for such recursive aggregations was quite limited in ASP systems. In fact, recursion over aggregates was restricted to convex aggregates, i.e., aggregates that may have only one transition from false to true, and one from true to false, in this specific order. Recently, such a restriction has been overcome, so that the user can finally use non-convex recursive aggregates in ASP programs, either on purpose or accidentally. A preliminary evaluation of ASP programs with non-convex recursive aggregates is reported in this paper.

answer set programming aggregation functions non-convex recursive aggregates

Answer set programming (ASP) is a declarative language for knowledge representation and reasoning [ 9 ]. ASP programs are sets of disjunctive logic rules, possibly using default negation under stable model semantics [ 21, 22 ]. Several constructs were added to the original, basic language in order to ease the representation of practical knowledge. Of particular interest are aggregate functions [ 5, 14, 17, 23, 27, 32 ], which allow for expressing properties on sets of atoms declaratively. In fact, in many ASP programs functional dependencies are enforced by means of COUNT aggregates, or equivalently using SUM aggregates; for example, a rule of the following form:

⊥ ← R0(X ), SUM[1, Y : R(X , Y , Z)] ≤ 1 constrains relation R to satisfy the functional dependency X → Y , where X ∪ Y ∪ Z is the set of attributes of R, and R0 is the projection of R on X . Aggregate functions are also commonly used in ASP to constrain a nondeterministic guess. For example, in the knapsack problem the total weight of the selected items must not exceed a given limit, which can be modeled by the following rule:

⊥ ← SUM[W, O : object (O, W, C ), in (O)] ≤ limit .

Mainstream ASP solvers [ 15, 20 ] almost agree on the semantics of aggregates [ 14, 17 ], here referred to as F-stable model semantics, even if several valid alternatives were also considered in the literature [ 23, 30, 31, 33 ]. It is interesting to observe that F-stable model semantics was proposed more than a decade ago, providing a reasonable semantics for aggregates also in the recursive case. Indeed, it is based on an extension of the original program reduct, and on a minimality check of the stable model candidate resembling the disjunctive case. Despite this, for many years the implementation of Fstable model semantics was incomplete, and recursion over aggregates was restricted to convex aggregates [ 28 ], the largest class of aggregates for which the common reasoning tasks still belong to the first level of the polynomial hierarchy in the normal case [ 3 ]. In fact, convex aggregates may have only one transition from false to true, and one from true to false, in this specific order, a property that guarantees tractability of model checking in the normal case.

However, non-convex aggregations may arise in several contexts while modeling complex knowledge [ 1, 11, 13 ], and there are also minimalistic examples that are easily encoded in ASP using recursive non-convex aggregates, while alternative encodings not using aggregates are not so obvious. One of such examples is provided by the Σ2P complete problem called Generalized Subset Sum [ 6 ]. In this problem, two vectors u and v of integers as well as an integer b are given, and the task is to decide whether the formula ∃x∀y(ux + vy 6= b) is true, where x and y are vectors of binary variables of the same length as u and v, respectively. For example, for u = [ 1, 2 ], v = [ 2, 3 ], and b = 5, the task is to decide whether the following formula is true: ∃x1x2∀y1y2(1 · x1 + 2 · x2 + 2 · y1 + 3 · y2 6= 5). Any natural encoding of such an instance would include an aggregate of the form SUM[1 : x1, 2 : x2, 2 : y1, 3 : y2] 6= 5. Luckily, a complete implementation of F-stable model semantics for common aggregation functions has been achieved this year by means of a translation combining disjunction and saturation in order to eliminate non-convexity from aggregates [ 4 ].

The aim of this paper is to evaluate a few problems that can be encoded in ASP using recursive non-convex aggregates. The tested programs are processed by the rewritings presented in [ 4 ], which are implemented in a prototype system written in Python that uses GRINGO and CLASP. In a nutshell, aggregates are represented by specific standard atoms, so that the grounding phase can be delegated to GRINGO [ 19 ], and the numeric output of GRINGO is then processed to properly encode aggregates for the subsequent stable model search performed by CLASP [ 20 ]. The focus of the paper is on programs using SUM aggregates, even if the tested system also supports several other common aggregation functions such as COUNT, AVG, MIN, MAX, EVEN, and ODD. 2

Background

Let V be a set of propositional atoms including ⊥. A propositional literal is an atom possibly preceded by one or more occurrences of the negation as failure symbol ∼. An aggregate literal, or simply aggregate, is of the following form:

SUM[w1 : l1, . . . , wn : ln] b (1) where n ≥ 0, b, w1, . . . , wn are integers, l1, . . . , ln are propositional literals, and ∈ {<, ≤, ≥, >, =, 6=}. (Note that [w1 : l1, . . . , wn : ln] is a multiset.) A literal is either a propositional literal, or an aggregate. A rule r is of the following form: p1 ∨ · · · ∨ pm ← l1 ∧ · · · ∧ ln (2) where m ≥ 1, n ≥ 0, p1, . . . , pm are propositional atoms, and l1, . . . , ln are literals. The set {p1, . . . , pm} \ {⊥} is referred to as head, denoted by H(r), and the set {l1, . . . , ln} is called body, denoted by B(r). A program Π is a finite set of rules. The set of propositional atoms (different from ⊥) occurring in a program Π is denoted by At (Π), and the set of aggregates occurring in Π is denoted by Ag (Π). y2 ← unequal ⊥ ← ∼unequal Example 1. Consider the following program Π1: x1 ← ∼∼x1 x2 ← ∼∼x2 y1 ← unequal unequal ← SUM[1 : x1, 2 : x2, 2 : y1, 3 : y2] 6= 5 As will be clarified after defining the notion of a stable model,Π1 encodes the instance of Generalized Subset Sum introduced in Section 1.

I |= B(r); – for a program Π, I |= Π if I |= r for all r ∈ Π.

For any expression π, if I |= π, we say that I is a model of π, I satisfies π, or π is true in I. In the following, > will be a shorthand for ∼⊥, i.e., > is a literal true in all interpretations.

The reduct of a program Π with respect to an interpretation I is obtained by removing rules with false bodies and by fixing the interpretation of all negative literals. More formally, the following function F (I, ·) is inductively defined: – for p ∈ V, F (I, p) := p; – F (I, ∼l) := > if I 6|= l, and F (I, ∼l) := ⊥ otherwise; – F (I, SUM[w1 : l1, . . . , wn : ln] b) := SUM[w1 : F (I, l1), . . . , wn : F (I, ln)] b; – for a rule r of the form (2), F (I, r) := p1 ∨ · · · ∨ pm ← F (I, l1) ∧ · · · ∧ F (I, ln); – for a program Π, F (I, Π) := {F (I, r) | r ∈ Π, I |= B(r)}.

Program F (I, Π) is the reduct of Π with respect to I. An interpretation I is a stable model of a program Π if I |= Π and there is no J ⊂ I such that J |= F (I, Π). Let SM (Π) denote the set of stable models of Π.

Example 2. Continuing with Example 1, the models of Π1, restricted to the atoms in At (Π1), are X, X ∪ {x1}, X ∪ {x2}, and X ∪ {x1, x2}, where X = {unequal , y1, y2}. Of these, only X ∪ {x1} is a stable model. Indeed, the reduct F (X ∪ {x1}, Π1) is x1 ← > y1 ← unequal y2 ← unequal unequal ← SUM[1 : x1, 2 : x2, 2 : y1, 3 : y2] 6= 5 and no strict subset of X ∪ {x1} is a model of the above program. On the other hand, the reduct F (X ∪ {x2}, Π1) is x2 ← > y1 ← unequal y2 ← unequal unequal ← SUM[1 : x1, 2 : x2, 2 : y1, 3 : y2] 6= 5 and {x2, y2} is a model of the above program. Similarly, it can be checked that X and X ∪ {x1, x2} are not stable models of Π1.

An aggregate A is convex (in program reducts) if J |= F (I, A) and L |= F (I, A) implies K |= F (I, A), for all J ⊆ K ⊆ L ⊆ I ⊆ V. If A is convex then I |= A and J |= F (I, A) implies K |= F (I, A), for all J ⊆ K ⊆ I. Note that aggregate SUM[1 : x1, 2 : x2, 2 : y1, 3 : y2] 6= 5 from Example 1 is non-convex. 3

Non-Convex Aggregates Elimination

ASP solvers can only process sums of the form (1) in which all numbers are nonnegative integers, and the comparison operator is ≥. This is due to the numeric format encoding the propositional program produced by the grounder. However, thanks to the rewritings proposed by [ 4 ], all sums can be rewritten in the form accepted by current ASP solvers. Following [ 4 ], strong equivalences can be used to restrict sums in the input program to only two forms, which are essentially (1) with ∈ {≥, 6=}. These first rewritings are given by means of strong equivalences [ 16, 25, 34 ]. Definition 1. Let π := l1 ∧ · · · ∧ ln be a conjunction of literals, for some n ≥ 1. A pair (J, I) of interpretations such that J ⊆ I is an SE-model of π if I |= π and J |= F (I, l1) ∧ · · · ∧ F (I, ln). Two conjunctions π, π0 are strongly equivalent, denoted by π ≡SE π0, if they have the same SE-models.

Strong equivalence means that replacing π by π0 preserves the stable models of any logic program.

Proposition 1 (Lifschitz et al. 2001; Turner 2003; Ferraris 2005). Let π, π0 be two conjunctions of literals such that π ≡SE π0. Let Π be a program, and Π0 be the program obtained from Π by replacing any occurrence of π by π0. It holds that Π ≡V Π0.

The following strong equivalences can be proven by showing equivalence with respect to models, and by noting that ∼ is neither introduced nor eliminated: (E1) SUM[w1 : l1, . . . , wn : ln] > b ≡SE SUM[w1 : l1, . . . , wn : ln] ≥ b + 1; (E2) SUM[w1 : l1, . . . , wn : ln] ≤ b ≡SE SUM[−w1 : l1, . . . , −wn : ln] ≥ −b; (E3) SUM[w1 : l1, . . . , wn : ln] < b ≡SE SUM[w1 : l1, . . . , wn : ln] ≤ b − 1; (E4) SUM[w1 : l1, . . . , wn : ln] = b ≡SE SUM[w1 : l1, . . . , wn : ln] ≤ b ∧

SUM[w1 : l1, . . . , wn : ln] ≥ b.

For example, (E1) and (E3) are easy to obtain because b is integer by assumption. Similarly, (E4) is immediate by the semantics introduced in Section 2. For (E2), instead, the following equivalences can be observed: (i) I |= SUM[w1 : l1, . . . , wn : ln] ≤ b; (ii) Pi∈[1..n], I|=li wi ≤ b; (iii) Pi∈[1..n], I|=li −wi ≥ −b; (iv) I |= SUM[−w1 : l1, . . . , −wn : ln] ≥ −b; where (iii) above is obtained by multiplying both sides of the inequality (ii) by −1, and the equivalence of (i) and (ii), and of (iii) and (iv), is immediate by the semantics of sums. It is important to observe that the application of (E1)–(E4), from the last to the first, to a programΠ gives an equivalent program pre(Π) whose aggregates are sums with comparison operators ≥ and 6=.

Theorem 1. Let Π be a program. It holds that Π ≡V pre(Π).

After this preprocessing, the structure of the input program is further simplified by eliminating non-convex aggregates. To ease the presentation, and without loss of generality, hereinafter aggregates are assumed to be of the following form: SUM[ − w1 : p1, . . . , −wj : pj , − wj+1 : ∼lj+1, . . . , −wk : ∼lk, wk+1 : pk+1, . . . , wm : pm, wm+1 : ∼lm+1, . . . , wn : ∼ln] b (3) (4) (5) (6) (7) where n ≥ m ≥ k ≥ j ≥ 0, w1, . . . , wn are positive integers, each pi is a propositional atom, each li is a propositional literal, ∈ {≥, 6=}, and b is an integer. Intuitively, aggregated elements of (3) are partitioned in four sets, namely positive literals with negative weights, negative literals with negative weights, positive literals with positive weights, and negative literals with positive weights.

Let Π be a program whose aggregates are of the form (3). Program rew (Π) is obtained from Π by replacing each occurrence of an aggregate of the form (3) by a fresh, hidden propositional atom aux [ 10, 24 ]. Moreover, if is ≥, then the following rule is added: aux ← SUM[w1 : p1F , . . . , wj : pjF , wj+1 : ∼∼lj+1, . . . , wk : ∼∼lk, wk+1 : pk+1, . . . , wm : pm, wm+1 : ∼lm+1, . . . , wn : ∼ln] ≥ b + w1 + · · · + wk where each piF is a fresh, hidden atom associated with the falsity of pi, for all i ∈ [1..j], and the following rules are also added to rew (Π): piF ← ∼pi piF ← aux pi ∨ piF ← ∼∼aux

Similarly, if

is 6=, then the following rules are added to rew (Π): aux ← SUM[w1 : p1, . . . , wj : pj , wj+1 : ∼∼lj+1, . . . , wk : ∼∼lk, wm+1 : ∼lm+1, . . . , wn : ∼ln] ≥ b + 1 + w1 + · · · + wk wj+1 : ∼lj+1, . . . , wk : ∼lk, wk+1 : pkF+1, . . . , wm : pFm, wm+1 : ∼∼lm+1, . . . , wn : ∼∼ln] ≥ −b + 1 + wk+1 + · · · + wn together with rules (5)–(7) for each new piF . Intuitively, any atom of the form piF introduced by the rewriting must be true whenever pi is false, but also when aux is true, so to implement what is usually referred to as saturation in the literature. Rules (5) and (6) encode such an intuition. Moreover, rule (7) guarantees that at least one between pi and piF belongs to any model of reducts obtained from interpretations containing aux . It is interesting to observe that when aux belongs to I the satisfaction of the associated aggregate can be tested according to all subsets of I in the reduct F (Π, I).

The intuition behind (4) is that an interpretation I satisfies an aggregate of the form (3) such that is ≥ if and only if the following inequality is satisfied: j k X −wi · I(pi) + X −wi · I(∼li) + m

X wi · I(pi) + i=1 i=j+1 i=k+1 n

X i=m+1 wi · I(∼li) ≥ b (10) where I(l) = 1 if I |= l, and I(l) = 0 otherwise, for all literals l. Moreover, inequality (10) is satisfied if and only if the following inequality is satisfied:

j X −wi · I(pi) + i=1 k X −wi · I(∼li) + m X wi · I(pi) + i=k+1 i=j+1

n + X i=m+1 wi · I(∼li) + w1 + · · · + wk ≥ b + k X wi i=1 and by distributivity (11) is equivalent to the following inequality:

j X wi · (1 − I(pi)) + i=1 k X wi · (1 − I(∼li)) + i=j+1 m + X wi · I(pi) + i=k+1 n

X i=m+1 wi · I(∼li) ≥ b + k X wi. i=1 Note that 1−I(l) = I(∼l) for all literals l, and piF is associated with the falsity of pi, for all i ∈ [1..j]. It is important to observe that negation was not used for positive literals (8) (9) (11) (12) in order to avoid oversimplifications in program reducts. Indeed, as already explained, for all i ∈ [1..j], atom piF will be derived true whenever pi is false, but also when the aggregate is true.

The intuition behind (8)–(9) is similar. Essentially, an aggregate SUM(S) 6= b of the form (3) is true if and only if either SUM(S) ≥ b + 1 or SUM(S) ≤ b − 1 is true, and (E2) is applied to the second aggregate in order to use the previously explained rewriting. Let rew ∗ denote the composition rew ◦ pre.

Example 3. Consider again program Π1 from Example 1. Its rewriting rew ∗(Π1) is as follows:

x1 ← ∼∼x1 unequal ← aux xF

1 ← ∼x1 xF

2 ← ∼x2 yF 1 ← ∼y1 yF 2 ← ∼y2 x2 ← ∼∼x2 y1 ← unequal y2 ← unequal ⊥ ← ∼unequal aux ← SUM[1 : x1F ; 2 : x2F ; 2 : y1F ; 3 : y2F ] ≥ 4 aux ← SUM[1 : x1; 2 : x2; 2 : y1; 3 : y2] ≥ 6 x1F ← aux x1 ∨ x1F ← ∼∼aux x2F ← aux x2 ∨ x2F ← ∼∼aux y1F ← aux y1 ∨ y1F ← ∼∼aux y2F ← aux y2 ∨ y2F ← ∼∼aux The only stable model of rew ∗(Π1) is {x1, unequal , y1, y2, aux , x1F , x2F , y1F , y2F }.

Correctness of the rewriting can be established by slightly adapting the proof by [ 4 ]. Theorem 2 (Correctness). Let Π be a program. It holds that Π ≡At(Π) rew ∗(Π).

4 Implementation

The rewritings introduced in Section 3 have been implemented in a prototype system written in Python and available at the following URL: http://alviano.net/ software/f-stable-models/. The prototype accepts an input language whose syntax is almost conformant to ASP Core 2.0 [ 2 ]. It is a first-order language, meaning that propositional atoms are replaced by first-order atoms made of a predicate and a list or terms, where each term is an object constant, an object variable, or a composed term obtained by combining a function symbol with other terms. As usual in ASP, all variables are universally quantified, so that the propositional semantics given in Section 2 can be used after a grounding phase that replaces variables by constants in all possible ways.

The only exception to the ASP Core 2.0 format is that sums have to be encoded using the standard predicates f sum and f set . Moreover, only positive literals can occur in aggregation sets. In more detail, a sum of the form SUM[w1 : p1, . . . , wn : pn] b, where n ≥ 0, b, w1, . . . , wn are integers, p1, . . . , pn are (first-order) atoms, and ∈ {<, ≤, ≥, >, =, 6=} is encoded by the following first-order atom:

f sum(id , μ( ), b) where μ( ) equals "<", "<=", ">=", ">", "=", or "!=", and id is an identified for the aggregation set, encoded by the following rules: f set (id , w1, p1) ← p1

f set (id , wn, pn) ← pn · · · where a body pi (i ∈ [1..n]) can be omitted if pi has no variables. (It is also possible to extend a body of the above rules in order to further constrain the aggregation set; for example, arithmetic expressions can be used to restrict the selection of atoms in the aggregation sets.) Example 4. Program Π1 from Example 1 is encoded as follows: x1 : − not not x1. x2 : − not not x2. y1 : − unequal. y2 : − unequal. : − not unequal.

unequal : − f sum(uneq, "!=", 5). f set(uneq, 1, x1). f set(uneq, 2, x2). f set(uneq, 2, y1).

f set(uneq, 3, y2). where not encodes the negation as failure symbol ∼, and rules with empty head are integrity constraints, i.e., rules whose head is equivalent to ⊥.

Alternatively, instances of Generalized Subset Sum can be specified by means of facts involving predicates exists, all , and bound . For example, the instance above is encoded by the following facts: exists(x1, 1). exists(x2, 2).

all(y1, 2). all(y2, 3).

bound(5).

A program encoding the Generalized Subset Sum problem for instances encoded by these predicates is the following: true(X, C) : − exists(X, C), not not true(X, C). true(X, C) : − all(X, C), unequal. : − not unequal. unequal : − f sum(uneq, "!=", B), bound(B).

f set(uneq, C, true(X, C)) : − true(X, C). where X , C , and B are object variables.

Given a program encoded as described above, the prototype obtains its propositional version by means of the grounder GRINGO. During the grounding phase, instances of predicate f sum are considered external, i.e., they are assigned the truth value undefined in order to prevent their elimination. These instances and those of predicate f set are identified and mapped in data structures of the prototype, so to have an internal representation of all sums occurring in the propositional program. The rewritings presented in Section 3 are then applied to these sums in order to eliminate any non-convexity. The new sums, and any additional rule introduced by the rewriting process, are added to the propositional program. Finally, the propositional program is printed to the standard output using the numeric format of GRINGO, so that CLASP can be used for computing its F-stable models, which eventually coincide with the F-stable models of the original program because additional atoms are hidden. 5

Experiment

The implemented rewritings were tested on a few domains that can be encoded using recursive sums. One of them is the Generalized Subset Sum problem presented in the introduction, which is of particular relevance in this experiment because its natural encoding in ASP requires a recursive non-convex sum. In fact, an ASP encoding for this problem that does not rely on recursive sums is not available, and therefore in this case the performance of the prototype was compared with an SMT encoding fed into Z3. The other two problems considered in this experiment are k-CliqueColoring and 2-QBF, Σ2p-complete problems whose natural encodings in ASP do not rely on recursive sums. In these two cases, an alternative encoding using recursive sums can be obtained, even if usually paying an overhead on the running time. The aim of the experiment for these two problems is to evaluate such an overhead. All tested instances are available at the following URL: http://archives.alviano.net/ publications/2015/RCRA2015-experiment.zip.

The experiment was run on an Intel Xeon CPU 2.4 GHz with 16 GB of RAM. CPU and memory usage were limited to 900 seconds and 15 GB, respectively. GRINGO, CLASP, and Z3 were tested with their default settings. Their performances were measured by PYRUNLIM (http://alviano.net/software/pyrunlim/). The results are reported in Table 1, where each row reports the number of instances and, for each tested ASP encoding, the number of solved instances, the average execution time and the average memory consumption. Data for Z3 are not reported in the table because it was run only on Generalized Subset Sum, discussed below.

Generalized Subset Sum [ 6 ]. Two vectors u and v of integers as well as an integer b are given, and the task is to decide whether the formula ∃x∀y(ux+vy 6= b) is true, where x and y are vectors of binary variables of the same length as u and v, respectively. For an instance such that u = u1, . . . , um (m ≥ 1) and v = v1, . . . , vn (n ≥ 1) the following ASP encoding was tested (actually, its non-propositional version): xi ← ∼∼xi ∀i ∈ [1..m] yi ← unequal ∀i ∈ [1..n] ⊥ ← ∼unequal unequal ← SUM[u1 : x1, . . . , um : xm, v1 : y1, . . . , vn : yn] 6= b

As for Z3, the following SMT encoding was tested: ∀y1 · · · ∀yn( ite(x1, u1, 0) + · · · + ite(xm, um, 0) +

ite(y1, v1, 0) + · · · + ite(yn, vn, 0) 6= b) where x1, . . . , xm and y1, . . . , yn are Boolean constants and variables, respectively, and ite(φ, t1, t2) is an if-then-else expression, i.e., its interpretation is t1 if φ is true, and t2 otherwise. As reported in the table, the ASP encoding leads to an excellent performance in many cases, with 38 solved instances and an average execution time of around 1.1 seconds. The performance achieved within the SMT encoding is instead less attractive, with only 14 solved instances and an average execution time of around 34.7 seconds. The tested ASP solver is also more efficient in memory, using 44 MB on average, while 148 MB are used by Z3 to solve the SMT instances. The reason of such different performances is that SMT is a more expressive language, allowing arbitrary alternations of quantifies, while in ASP at most one alternation can be simulated by means of saturation techniques. It turns out that ASP solvers can implement more optimized algorithms for problems on the second level of the polynomial hierarchy. k-Clique-Coloring [ 29 ]. Given a graph G = (V, E) with n nodes, and an integer k ≥ 2, is possible to assign k colors to vertices in V such that each maximal clique K of G contains two vertices of different colors? The tested encoding using non-convex sums is reported below (again, its non-propositional version was actually tested). xc ← ∼∼xc ⊥ ← SUM[1 : x1, . . . , 1 : xk] 6= 1. ⊥ ← ∼saturate inx ∨ out x ← inx ← saturate out x ← saturate saturate ← inx, iny saturate ← inx, iny, xc, yd saturate ← out x, SUM[n : saturate, − 1 : iny1 , . . . , −1 : inyn−1 , 1 : inz1 , . . . , 1 : inzj ] ≥ 0 ∀x ∈ V, ∀c ∈ [1..k] ∀x ∈ V ∀x ∈ V ∀x ∈ V ∀x ∈ V ∀x, y ∈ V, x 6= y, (x, y) ∈/ E ∀x, y ∈ V, ∀c, d ∈ [1..k], c 6= d ∀x ∈ V, where {y1, . . . , yn−1} = V \ {x}, {z1, . . . , zj } = {z | (x, z) ∈ E} Intuitively, a color is assigned to each vertex, and the saturation is activated whenever one of the following conditions is verified: – the guessed K contains two non-adjacent nodes, i.e., K is not a clique; – the guessed K contains two nodes with different colors; – there is a vertex x ∈ V \ K such that x is adjacent to all vertices in K, i.e., K is not a maximal clique.

The alternative encoding not using recursive sums is obtained by replacing the last rule above with the following rule: saturate ← out x, out y1 , . . . , out yj

∀x ∈ V where {y1, . . . , yj } = {y ∈ V \ {x} | (x, y) ∈/ E}. Intuitively, in this case the third condition leading to saturate is the following: – there is a vertex x ∈ V \ K such that all vertices in V that are not adjacent to x do not belong to K, i.e., K is not a maximal clique.

For this problem, both encodings lead to solve all tested instances, which are the graphs submitted to the 4th ASP Competition [ 2 ] for the Graph Coloring problem. However, the overhead due to the use of recursive non-convex aggregates slows the computation down by a factor of 8, and also the memory consumption is around 4 times higher. 2-QBF. Given a 2-DNF ∃x∀yφ, is the formula valid? The tested encoding not using sums is the following: x ← ∼∼x ⊥ ← ∼saturate yT ∨ yF ← yT ← saturate yF ← saturate saturate ← μ(l1), . . . , μ(ln) ∀x ∈ x ∀y ∈ y ∀y ∈ y ∀y ∈ y ∀l1 ∧ · · · ∧ ln ∈ φ, n ≥ 1 where μ(x) = x and μ(¬x) = ∼x for all x ∈ x, and μ(y) = yT and μ(¬y) = yF for all y ∈ y. An equivalent encoding using non-convex sums can be obtained by replacing all rules with yT or yF in the head with the following rules: yT yF ← SUM[1 : saturate, −1 : yF ] ≥ 0 ← SUM[1 : saturate, −1 : yT ] ≥ 0 ∀y ∈ y ∀y ∈ y The tested instances are all the 2-QBF instances in the QBF Gallery 2014 (http: //qbf.satisfiability.org/gallery/results.html). Also in this case there is an overhead due to the unnatural use of non-convex sums. It impacts significantly on the Application Track, where the difference in terms of solved instances is 6. 6

Related Work

F-stable model semantics [ 14, 17 ] is implemented by widely-used ASP solvers [ 15, 20 ]. The original definition in [ 14, 17 ] is slightly different than the one provided in Section 2. In fact, propositional formulas can be arbitrarily nested in [ 17 ], while a more constrained structure is assumed in this paper in order to achieve an efficient implementation. On the other hand, double negation is not permitted in [ 14 ], even if it can be simulated by means of auxiliary atoms: a rule p ← ∼∼p can be equivalently encoded by using a fresh atom pF and the following subprogram: {p ← ∼pF , pF ← ∼p}. Similarly, negated literals cannot occur in the aggregates considered by [ 14 ] but again can must be encoded by means of auxiliary atoms. Another difference with [ 14 ] is on negated aggregates, which are not permitted by the language considered in this paper because [ 17 ] and [ 14 ] actually assign different semantics to programs with negated aggregates. As a final remark, the reduct of [ 14 ] does not remove negated literals from satisfied bodies, which however are necessarily true in all counter-models because double negation is not allowed.

Techniques to rewrite logic programs with aggregates into equivalent programs with simpler aggregates were investigated in the literature right from the beginning [ 32 ]. In particular, rewritings into LPARSE-like programs, which differ from those presented in this paper, were considered in [ 26 ]. As a general comment, since disjunction is not considered in [ 26 ], all aggregates causing a jump from the first to the second level of the polynomial hierarchy are excluded a priori. This is the case for aggregates of the form SUM(S) 6= b, AVG(S) 6= b, and COUNT(S) 6= b, as first noted by [ 33 ], but also for comparators other than 6= when negative weights are involved. In fact, in [ 26 ] negative weights are eliminated by a rewriting similar to the one in (4), but negated literals are introduced instead of auxiliary atoms, which may lead to unintuitive results [ 18 ]. A different rewriting was presented by [ 17 ], whose output are programs with nested expressions, a construct that is not supported by current ASP systems. Other relevant rewriting techniques were proposed in [ 8, 7 ], and proved to be quite efficient in practice. However, these rewritings produce aggregate-free programs preserving F-stable models only in the stratified case, or if recursion is limited to convex aggregates. On the other hand, it is interesting to observe that the rewritings of [ 8, 7 ] are applicable to the output of the rewritings presented in this paper in order to completely eliminate aggregates, thus preserving F-stable models in general.

Several other stable model semantics were proposed for interpreting logic programs with aggregates. Many of these semantics rely on stability checks that are not based on minimality [ 30, 31, 33 ], and therefore the rewritings presented by [ 4 ] and recalled in Section 3 cannot be used for these semantics. A more recent proposal is based on a stability check that essentially eliminates aggregates from program reducts [ 23 ], and therefore the rewritings by [ 4 ] cannot help also in this case. Finally, there are other ASP constructs that are semantically close to aggregates, such as DL [ 13 ] and HEX [ 12 ] atoms, for interacting with external knowledge bases possibly expressed in different languages; as these constructs cannot be compactly reduced to sums in general, the rewritings by [ 4 ] do not apply to these languages as well. 7

Conclusion

ASP takes advantage of several constructs to ease the representation of complex knowledge. Aggregation functions are among the most commonly used constructs in ASP specifications. The rewritings proposed by [ 4 ] provide a concrete simplification of the structure of aggregations in input programs, so to improve the efficiency of low-level reasoners. Such rewritings are implemented in a prototype system, presented in this paper, which reported a reasonable performance on benchmarks for which more tailored encodings using disjunction in rule heads exist. More relevant, when such an aggregate-free encoding is unknown or untuitive, for example in the Generalized Subset Sum problem, the rewritings implemented in the prototype are particularly useful. Indeed, in this specific benchmark ASP solving significantly outperforms an alternative encoding in the more expressive language of SMT.

It must be remarked that this is only a preliminary evaluation of recursive nonconvex aggregates in ASP. For the future, we plan to collect more encodings for problems that can be easily represented by using recursive non-convex aggregates, so to obtain a more suitable test suite for evaluating the efficiency of ASP solvers in presence of aggregations of this kind. Moreover, we will investigate alternative mappings of common aggregation functions into sums, with the aim of simplifying some of the rewritings by [ 4 ]. In particular, concerning ODD and EVEN, the rewritings by [ 4 ] are quadratic in size, and hence an interesting question to answer is whether there exist alternative rewritings of these aggregations whose sizes remain linear.

1. Abseher , M. , Bliem , B. , Charwat , G. , Dusberger , F. , Woltran , S. : Computing secure sets in graphs using answer set programming . In: Inclezan , D. , Maratea , M. (eds.) Seventh International Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2014 ) ( 2014 )

2. Alviano , M. , Calimeri , F. , Charwat , G. , Dao-Tran , M. , Dodaro , C. , Ianni , G. , Krennwallner , T. , Kronegger , M. , Oetsch , J. , Pfandler , A. , P u¨hrer, J., Redl , C. , Ricca , F. , Schneider , P. , Schwengerer , M. , Spendier , L.K. , Wallner , J.P. , Xiao , G. : The fourth answer set programming competition: Preliminary report . In: Cabalar, P. , Son , T.C. (eds.) LPNMR. pp. 42 - 53 . LNCS ( 2013 )

3. Alviano , M. , Faber , W.: The complexity boundary of answer set programming with generalized atoms under the FLP semantics . In: Cabalar, P. , Son , T.C. (eds.) Logic Programming and Nonmonotonic Reasoning , 12th International Conference, LPNMR 2013, Corunna, Spain, September 15-19 , 2013 . Proceedings. Lecture Notes in Computer Science , vol. 8148 , pp. 67 - 72 . Springer ( 2013 ), http://dx.doi.org/10.1007/978-3- 642 -40564- 8 _ 7

4. Alviano , M. , Faber , W. , Gebser , M. : Rewriting recursive aggregates in answer set programming: back to monotonicity . Theory and Practice of Logic Programming ( 2015 ), to appear

5. Bartholomew , M. , Lee , J. , Meng , Y. : First-order semantics of aggregates in answer set programming via modified circumscription . In: Logical Formalizations of Commonsense Reasoning, Papers from the 2011 AAAI Spring Symposium , Technical Report SS-11-06 , Stanford, California, USA, March 21 -23, 2011 . AAAI ( 2011 ), http://www.aaai.org/ ocs/index.php/SSS/SSS11/paper/view/2472

6. Berman , P. , Karpinski , M. , Larmore , L.L. , Plandowski , W. , Rytter , W.: On the complexity of pattern matching for highly compressed two-dimensional texts . J. Comput. Syst. Sci . 65 ( 2 ), 332 - 350 ( 2002 ), http://dx.doi.org/10.1006/jcss. 2002 .1852

7. Bomanson , J. , Gebser , M. , Janhunen , T. : Improving the normalization of weight rules in answer set programs . In: Ferme´, E. , Leite , J . (eds.) JELIA 2014 , Funchal, Madeira, Portugal, September 24-26 , 2014 . Proceedings. Lecture Notes in Computer Science , vol. 8761 , pp. 166 - 180 . Springer ( 2014 ), http://dx.doi.org/10.1007/ 978-3- 319 -11558-0_ 12

8. Bomanson , J. , Janhunen , T. : Normalizing cardinality rules using merging and sorting constructions . Lecture Notes in Computer Science , vol. 8148 , pp. 187 - 199 . Springer ( 2013 ), http://dx.doi.org/10.1007/978-3- 642 -40564-8_ 19

9. Brewka , G. , Eiter , T. , Truszczynski , M. : Answer set programming at a glance . Commun. ACM 54 ( 12 ), 92 - 103 ( 2011 ), http://doi.acm. org/10 .1145/2043174. 2043195

10. Eiter , T. , Tompits , H. , Woltran , S. : On solution correspondences in answer set programming . In: Kaelbling, L. , Saffiotti , A . (eds.) Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI'05) . pp. 97 - 102 . Professional Book Center ( 2005 )

11. Eiter , T. , Fink , M. , Krennwallner , T. , Redl , C. : Conflict-driven ASP solving with external sources . Theory and Practice of Logic Programming 12 ( 4-5 ), 659 - 679 ( 2012 ), http:// dx.doi.org/10.1017/S1471068412000233

12. Eiter , T. , Fink , M. , Krennwallner , T. , Redl , C. , Schu¨ller, P.: Efficient hex-program evaluation based on unfounded sets . J. Artif. Intell. Res. (JAIR) 49 , 269 - 321 ( 2014 ), http://dx. doi.org/10.1613/jair.4175

13. Eiter , T. , Ianni , G. , Lukasiewicz , T. , Schindlauer , R. , Tompits , H.: Combining answer set programming with description logics for the semantic web . Artif. Intell . 172 ( 12 - 13 ), 1495 - 1539 ( 2008 ), http://dx.doi.org/10.1016/j.artint. 2008 . 04 .002

14. Faber , W. , Pfeifer , G. , Leone , N.: Semantics and complexity of recursive aggregates in answer set programming . Artif. Intell . 175 ( 1 ), 278 - 298 ( 2011 ), http://dx.doi.org/10. 1016/j.artint. 2010 . 04 .002

15. Faber , W. , Pfeifer , G. , Leone , N. , Dell'Armi , T. , Ielpa , G. : Design and implementation of aggregate functions in the DLV system . Theory and Practice of Logic Programming 8 ( 5-6 ), 545 - 580 ( 2008 ), http://dx.doi.org/10.1017/S1471068408003323

16. Ferraris , P. : Answer sets for propositional theories . In: Baral, C. , Greco , G. , Leone , N. , Terracina , G . (eds.) Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05). Lecture Notes in Artificial Intelligence , vol. 3662 , pp. 119 - 131 . Springer-Verlag ( 2005 )

17. Ferraris , P. : Logic programs with propositional connectives and aggregates . ACM Trans. Comput. Log . 12 ( 4 ), 25 ( 2011 ), http://doi.acm. org/10 .1145/1970398. 1970401

18. Ferraris , P. , Lifschitz , V. : Weight constraints as nested expressions . Theory and Practice of Logic Programming 5 ( 1-2 ), 45 - 74 ( 2005 ), http://dx.doi.org/10.1017/ S1471068403001923

19. Gebser , M. , Kaminski , R., K o¨nig, A. , Schaub , T. : Advances in gringo series 3 . In: Delgrande, J.P. , Faber , W. (eds.) LPNMR 2011 , Vancouver, Canada, May 16 -19, 2011 . Proceedings. Lecture Notes in Computer Science , vol. 6645 , pp. 345 - 351 . Springer ( 2011 ), http:// dx.doi.org/10.1007/978-3- 642 -20895-9_ 39

20. Gebser , M. , Kaufmann , B. , Schaub , T. : Conflict-driven answer set solving: From theory to practice . Artif. Intell . 187 , 52 - 89 ( 2012 ), http://dx.doi.org/10.1016/j. artint. 2012 . 04 .001

21. Gelfond , M. , Lifschitz , V. : The stable model semantics for logic programming . In: Kowalski, R.A. , Bowen , K.A . (eds.) Logic Programming , Proceedings of the Fifth International Conference and Symposium , Seattle, Washington, August 15-19 , 1988 ( 2 Volumes) . pp. 1070 - 1080 . MIT Press ( 1988 )

22. Gelfond , M. , Lifschitz , V. : Classical negation in logic programs and disjunctive databases. New Generation Comput . 9 ( 3 /4), 365 - 386 ( 1991 ), http://dx.doi.org/10.1007/ BF03037169

23. Gelfond , M. , Zhang , Y.: Vicious circle principle and logic programs with aggregates . Theory and Practice of Logic Programming 14 ( 4-5 ), 587 - 601 ( 2014 ), http://dx.doi.org/ 10.1017/S1471068414000222

24. Janhunen , T. , Niemela¨, I. : Applying visible strong equivalence in answer-set program transformations . In: Erdem, E. , Lee , J. , Lierler , Y. , Pearce , D . (eds.) Correct Reasoning: Essays on Logic-Based AI in Honour of Vladimir Lifschitz. Lecture Notes in Computer Science , vol. 7265 , pp. 363 - 379 . Springer-Verlag ( 2012 )

25. Lifschitz , V. , Pearce , D. , Valverde , A. : Strongly equivalent logic programs . ACM Transactions on Computational Logic 2 ( 4 ), 526 - 541 ( 2001 )

26. Liu , G. , You , J.: Relating weight constraint and aggregate programs: Semantics and representation . Theory and Practice of Logic Programming 13 ( 1 ), 1 - 31 ( 2013 ), http://dx. doi.org/10.1017/S147106841100038X

27. Liu , L. , Pontelli , E. , Son , T.C. , Truszczynski , M. : Logic programs with abstract constraint atoms: The role of computations . Artif. Intell . 174 ( 3-4 ), 295 - 315 ( 2010 ), http://dx. doi.org/10.1016/j.artint. 2009 . 11 .016

28. Liu , L. , Truszczynski , M. : Properties and applications of programs with monotone and convex constraints . J. Artif. Intell. Res. (JAIR) 27 , 299 - 334 ( 2006 ), http://dx.doi.org/ 10.1613/jair.2009

29. Marx , D. : Complexity of clique coloring and related problems . Theor. Comput. Sci . 412 ( 29 ), 3487 - 3500 ( 2011 )

30. Pelov , N. , Denecker , M. , Bruynooghe , M.: Well-founded and stable semantics of logic programs with aggregates . Theory and Practice of Logic Programming 7 ( 3 ), 301 - 353 ( 2007 ), http://dx.doi.org/10.1017/S1471068406002973

31. Shen , Y. , Wang , K. , Eiter , T. , Fink , M. , Redl , C. , Krennwallner , T. , Deng , J.: FLP answer set semantics without circular justifications for general logic programs . Artif. Intell . 213 , 1 - 41 ( 2014 ), http://dx.doi.org/10.1016/j.artint. 2014 . 05 .001

32. Simons , P. , Niemela¨, I. , Soininen , T. : Extending and implementing the stable model semantics . Artif. Intell . 138 ( 1-2 ), 181 - 234 ( 2002 ), http://dx.doi.org/10.1016/ S0004- 3702 ( 02 ) 00187 -X

33. Son , T.C. , Pontelli , E.: A constructive semantic characterization of aggregates in answer set programming . Theory and Practice of Logic Programming 7 ( 3 ), 355 - 375 ( 2007 ), http: //dx.doi.org/10.1017/S1471068406002936

34. Turner , H.: Strong equivalence made easy: nested expressions and weight constraints . Theory and Practice of Logic Programming 3 ( 4-5 ), 609 - 622 ( 2003 )