From Non-Convex Aggregates to Monotone Aggregates in ASP

1 Introduction

Answer set programming (ASP) is a declarative language for knowledge representation and reasoning [Brewka et al., 2011]. In ASP knowledge is encoded by means of logic rules, possibly using disjunction and default negation, interpreted according to the stable model semantics [Gelfond and Lifschitz, 1988; 1991]. In a nutshell, stable models are minimal models of a program reduct obtained by deleting rules whose body is false, and by fixing the interpretation of negative literals in the remaining rules. Hence, stable models are those models that contain only necessary atoms under the assumption they provide for default negated formulas.

Since its first proposal, the basic language was extended by several constructs in order to ease the representation of practical knowledge, and particular interest was given to aggregate functions [Simons et al., 2002; Liu et al., 2010; Bartholomew et al., 2011; Faber et al., 2011; Ferraris, 2011; Gelfond and Zhang, 2014]. In fact, aggregates allow for expressing properties on sets of atoms collectively, and are

⇤This work is based on a paper presented at the 31st International Conference on Logic Programming (ICLP 2015) [Alviano et al., 2015]. Mario Alviano 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).

Martin Gebser

University of Potsdam, Germany gebser@cs.uni-potsdam.de

widely used for example to enforce functional dependencies, where a rule of the 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. Among the several semantics proposed for interpreting ASP programs with aggregates, two of them [Faber et al., 2011; Ferraris, 2011] are implemented in widely-used ASP solvers [Faber et al., 2008; Gebser et al., 2012]. The two semantics agree for programs without negated aggregates, and are thus referred indistinctly in this paper as F-stable model semantics (where we often leave "F-" implicit in the following). Interestingly, under this restriction F-stable models can be still defined as minimal models of a program reduct obtained by deleting rules whose body is false, and by fixing the interpretation of negative literals in the remaining rules [Alviano et al., 2015], exactly as in the aggregate-free case.

Non-convex aggregations are of particular interest because they may arise in several contexts while modeling complex knowledge [Eiter et al., 2008; 2012; Abseher et al., 2014]. A minimalistic example is provided by the ⌃P2 -complete problem called Generalized Subset Sum [Berman et al., 2002], where two vectors u and v of integers as well as an integer b are given, and the task is to decide whether the formula 9x8y(ux + vy 6= b) is true, where x and y are vectors of binary variables of the same length as u or 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: 9x1x28y1y2(1 · x1 + 2 · x2 + 2 · y1 + 3 · y2 6= 5). Any natural encoding of such an instance would include a non-convex aggregate of the form SUM[1 : x1↪ 2 : x2↪ 2 : y1↪ 3 : y2] 6= 5, which was not correctly handled by any ASP system before 2015. In fact, despite the fact that F-stable models were first proposed more than a decade ago, a complete implementation of non-convex aggregates was achieved only last year in the paper that this one is based on [Alviano et al., 2015].

Supporting non-convex aggregates was a challenge because typical ASP systems implement a two phases computation: first, the grounding phase instantiates the input program; then, the stable models of the ground program are computed by the solving phase. The two phases thus handle different input formats: while the grounding phase can process any program written by the user, the solving phase expects to read ground programs having a limited structure. In particular, the solving phase expects aggregates to be of a simple form known as monotone aggregates, and many common reasoning tasks on normal programs with monotone aggregates belong to the first level of the polynomial hierarchy, while in general they belong to the second level for normal programs with aggregates [Faber et al., 2011; Ferraris, 2011]. This observation already evidences that all rewriting techniques introduced before 2015 are applicable only if recursion is limited to convex aggregates [Liu and Truszczy´nski, 2006], 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 [Alviano and Faber, 2013]. In order to bridge the complexity gap between monotone and non-convex aggregates, introducing disjunction in rule heads is necessary, and it is actually the missing tile of the puzzle, discovered in [Alviano et al., 2015].

