On the Properties of GZ-Aggregates in Answer Set Programming

1 Introduction

Answer set programming (ASP) is a declarative language for knowledge representation and reasoning [Brewka et al., 2011] powered by many efficient systems [Calimeri et al., 2016]. ASP specifications are sets of logic rules, possibly using disjunction and default negation, interpreted according to the stable model semantics [Gelfond and Lifschitz, 1988; 1991]. Default negation in particular eases the representation of decisions to be taken based on assumptions on unknown knowledge. In fact, a stable model I of an ASP program ⇧ has to satisfy all logic rules in ⇧, and in addition has to satisfy a stability condition: everything in I is necessary in order to satisfy all logic rules in ⇧ under the assumptions provided by I itself for default negated literals. Hence, the stability condition guarantees correctness of the assumptions on the unknown knowledge used in the reasoning process. Moreover, the stability condition enforces the vicious circle principle, which essentially asserts that the truth of an atom must be inferred by means of a definition not referring, directly or indirectly, to the truth of the atom itself.

The basic language is extended by several constructs to ease the representation of practical knowledge. Aggregate functions are among these extensions [Simons et al., 2002; Pelov et al., 2007; Son and Pontelli, 2007; Shen et al., 2014;

⇤This work is based on a paper presented at the International Conference on Logic Programming (ICLP 2015) [Alviano and Leone, 2015], and was partially supported by the Italian Ministry of University and Research under PON project "Ba2Know (Business Analytics to Know) Service Innovation - LAB", No. PON03PE 00001 1, and by Gruppo Nazionale per il Calcolo Scientifico (GNCS-INdAM).

Liu et al., 2010; Faber et al., 2011; Bartholomew et al., 2011], and allow to express properties on sets of atoms declaratively. For example, aggregate functions are often used to enforce functional dependencies; a rule of the following form:

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 aggregating over a multiset:

As a further example, aggregate functions ease the representation of logic circuits made of gates of unbounded fan-in [Gelfond and Zhang, 2014]; the following rule models that the output value of an XOR gate is 1 if an odd number of its inputs have value 1:

This last example is of particular interest, as it includes a recursive definition involving an aggregate. In fact, a strength of ASP is the possibility to represent and reason on recursive definitions, which are quite common in mathematics and computer science. However, when aggregates are involved in recursive definitions, the notion of stable model is nontrivial, and actually still under debate. Of the several semantics proposed for ASP programs with aggregates, two of them [Ferraris, 2011; Faber et al., 2011] are implemented in popular ASP solvers [Gebser et al., 2012; Faber et al., 2008], agree for programs without negated aggregates [Alviano et al., 2015], and are referred here as Fstable model semantics. They are essentially based on the stability condition reported at the beginning of this introduction: everything in a stable model I of an ASP program ⇧ is necessary for satisfying all logic rules in ⇧ under the assumptions provided by I itself for default negated literals.

Technically, F-stable models do not satisfy the vicious circle principle, as inference of atoms via definitions referring the truth values of the atoms themselves is not inhibited. Actually, in some cases violating the vicious circle principle is necessary for associating some stable models to a given ASP

program [Alviano and Faber, 2015b]. However, when possible, stable models obeying the vicious circle principle may be preferred, and this fact motivated an alternative semantics that was recently proposed by [Gelfond and Zhang, 2014], and is here referred to as GZ- or G-stable model semantics. In the new semantics, an assumption is also done on satisfied aggregates: they are satisfied because of the true atoms in their domains. The stability condition thus requires that everything in a stable model I of an ASP program ⇧ is necessary for satisfying all logic rules in ⇧ under the assumptions provided by I itself for both default negated literals and aggregates. Interestingly, G-stable models are F-stable models, but the converse is not always true [Alviano and Faber, 2015a].

