=Paper=
{{Paper
|id=Vol-1451/paper1
|storemode=property
|title=Evaluating Answer Set Programming with Non-Convex Recursive Aggregates
|pdfUrl=https://ceur-ws.org/Vol-1451/paper1.pdf
|volume=Vol-1451
|dblpUrl=https://dblp.org/rec/conf/aiia/Alviano15
}}
==Evaluating Answer Set Programming with Non-Convex Recursive Aggregates==
https://ceur-ws.org/Vol-1451/paper1.pdf
Evaluating Answer Set Programming with Non-Convex
Recursive Aggregates
Mario Alviano
Department of Mathematics and Computer Science,
University of Calabria, 87036 Rende (CS), Italy
alviano@mat.unical.it
Abstract. Aggregation functions are widely used in answer set programming
(ASP) for representing and reasoning on knowledge involving sets of objects col-
lectively. 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 lim-
ited 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.
Keywords: answer set programming, aggregation functions, non-convex recur-
sive aggregates
1 Introduction
Answer set programming (ASP) is a declarative language for knowledge representa-
tion 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 knowl-
edge. 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
1
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
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 seman-
tics 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 F-
stable model semantics was incomplete, and recursion over aggregates was restricted to
convex aggregates [28], the largest class of aggregates for which the common reason-
ing 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: ∃x1 x2 ∀y1 y2 (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
2
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
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 liter-
als. 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(Π).
Example 1. Consider the following program Π1 :
x1 ← ∼∼x1 x2 ← ∼∼x2 y1 ← unequal y2 ← unequal ⊥ ← ∼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.
An interpretation I is a set of propositional atoms such that ⊥ ∈
/ I. Relation |= is
inductively defined as follows:
– for p ∈ V, I |= p if p ∈ I;
– I |= ∼l if I 6|= l; P
– I |= SUM[w1 : l1 , . . . , wn : ln ] b if i∈[1..n],I|=li wi b;
– for a rule r, I |= B(r) if I |= l for all l ∈ B(r), and I |= r if H(r) ∩ I 6= ∅ when
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 remov-
ing 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
3
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
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 non-
negative 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 pro-
gram 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 re-
spect 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. Simi-
larly, (E4) is immediate by the semantics introduced in Section 2. For (E2), instead, the
following equivalences can be observed:
4
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
(i) I |= SUM[w1 : l1 , . . . , wn : ln ] ≤ b;
P
(ii) wi ≤ b;
Pi∈[1..n], I|=li
(iii) i∈[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 ,
(3)
wk+1 : pk+1 , . . . , wm : pm ,
wm+1 : ∼lm+1 , . . . , wn : ∼ln ] b
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 : pF F
1 , . . . , w j : pj ,
wj+1 : ∼∼lj+1 , . . . , wk : ∼∼lk ,
(4)
wk+1 : pk+1 , . . . , wm : pm ,
wm+1 : ∼lm+1 , . . . , wn : ∼ln ] ≥ b + w1 + · · · + wk
where each pFi 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 (Π):
pF
i ← ∼pi (5)
pF
i ← aux (6)
pi ∨ pF
i ← ∼∼aux (7)
5
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
Similarly, if is 6=, then the following rules are added to rew (Π):
aux ← SUM[w1 : pF F
1 , . . . , wj : pj ,
wj+1 : ∼∼lj+1 , . . . , wk : ∼∼lk ,
(8)
wk+1 : pk+1 , . . . , wm : pm ,
wm+1 : ∼lm+1 , . . . , wn : ∼ln ] ≥ b + 1 + w1 + · · · + wk
aux ← SUM[w1 : p1 , . . . , wj : pj ,
wj+1 : ∼lj+1 , . . . , wk : ∼lk ,
(9)
wk+1 : pF F
k+1 , . . . , wm : pm ,
wm+1 : ∼∼lm+1 , . . . , wn : ∼∼ln ] ≥ −b + 1 + wk+1 + · · · + wn
together with rules (5)–(7) for each new pF i . Intuitively, any atom of the form pi in-
F
troduced 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 pF i 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
X k
X m
X n
X
−wi · I(pi ) + −wi · I(∼li ) + wi · I(pi ) + wi · I(∼li ) ≥ b (10)
i=1 i=j+1 i=k+1 i=m+1
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 k
X m
X
−wi · I(pi ) + −wi · I(∼li ) + wi · I(pi ) +
i=1 i=j+1 i=k+1
(11)
n
X k
X
+ wi · I(∼li ) + w1 + · · · + wk ≥ b + wi
i=m+1 i=1
and by distributivity (11) is equivalent to the following inequality:
j
X k
X
wi · (1 − I(pi )) + wi · (1 − I(∼li )) +
i=1 i=j+1
(12)
m
X n
X k
X
+ wi · I(pi ) + wi · I(∼li ) ≥ b + wi .
i=k+1 i=m+1 i=1
Note that 1−I(l) = I(∼l) for all literals l, and pF
i 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
6
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
in order to avoid oversimplifications in program reducts. Indeed, as already explained,
i will be derived true whenever pi is false, but also when the
for all i ∈ [1..j], atom pF
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 x2 ← ∼∼x2 y1 ← unequal y2 ← unequal ⊥ ← ∼unequal
unequal ← aux aux ← SUM[1 : xF F F F
1 ; 2 : x2 ; 2 : y1 ; 3 : y2 ] ≥ 4
aux ← SUM[1 : x1 ; 2 : x2 ; 2 : y1 ; 3 : y2 ] ≥ 6
xF1 ← ∼ x 1 xF
1 ← aux x1 ∨ xF 1 ← ∼∼aux
F F
x 2 ← ∼x 2 x2 ← aux x2 ∨ xF 2 ← ∼∼aux
y1F ← ∼y1 y1F ← aux y1 ∨ y1F ← ∼∼aux
y2F ← ∼y2 y2F ← aux y2 ∨ y2F ← ∼∼aux
1 , x2 , y1 , y2 }.
The only stable model of rew ∗ (Π1 ) is {x1 , unequal , y1 , y2 , aux , xF F F F
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 sys-
tem 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 vari-
ables 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
7
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
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 . unequal : − f sum(uneq, "!=", 5).
x2 : − not not x2 . f set(uneq, 1, x1 ).
y1 : − unequal. f set(uneq, 2, x2 ).
y2 : − unequal. f set(uneq, 2, y1 ).
: − not unequal. 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). all(y1 , 2). bound(5).
exists(x2 , 2). all(y2 , 3).
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 unde-
fined 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 rep-
resentation 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.
8
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
5 Experiment
The implemented rewritings were tested on a few domains that can be encoded us-
ing 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 natu-
ral 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 encod-
ing fed into Z 3. The other two problems considered in this experiment are k-Clique-
Coloring 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 in-
stances 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 Z 3 were tested with their default settings. Their performances were mea-
sured by PYRUNLIM (http://alviano.net/software/pyrunlim/). The re-
sults 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 Z 3 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
Table 1. Performance of GRINGO + CLASP (number of solved instances; average execution time
in seconds; average memory consumption in MB).
Aggregates Alternative
Benchmark inst sol time mem sol time mem
Generalized Subset Sum 46 38 1.1 44 n/a n/a n/a
k-Clique Coloring 60 60 177.2 863 60 20.9 205
Preprocessing Track 17 8 64.8 171 9 98.3 171
2-QBF
QBFLib Track 32 1 0.1 101 1 0.1 102
Application Track 48 13 126.1 45 19 22.7 45
9
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
As for Z 3, 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 Z 3 to solve the SMT instances. The reason of such different per-
formances 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 satura-
tion 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 ∀x ∈ V, ∀c ∈ [1..k]
⊥ ← SUM[1 : x1 , . . . , 1 : xk ] 6= 1. ∀x ∈ V
⊥ ← ∼saturate
in x ∨ out x ← ∀x ∈ V
in x ← saturate ∀x ∈ V
out x ← saturate ∀x ∈ V
saturate ← in x , in y ∀x, y ∈ V, x 6= y, (x, y) ∈/E
saturate ← in x , in y , xc , yd ∀x, y ∈ V, ∀c, d ∈ [1..k], c 6= d
saturate ← out x , SUM[n : saturate,
− 1 : in y1 , . . . , −1 : in yn−1 ,
1 : in z1 , . . . , 1 : in zj ] ≥ 0 ∀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
10
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
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 ∀x ∈ x
⊥ ← ∼saturate
yT ∨ yF ← ∀y ∈ y
y T ← saturate ∀y ∈ y
y F ← saturate ∀y ∈ y
saturate ← µ(l1 ), . . . , µ(ln ) ∀l1 ∧ · · · ∧ ln ∈ φ, n ≥ 1
where µ(x) = x and µ(¬x) = ∼x for all x ∈ x, and µ(y) = y T and µ(¬y) = y F for
all y ∈ y. An equivalent encoding using non-convex sums can be obtained by replacing
all rules with y T or y F in the head with the following rules:
y T ← SUM[1 : saturate, −1 : y F ] ≥ 0 ∀y ∈ y
y F ← SUM[1 : saturate, −1 : y T ] ≥ 0 ∀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 signifi-
cantly 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 Sec-
tion 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 imple-
mentation. 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 ag-
gregates. As a final remark, the reduct of [14] does not remove negated literals from
11
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
satisfied bodies, which however are necessarily true in all counter-models because dou-
ble 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 knowl-
edge. 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 tai-
lored encodings using disjunction in rule heads exist. More relevant, when such an
aggregate-free encoding is unknown or untuitive, for example in the Generalized Sub-
set 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.
12
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
It must be remarked that this is only a preliminary evaluation of recursive non-
convex aggregates in ASP. For the future, we plan to collect more encodings for prob-
lems 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 pres-
ence 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.
References
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 Interna-
tional 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ü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 general-
ized 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 program-
ming: 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 pro-
gramming via modified circumscription. In: Logical Formalizations of Commonsense Rea-
soning, Papers from the 2011 AAAI Spring Symposium, Technical Report SS-11-06, Stan-
ford, 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: Fermé, E., Leite, J. (eds.) JELIA 2014, Funchal,
Madeira, Portugal, September 24-26, 2014. Proceedings. Lecture Notes in Computer Sci-
ence, 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 con-
structions. 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. Com-
mun. ACM 54(12), 92–103 (2011), http://doi.acm.org/10.1145/2043174.
2043195
13
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
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 Con-
ference 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., Schü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 an-
swer 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., Ter-
racina, 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 Prac-
tice of Logic Programming 5(1-2), 45–74 (2005), http://dx.doi.org/10.1017/
S1471068403001923
19. Gebser, M., Kaminski, R., Kö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 the-
ory 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 Confer-
ence 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., Niemelä, I.: Applying visible strong equivalence in answer-set program trans-
formations. 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 Transac-
tions on Computational Logic 2(4), 526–541 (2001)
14
M.Alviano Evaluating ASP with Non-Convex Recursive Aggregates
26. Liu, G., You, J.: Relating weight constraint and aggregate programs: Semantics and repre-
sentation. 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 con-
vex 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 pro-
grams 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., Niemelä, I., Soininen, T.: Extending and implementing the stable model se-
mantics. 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)
15