The translation is however non-trivial because in general non-convex aggregates have to be replaced by disjunctions of monotone aggregates, so that an auxiliary atom representing the truth value of a non-convex aggregate can be derived whenever some of the monotone aggregates in the disjunction is true. In logic programming, the conventional approach for encoding such a disjunction consists in a set of rules, each having the auxiliary atom in the head and one of the monotone aggregates in the body. However, often this conventional approach can only preserve models, but not stable models. In fact, recall that stable models are minimal models of a program reduct, and the program reduct only contains rules whose body is true. So how to guarantee that all rules resulting from the translation of a non-convex aggregate survive in a program reduct when the aggregate is true? In addition, the program reduct is such that the interpretation of negative literals is fixed. That is, how to guarantee that the interpretation of positive literals in the non-convex aggregate does not become fixed in program reducts? These and related "optimization" issues have been solved in our previous work [Alviano et al., 2015]. The basic ideas and intuitions of the translation function presented at ICLP 2015 are given in this paper. In particular, the paper focuses on SUM, as all other aggregation functions considered in [Alviano et al., 2015] can be translated to sums by using strong equivalences [Lifschitz et al., 2001; Turner, 2003; Ferraris, 2011].

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:

where n ≥ 0, b↪w1↪ ▷ ▷ ▷ ↪wn are integers, l1↪ ▷ ▷ ▷ ↪ ln are propositional literals, ⊙ 2 ¶<↪↪≥↪>↪=↪6=♦, and [w1 : l1↪ ▷ ▷ ▷ ↪wn : ln] is a multiset. (Note that this notation of propositional aggregates differs fromASP-Core-2 format 1 for ease of presentation.) A literal is either a propositional literal, or an aggregate. A rule r is of the following form:

1 https://www.mat.unical.it/aspcomp2013/ASPStandardization/

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 (⇧).

Example 1. Consider the following program⇧1:

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 ? ◁2 I, and associates literals with binary digits as follows: for p 2 V, I(p) equals 1 if p 2 I, and 0 otherwise; I(⇠l) := 1-I(l); I(SUM[w1 : l1↪ ▷ ▷ ▷ ↪wn : ln] ⊙b) equals 1 if Pi2[1▷▷n] wiI(li) ⊙ b, and 0 otherwise.

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♦. ⌅

Relation ♣= is inductively defined as follows: for a literal l, I ♣= l if I(l) = 1; for a rule r of the form (2), I ♣= B(r) if I ♣= li for all i 2 [1▷▷n], and I ♣= r if H(r) \ I 6= ; when I ♣= B(r); for a program ⇧, I ♣= ⇧ if I ♣= r for all r 2 ⇧. 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 is inductively defined: for p 2 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 2 ⇧↪ 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 ⇧. Two programs ⇧ and ⇧0 are equivalent with respect to a context V ✓ V, denoted ⇧ ⌘V ⇧0 , if both ♣SM(⇧)♣ = ♣SM(⇧0 )♣ and ¶I \ V ♣ I 2 SM(⇧)♦ = ¶I \ V ♣ I 2 SM(⇧0 )♦.

Example 3. Continuing with Example 2, the only stable model of ⇧1 is ¶x1↪ unequal ↪ y1↪ y2♦. Indeed, the reduct F (¶x1↪ unequal ↪ y1↪ y2♦↪ ⇧1) is

and no strict subset of ¶x1↪ unequal ↪ y1↪ y2♦ is a model of the above program. On the other hand, the reduct F (¶x2↪ unequal ↪ y1↪ y2♦↪ ⇧1) is

and ¶x2↪ y2♦ is a model of the above program. Similarly, it can be checked that ¶unequal ↪ y1↪ y2♦ and ¶x1↪ x2↪ unequal ↪ y1↪ y2♦ are not stable models of ⇧1. ⌅

Example 4. Resorting again to Example 2, note that the aggregate SUM[1 : x1↪ 2 : x2↪ 2 : y1↪ 3 : y2] 6= 5 is non-convex. Replacing 6= with > (resp. <) would result into a monotone (resp. convex) aggregate. ⌅

An aggregate A is monotone (in program reducts) if J ♣= F(I↪ A) implies K ♣= F(I↪ A), for all J ✓ K ✓ I ✓ V, and it 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; when either property applies, I ♣= A and J ♣= F(I↪ A) yield K ♣= F(I↪ A), for all J ✓ K ✓ I.

3 Compilation

Current ASP solvers (as opposed to grounders) only accept a limited set of aggregates, essentially sums of the form (1) such that b↪ w1↪ ▷ ▷ ▷ ↪ wn are non-negative integers, and ⊙ is ≥. The corresponding class of programs will be referred to as LPARSE-like programs. Hence, compilations from the general language are required. More formally, what is needed is a polynomial-time computable function associating every program ⇧ with an LPARSE-like program ⇧0 such that ⇧ ⌘At(⇧) ⇧0 . Such a function was given in [Alviano et al., 2015], and is briefly recalled in this section. Before, however, it is instructive to consider a few examples that show why other approaches fail to preserve stable models.