Our previous paper [Alviano and Leone, 2015], honored with the Best Paper Award at the 31st International Conference on Logic Programming (ICLP 2015), explored this new semantics, reporting a detailed complexity analysis of coherence testing and cautious reasoning [Eiter and Gottlob, 1995], two of the main computational tasks in ASP. In a nutshell, coherence testing amounts to check the existence of a stable model of an input program, while cautious reasoning consists in checking whether a given atom is true in all stable models of the input program. A summary of the complexity results is reported in Table 1, where programs combining monotone (M), convex (C) and non-convex (N) aggregates with negation (⇠) and disjunction (_) are considered.

Concerning coherence testing, membership in ⌃P2 was proved in [Gelfond and Zhang, 2014], and we proved ⌃P2 - hardness already for negation-free programs with a very limited form of aggregate functions, referred to as monotone aggregates in the literature. This result is in contrast with Fstable model semantics, for which coherence of negation-free programs with monotone aggregates is guaranteed. Indeed, this is likely to be an unwanted artifact of G-stable models, which however also comes with an interesting and unique property: the increase in complexity also adds expressive power to the language, as aggregates referred to as monotone in the literature allow to simulate integrity constraints and possibly default negation when interpreted according to the semantics by [Gelfond and Zhang, 2014]. Eventually, the simulation of integrity constraints and default negation are the gadgets that we used to prove some complexity results for G-stable model semantics.

On the other hand, there are also many cases in which Gstable models actually decrease the complexity of the reasoning tasks. In fact, while any non-convex aggregate [Alviano and Faber, 2013] is sufficient to show ⌃P2 -hardness for Fcoherence testing already for disjunction-free programs, Gcoherence testing was proved to be NP-complete in general for disjunction-free programs. Finally, P-completeness was proved for programs with monotone aggregates if disjunction and negation are not used, a result compatible with F-stable model semantics. However, also in this case G-stable models allow to simulate integrity constraints, which is not possible with F-stable models.

As for the complexity of cautious reasoning, membership and hardness in the complementary complexity classes were proved for all the analyzed fragments of the language. These complexity results also implicitly characterize the computational complexity of another common reasoning task in ASP, known as brave reasoning, which consists in checking whether a given propositional atom is true in some stable model of an input program. In fact, brave reasoning has the same complexity of coherence testing when programs are interpreted under G-stable model semantics.