Example 5. Consider program ⇧1 from Example 1 and the following program ⇧2, often used as an intermediate step to obtain an LPARSE-like program:

The two programs differ only subtly: the last rule of ⇧1 is replaced by two rules in ⇧2, following the intuition that the original aggregate is true in an interpretation I if and only if either I ♣= SUM[1 : x1↪ 2 : x2↪ 2 : y1↪ 3 : y2] > 5 or I ♣= SUM[1 : x1↪ 2 : x2↪ 2 : y1↪ 3 : y2] < 5. However, the two programs are not equivalent. Indeed, it can be checked that ⇧2 has no stable model, and in particular ¶x1↪ unequal ↪ y1↪ y2♦ is not stable because F (¶x1↪ unequal ↪ y1↪ y2♦↪ ⇧2) is

and ¶x1♦ is one of its models.

⌅

Example 5 is essentially the origin of the first question posed in the introduction: How to guarantee that all rules resulting from the translation of a non-convex aggregate survive in a program reduct when the aggregate is true? Another obstacle for previous translation functions is represented by negative integers, whose substitution may change the semantics of programs.

Example 6. Let ⇧3 be the following program:

Its only stable model is ¶p↪ q♦. The negative integer is usually removed by means of a rewriting adapted from pseudoBoolean constraint solvers, which replaces each element w : l in (1) such that w < 0 by -w : ⇠l, and also adds -w to b. The resulting program in this example is

which has no stable models. In particular, ¶p↪ q♦ is not stable because in the program reduct the aggregate is replaced by SUM[1 : p↪ 1 : ?] ≥ 1, and therefore ; is a smaller model. ⌅

Example 6 is thus the origin of the second question posed in the introduction: How to guarantee that the interpretation of positive literals in the non-convex aggregate does not become fixed in program reducts? Actually, the fact that rewritings such as those hinted in the above examples do not preserve stable models in general can be also explained via complexity arguments. Indeed, while checking the existence of a stable model is ⌃P2 -complete for programs with atomic heads, this problem is in NP for LPARSE-like programs with atomic heads, and disjunction is necessary for modeling ⌃P2 - hard instances. It follows that, unless the polynomial hierarchy collapses to its first level, a polynomial-time compilation must possibly introduce disjunction when rewriting recursive programs. This intuition is used in Section 3.2. Before, in Section 3.1, the structure of input programs is simplified by rewriting sums so that comparison operators are either ≥ or 6=; after this simplification, negative integers and 6= constitute the remaining gap to LPARSE-like programs.

3.1 Mapping to sums

The notion of strong equivalence [Lifschitz et al., 2001; Turner, 2003; Ferraris, 2011] will be used in this section. Let ⇡ := l1 ^· · ·^ln be a conjunction of literals, for some n ≥ 0. A pair (J↪ I) of interpretations such that J ✓ I is an SEmodel 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.

The following strong equivalences can be proven by showing equivalence with respect to models, and by noting that ⇠ is neither introduced nor eliminated:

For example, (A) is based on the fact that the following statements are equivalent, for every interpretation I:

1. I ♣= SUM[w1 : l1↪ ▷ ▷ ▷ ↪wn : ln]  b;
2. Pi2[1▷▷n] -wiI(li) ≥ -b;
3. Pi2[1▷▷n] wiI(li)  b;
4. I ♣= SUM[-w1 : l1↪ ▷ ▷ ▷ ↪-wn : ln] ≥ -b.

Similar observations apply to (B)-(E). The application of (A)-(E), from the last to the first, to a program ⇧ gives an equivalent program ⇧0 with sums over distinct literals associated with integers different from zero, and whose comparison operators are ≥ and 6=.

3.2 Eliminating non-monotone aggregates

The structure of program ⇧0 can be further simplified by eliminating non-monotone aggregates. (To ease the presentation, in the following we call an aggregate A non-monotone if it contains a negative integer, or if ⊙ is 6=, thus disregarding special cases in which A would still be monotone or convex.) For an aggregate A of the form (1) such that ⊙ is ≥, we define a rule with a fresh propositional atom aux, representing the truth value of A, as head and a monotone aggregate as body:

Note that any (wi : li) such that wi < 0 and li ◁2 V is replaced by (-wi : ⇠li), thus rewarding the falsity of li rather than penalizing li, which is in turn compensated by adding -wi to the bound b; such a replacement preserves models even if condition li ◁2 V is removed [Simons et al., 2002], while this is not the case for stable models [Ferraris and Lifschitz, 2005]. For this reason, for any li 2 V associated with a negative weight in A, (3) introduces a fresh, hidden propositional atom lF i [Eiter et al., 2005; Janhunen and Niemel¨a, 2012], and the following rules are also added to the rewritten program:

Intuitively, lF i must be true whenever li is false, but alsowhen aux is true, so to implement the concept of saturation [Eiter and Gottlob, 1995]. Rules (4) and (5) encode such an intuition. Moreover, rule (6) guarantees that at least one of li and lF i belongs to any model of reducts obtained from interpretations I containing aux. In fact, lF i represents the falsity of li in the reduct of rule (3) with respect to I in order to test the satisfaction of the monotone aggregate in (3) relative to subsets of I.

Example 7. Consider ⇧3 from Example 6, and the following program ⇧03 obtained by applying the rewriting above:

Since SM(⇧03 ) consists of the stable model ¶p↪ q↪ aux↪ qF ♦ only, we have ⇧3 ⌘¶p↪q♦ ⇧03 . That is, the two programs are equivalent with respect to the visible atoms ¶p↪ q♦ . ⌅

Note that so far the rewriting of non-monotone aggregates provided an answer to the second question posed in the introduction, i.e., the interpretation of positive literals is not fixed in program reducts thanks to the addition of auxiliary atoms that allow for checking all possible assignments. In order to also answer the first question posed in the introduction, the rewriting has to be extended to an aggregate A := SUM[w1 : l1↪ ▷ ▷ ▷ ↪wn : ln] 6= b. In fact, we are going to consider two cases based on splitting A into A> := SUM[w1 : l1↪ ▷ ▷ ▷ ↪wn : ln] ≥ b + 1 and A< := SUM[-w1 : l1↪ ▷ ▷ ▷ ↪-wn : ln] ≥ -b + 1. (Note that A> ⌘SE SUM[w1 : l1↪ ▷ ▷ ▷ ↪wn : ln] > b, and A< ⌘SE SUM[w1 : l1↪ ▷ ▷ ▷ ↪wn : ln] < b.) In a nutshell, all occurrences of A are replaced by a fresh atom aux , which is also the head of two new rules of the form (3), one for A> and one for A<. Moreover, rules of the form (4)-(6) are introduced for each i 2 [1▷▷n] such that li 2 V, so that all possible assignments can still be checked in program reducts.

Example 8. Consider ⇧1 from Example 1, and the following program ⇧01 obtained by applying the rewriting above:

where rules of the form (4)-(6) for all li 2 ¶x1↪ x2↪ y1↪ y2♦ are omitted for brevity. Since the only stable model of ⇧01 is ¶x1↪ unequal ↪ y1↪ y2↪ aux↪ xF1 ↪ xF2 ↪ yF 1 ↪ yF 2 ♦, we have ⇧1 ⌘¶x1↪x2↪unequal ↪y1↪y2♦ ⇧01 . ⌅

It is important to note that the rewritten A> and A< are both true in the stable model above, which is eventually the answer to the first question posed in the introduction. In fact, the rewriting process described in this section can be iterated to eliminate all non-monotone aggregates from a program ⇧, where rew(⇧) denotes the resulting LPARSE-like program.

Theorem1. For any program⇧, we have⇧ ⌘At(⇧) rew(⇧).

4 Conclusion

The representation of knowledge in ASP is eased by the availability of several constructs, among them aggregation functions. As it is common in combinatorial problem solving, the structure of input instances is simplified in order to improve the efficiency of low-level reasoning. Concerning aggregation functions, the simplified form processed by current ASP solvers is known as monotone, and by complexity arguments faithfulness of any polynomial rewriting requires the introduction of disjunction if recursion is not limited to convex aggregates. Even though the translation presented in this paper is not particularly optimized towards actual recursion, an experiment reported in [Alviano, 2015] shows that it can pave the way to new applications of ASP. In fact, among 46 tested instances of Generalized Subset Sum, 38 were solved by GRINGO+CLASP within a timeout of 900 seconds, while the SMT solver Z3 could only solve 14 of these instances.