Further interesting results in [Alviano and Leone, 2015] are the two rewriting techniques for compiling programs interpreted according to G-stable model semantics into programs interpreted according to F-stable model semantics. While the first rewriting is simpler and introduces fewer auxiliary symbols, the second has the advantage of producing programs with non recursive aggregates only. These two rewritings, recalled in Section 3, are polynomial, faithful and modular translation functions [Janhunen, 2006], and are implemented in a system prototype. It is publicly available (http://alviano.net/software/g-stable-models/) and allows for experimenting with this newly proposed semantics.

2 Background

After defining the syntax of logic programs with aggregates, two semantics are introduced, referred to as F- [Ferraris, 2011; Faber et al., 2011] and G-stable models [Gelfond and Zhang, 2014]. (The original definitions are properly adapted to better fit the results in this paper.)

2.1 Syntax

Let T,F denote the Boolean truth values true and false, respectively. Let U be a finite set of propositional atoms. An aggregate A is a Boolean function whose domain, denoted dom(A), is a subset of U. A literal is a propositional atom or an aggregate possibly preceded by (one or more occurrences of) the negation as failure symbol ⇠. A rule r is an expression of the following form:

where p1↪ ▷ ▷ ▷ ↪ pm are propositional atoms, l1↪ ▷ ▷ ▷ ↪ ln are literals, m ≥ 1 and n ≥ 0. Set ¶p1↪ ▷ ▷ ▷ ↪ pm♦ is the head of r, denoted H(r), and set ¶l1↪ ▷ ▷ ▷ ↪ ln♦ is the body of r, denoted B(r). A program ⇧ is a finite set of rules of the form (1). The set of propositional atoms occurring in ⇧ is denoted At(⇧).

Example 1. Let A1 be an aggregate such that dom(A1) = ¶a↪ b♦ and A1(C) = ♣¶a↪ b♦ \C♣ ≥ 1, for all C ✓ dom(A1). A program using A1 is ⇧1 = ¶a ⇠⇠a; b _ c A1♦. ⌅

2.2 Semantics

An interpretation I is a subset of U. Let S↪ S0 be sets of interpretations, and C be a set of propositional atoms. Sets S and S0 are equivalent in the context C, denoted S ⌘C S0 , if ♣S♣ = ♣S0 ♣ and ¶I \C ♣ I 2 S♦ = ¶I \C ♣ I 2 S0 ♦.

Aggregates are classified in three groups [Liu and Truszczynski, 2006]. An aggregate A is monotone if A(I) = T implies A(J) = T, for all I ✓ J ✓ U. An aggregate A is convex if A(I) = A(K) = T implies A(J) = T, for all I ✓ J ✓ K ✓ U. The remaining aggregates are called non-convex. Note that monotone aggregates are convex, and the inclusion is strict.

Example 2. Let k be a natural number, and I be an interpretation. An aggregate A such that A(I) := ♣dom(A) \ I♣ ≥ k is monotone. An aggregate A such that A(I) := ♣dom(A) \ I♣ = k is convex. An aggregate A such that A(I) := ♣dom(A) \ I♣ 6= k is non-convex. ⌅

Relation ♣= is inductively defined as follows: for a propositional atom p 2 U, I ♣= p if p 2 I; for an aggregate A, I ♣= A if A(I \ dom(A)) = T; for a negated literal ⇠l, I ♣= ⇠l if I 6♣= l; for a set or conjunction C, I ♣= C if I ♣= p holds for each p 2 C; for a rule r, I ♣= r if H(r) \ I 6= ; whenever I ♣= B(r). I is a model of a program ⇧ if I ♣= ⇧, i.e., if I ♣= r for all r 2 ⇧.

Example 3. Continuing Example 1, the models of ⇧1, restricted to the atoms occurring in the program, are the following: ;, ¶a↪ b♦, ¶a↪ c♦, ¶a↪ b↪ c♦, ¶b♦, ¶b↪ c♦, and ¶c♦. ⌅

F-stable models. Let ⇧ be a program and I an interpretation. The F-reduct of ⇧ with respect to I is defined as follows: F(⇧↪ I) = ¶F(r↪ I) ♣ r 2 ⇧↪ I ♣= B(r)♦, where F(r↪ I) = p1_· · ·_pm F(l1↪ I)↪ ▷ ▷ ▷ ↪ F(ln↪ I) for r being of the form (1), F(l↪ I) = l if l is a propositional atom or an aggregate A, and F(l↪ I) = ; if l is a negative literal. I is an F-stable model of ⇧ if I ♣= ⇧ and there is no J ⇢ I such that J ♣= F(⇧↪ I). The set of F-stable models of ⇧ is denoted FSM (⇧).

Example 4. The F-stable models of ⇧1 in Example 1 are the following: ;, ¶a↪ b♦, and ¶a↪ c♦. Indeed, note that F(⇧1↪ ;) = ;, F(⇧1↪ ¶a↪ b♦) = F(⇧1↪ ¶a↪ c♦) = ¶a ; b _ c A1♦, and each model is minimal for its reduct. On the other hand, ¶b♦ is not an F-stable model because ; is a model of F(⇧1↪ ¶b♦) = ¶b _ c A1♦. ⌅

G-stable models. Let ⇧ be a program and I an interpretation. The G-reduct of ⇧ with respect to I is defined as follows: G(⇧↪ I) = ¶G(r↪ I) ♣ r 2 ⇧↪ I ♣= B(r)♦, where G(r↪ I) = p1 _ · · · _ pm G(l1↪ I)↪ ▷ ▷ ▷ ↪G(ln↪ I) for r being of the form (1), G(l↪ I) = l if l is a propositional literal, G(l↪ I) = I \dom(A) if l is an aggregate A, and G(l↪ I) = ; if l is a negative literal. I is a G-stable model of ⇧ if I ♣= ⇧ and there is no J ⇢ I such that J ♣= G(⇧↪ I). The set of G-stable models of ⇧ is denoted GSM (⇧).

Example 5. The G-stable models of ⇧1 in Example 1 are the following: ; and ¶a↪ c♦. Indeed, G(⇧1↪ ;) = ; and G(⇧1↪ ¶a↪ c♦) = ¶a ; b _ c a♦. Note that A1 is replaced by a in the last rule of G(⇧1↪ ¶a↪ c♦) because ¶a↪ c♦\dom(A1) = ¶a♦. Also observe that ¶a↪ b♦ is not a Gstable model because G(⇧1↪ ¶a↪ b♦) = ¶a ; b _ c a↪ b♦, and ¶a♦ is a model of this reduct. ⌅

Let X 2 ¶F↪ G♦. A program ⇧ is X-coherent if ⇧ has at least one X-stable model; otherwise, ⇧ is X-incoherent. Xcoherence testing is the computational problem of checking whether an input program ⇧ is X-coherent. A propositional atom p is an X-cautious consequence of ⇧ if p belongs to all X-stable models of ⇧. X-cautious reasoning is the computational problem of checking whether a given propositional atom p is an X-cautious consequence of an input program ⇧.

3 Compilation

G-stable models of a logic program can be computed via compilations into F-stable model semantics. Actually, two different rewritings are presented in this section. The first rewriting is more compact, in the sense that it introduces fewer auxiliary atoms. The second rewriting instead requires more auxiliary atoms, but has the advantage that the output program only comprise stratified aggregates (essentially, in these programs no recursive definition involves an aggregate; see [Faber et al., 2011] for a formal definition).

First Rewriting. Let rew(⇧) be the programobtained from program ⇧ by performing the following operations:

1. For each p 2 At(⇧) occurring in aggregates, a fresh atom p0 and the following rules are introduced:

1. For each rule r 2 ⇧ and each aggregate A 2 B(r) such that dom(A) = ¶p1↪ ▷ ▷ ▷ ↪ pn♦ (for some n ≥ 0), literals p01 ↪ ▷ ▷ ▷ ↪ p0n are added to the body of r.

Example 6. Consider again program ⇧1 from Example 1, whose G-stable models are ; and ¶a↪ c♦, as shown in Example 5. Program rew(⇧1) is the following:

Its F-stable models are the following: ; [ X and ¶a↪ c♦ [ X, where X = ¶a0 ↪ b0 ♦. In fact, a0 ↪ b0 are necessarily true because of rules of the form (2). Moreover, note that if a is false in some model I then a0 is necessarily true in any model of the reduct F(⇧1↪ I). On the other hand, if a is true in I then a0 can be possibly assumed false in a model of F (⇧1↪ I). Similarly for b and b0 . ⌅

A drawback of this first compilation is that the evaluation of the resulting program may be in a higher complexity class than the evaluation of the original program. For example, G-coherence testing of disjunction-free programs is NPcomplete in general, while a ⌃P2 procedure will be used to test F-coherence of the rewritten program.

Example 7. Let A2 be a non-convex aggregate such that dom(A2) = ¶a↪ b♦ and A2(C) = ♣¶a↪ b♦ \ C♣ 6= 1, for all C ✓ dom(A2). Let ⇧2 be the following program:

and rew(⇧2) be its rewriting:

Note that GSM(⇧2) = FSM(rew(⇧2)) = ;. However, G-coherence testing of ⇧2 is in NP, while F-coherence testing of programs with non-convex aggregates such as rew(⇧2) is ⌃P2 -complete in general. In fact, F-reducts may still contain (non-convex) aggregates; since a polytime procedure for testing subset minimality of a model for such programs is unknown, a nondeterministic guess is required in general. Continuing with program rew(⇧2), its Freduct with respect to ¶a↪ b↪ a0 ↪ b0 ♦ is the following program F (rew(⇧2)↪ ¶a↪ b↪ a0 ↪ b0 ♦):

which still contains the non-convex aggregate A2. In this case, ¶a↪ b↪ a0 ↪ b0 ♦ is not an F-stable model because ; is a model of F (rew(⇧2)↪ ¶a↪ b↪ a0 ↪ b0 ♦). ⌅

Such a drawback motivates the introduction of a second compilation. To ease the presentation, the syntax of the language is extended with integrity constraints, that is, rules of the form (1) with empty heads. Note that the semantics provided in Section 2 can already cope with such an extension.

Second Rewriting. Let str(⇧) be the program obtained from program ⇧ by performing the following operations:

1. For each p 2 At(⇧) occurring in aggregates, two fresh atoms p0 ↪ p00 and the following rules are introduced:

1. For each rule r 2 ⇧ and each aggregate A 2 B(r) such that dom(A) = ¶p1↪ ▷ ▷ ▷ ↪ pn♦ (n ≥ 0), literals p01 ↪ ▷ ▷ ▷ ↪ p0n are added to B(r), and A is replaced by a new aggregate A00 such that dom(A00 ) = ¶p00 1 ↪ ▷ ▷ ▷ ↪ p00n ♦ and A00 (I) = A(¶p 2 U ♣ p00 2 I♦), for all I ✓ U.

Example 8. Resorting again program ⇧1 from Example 1, str(⇧1) is the following program:

where dom(A00 1 ) = ¶a00 ↪ b00 ♦ and A00 1 (I) = ♣¶a00 ↪ b00 ♦ \ I♣ ≥ 1, for all I ✓ U. The F-stable models of str(⇧1) are the following: ;[X and ¶a↪ c♦[X[¶a00 ♦, where X = ¶a0 ↪ b0 ♦. In fact, for atoms a0 ↪ b0 , comments in Example 6 apply. Atom a00 instead is forced to have the same truth value of a because of rules of the form (4). Similarly for b00 and b. ⌅

Note that the additional auxiliary atoms of the form p00 in the second rewriting are used to fix the interpretation of aggregates in program reducts.

Example 9. Consider again program ⇧2 from Example 7, and its rewriting str(⇧2):

where dom(A00 2 ) = ¶a00 ↪ b00 ♦ and A00 2 (I) = ♣¶a00 ↪ b00 ♦\I♣ 6= 1, for all I ✓ U. The rewritten program str(⇧2) still contains a non-convex aggregate, namely A00 2 , which however is such that its interpretation is fixed in program reducts. Hence, any F-reduct of str(⇧2) can be considered as a program without negation and aggregates. For example, the F-reduct of str(⇧2) with respect to ¶a↪ b↪ a0 ↪ b0 ↪ a00 ↪ b00 ♦ is the following program F (str (⇧2)↪ ¶a↪ b↪ a0 ↪ b0 ↪ a00 ↪ b00 ♦):

Note that a00 and b00 are necessarily true in any model of the above program, which in turn implies truth of A2. ⌅

Correctness of the two rewritings presented in this section was formally proved by [Alviano and Leone, 2015].

Theorem 1. If ⇧ is a program, then

4 Conclusion

G-stable models are a recent proposal for interpreting logic programs with aggregates. A detailed complexity analysis of the main reasoning tasks for this new semantics was reported in [Alviano and Leone, 2015], and briefly recalled in the introduction of this paper, highlighting similarities and differences versus mainstream ASP semantics, here referred to as F-stable models. A practical link between G- and Fstable models is provided by the rewritings in Section 3: G-stable models of an input program can be obtained by computing F-stable models of a rewritten program, where the size of the rewritten program is linear with respect to the size of the original program. It is interesting to observe that the second rewriting in Section 3 is such that all atoms occurring in aggregates are defined only by rules of the form p00 ⇠⇠p00 . This fact is sufficient to guarantee that the rewritten programs contain stratified aggregates only, which are handled efficiently by modern ASP solvers. A prototype system for computing G-stable models is thus obtained by means of these rewritings and using existing ASP solvers as back-end. As a final remark, it is interesting to observe that the second rewriting in Section 3 can be combined with the rewritings by [Bomanson and Janhunen, 2013; Bomanson et al., 2014] in order to completely remove GZaggregates from ASP programs.