# compilation_of_aggregates_in_asp_systems__cb9d3d6c.pdf

Compilation of Aggregates in ASP Systems

Giuseppe Mazzotta, Francesco Ricca, Carmine Dodaro

Department of Mathematics and Computer Science, University of Calabria, Rende (CS), Italy giuseppe.mazzotta@unical.it, francesco.ricca@unical.it, carmine.dodaro@unical.it

Answer Set Programming (ASP) is a well-known declarative AI formalism for knowledge representation and reasoning. State-of-the-art ASP implementations employ the ground&solve approach, and they were successfully applied to industrial and academic problems. Nonetheless there are classes of ASP programs whose evaluation is not efficient (sometimes not feasible) due to the combinatorial blow-up of the program produced by the grounding step. Recent research suggests that compilation-based techniques can mitigate the grounding bottleneck problem. However, no compilationbased technique has been developed for ASP programs that contain aggregates, which are one of the most relevant and commonly-employed constructs of ASP. In this paper, we propose a compilation-based approach for ASP programs with aggregates. We implement it on top of a state-of-theart ASP system, and evaluate the performance on publiclyavailable benchmarks. Experiments show our approach is effective on ground-intensive ASP programs.

Introduction Answer Set Programming (ASP) (Brewka, Eiter, and Truszczynski 2011) is a declarative AI formalism for knowledge representation and reasoning based on the stable model semantics (Gelfond and Lifschitz 1991). ASP is a viable solution for representing and solving many classes of problems thanks to a standardized first-order language that has been implemented in several efficient systems (Gebser et al. 2018). Indeed, ASP has been successfully applied to several academic and industrial AI applications such as planning, scheduling, robotics, decision support, natural language understanding and more (cfr. (Erdem and Oztok 2015)). Albeit ASP is supported by efficient systems, the improvement of their performance is still an open and interesting research topic. State-of-the-art ASP systems are based on the ground&solve approach (Kaufmann et al. 2016). The first-order input program is transformed by the grounder module in its propositional counterpart, whose stable models are computed by the solver, implementing a Conflict-Driven Clause Learning (CDCL) algorithm (Kaufmann et al. 2016). ASP implementations based on ground&solve, basically, enabled the development of ASP applications. Nonethe-

Copyright 2022, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

less there are classes of ASP programs whose evaluation is not efficient (sometimes not feasible) due to the combinatorial blow-up of the program produced by the grounding step. This issue is known under the term grounding bottleneck (Ostrowski and Schaub 2012; Calimeri et al. 2016). Many attempts have been done to approach the grounding bottleneck, from language extensions (Ostrowski and Schaub 2012; Balduccini and Lierler 2017, 2013; Aziz, Chu, and Stuckey 2013; Cat et al. 2015; Susman and Lierler 2016; Eiter, Redl, and Sch uller 2016) to lazy grounding (Pal u et al. 2009; Lef evre and Nicolas 2009; Weinzierl 2017). These techniques obtained good preliminary results, but lazy grounding systems are still not competitive with ground&solve systems on common problems (Gebser et al. 2018). Recent research suggests that compilation-based techniques can mitigate the grounding bottleneck problem due to constraints (Cuteri et al. 2019, 2020). Essentially, their idea is to identify the subprograms causing the grounding bottleneck, and subsequently translate them to propagators, which are custom procedures that lazily simulate the ground&solve on the removed subprograms. Problematic constraints are removed from the non-ground input program and the corresponding propagator is dynamically linked to the solver to simulate their presence at running time. This approach is meant to speed-up computation by avoiding full grounding and exploiting information known at compilation time to create custom procedures that are specific to the program at hand. However, no compilation-based technique has been developed so far for ASP programs with aggregates (Faber, Pfeifer, and Leone 2011), which are among the most relevant and commonly-employed constructs of ASP (Gebser, Maratea, and Ricca 2017).

In this paper, we propose a compilation-based approach for ASP programs with aggregates. We identify the syntactic conditions under which a program with aggregates can be compiled, thus extending the definition of compilable subprogram of (Cuteri et al. 2019). Then, we implement the approach on top of the state-of-the-art ASP solver WASP (Alviano et al. 2015). Propagators are both of the eager (called during the propagation phase) and lazy (called once an answer set candidate is found) kind (Dodaro and Ricca 2020). Our compiler automatically selects the kind based on the program structure. Experiments show our approach is effective on ground-intensive ASP programs.

The Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI-22)

Preliminaries ASP Syntax. Variables are strings starting with uppercase letter and constants are non-negative integers or strings starting with lowercase letters. A term is either a variable or a constant. A standard atom is an expression of the form p(t1, . . . , tn), where p is a predicate of arity n and t1, . . . , tn are terms. A standard atom p(t1, . . . , tn) is ground if t1, . . . , tn are constants. A standard literal is an atom p or its negation p, where denotes negation as failure. A ground set is a set of pairs of the form consts : conj , where consts is a list of constants and conj is a conjunction of ground standard literals. A symbolic set is a set specified syntactically as {Vars : Conj}, where Vars is a non-empty list of variables, and Conj is a nonempty conjunction of standard literals. An aggregate function is of the form f(S), where S is a symbolic set, and f {#count, #sum} is an aggregate function symbol. An aggregate atom is of the form f(S) T, where f(S) is an aggregate function, {<, , >, , =} is a comparison operator, and T is a term called guard. An aggregate atom f(S) T is ground if T is a constant and S is a ground set. An atom is either a standard atom or an aggregate atom. A literal is an atom or its negation. The complement of l is denoted l, and it is a, if l = a, or a a if l = a. This notation is extended also to sets of literals. For a set of literals L, L+ and L denote the set of positive and negative literals appearing in L, resp. An ASP program π is a set of rules:

h b1, . . . , bk, bk+1, . . . , bm (1)

with m k 0, where h is a standard atom referred to as head and it can absent, whereas b1, . . . , bk, bk+1, . . . , bm is the body, b1, . . . , bk are atoms, and bk+1, . . . , bm are standard atoms. A constraint is a rule where h is absent, and a fact is a rule where m = 0. Moreover, for a rule r, Hr and Br are two sets containing the head and the body of a rule r, respectively, B+ r and B r are two sets containing the positive and the negative body of r, respectively, Ba r denotes the set of aggregate atoms appearing in Br, and Conj +(Ba r ) and Conj (Ba r ) denotes the set of positive and negative standard literals appearing in the aggregate atoms of the body, respectively. Given a program π, Uπ is the Herbrand Universe, and represents the set of all constants appearing in π; whereas Bπ is the Herbrand Base, and the set of all possible ground atoms that can be built using predicate in π and constants in Uπ. B denotes Bπ Bπ. Given an ASP expression (atom, literal, rule, program, etc.) ϵ and the Herbrand Universe Uπ, we define ground(ϵ) as the set of all instantiations of ϵ built by assigning variables to constant in Uπ.

ASP Semantics. An interpretation I B is a set of literals. A literal l is true w.r.t I if l I, l is false w.r.t. I if l I, otherwise it is undefined. In the following, for a program π, IU π denotes all literals in B that are undefined. For a rule, its body is a conjunction of literals. A conjunction conj of literals is true w.r.t I if all literals in conj are true w.r.t. I, and false if there is at least one literal in conj that is false w.r.t. I. Let I(S) denote the multiset [t1|(t1, . . . , tn) : conj S, ground(conj) is true w.r.t. I]. The evaluation I(f(S)) of an aggregate function f(S) w.r.t.

I is the result of the application of f on I(S). An interpretation I is total if all literals in B are either true or false, otherwise I is partial. An interpretation I is consistent if for each literal l I, l I, otherwise it is inconsistent. A total and consistent interpretation I is a model for π if for each rule r ground(π), the head of r is true whenever the body of r is true. Given a program π and an interpretation I, the FLP-reduct (Faber, Pfeifer, and Leone 2011) of π, denoted by πI, is defined as the set of rules obtained from π by deleting those rules whose body is false w.r.t I. Let I be a model for π, I is also a stable model for π if there is no I I such that I is a model for πI.

Classical CDCL Evaluation. The standard solving approach for ASP uses two components, namely grounder and solver. The grounder takes as input an ASP program π and produces ground(π), which is later on processed by the solver to produce stable models. The solver employes an algorithm that extends the CDCL algorithm with propagators specific to ASP (Kaufmann et al. 2016). The CDCL is based on a choose-propagate-learn pattern, and the idea is to build a stable model step-by-step starting from an empty interpretation I. At each step, a literal is heuristically selected and added to I (choice). Then, specific procedures, called (eager) propagators, are used to extend I with the deterministic consequences of this choice and their reason, i.e., literals in I leading to the propagation. In case the propagation leads to an inconsistency in the interpretation I, the algorithm learns a new constraint using the reason of each propagated literal, undoes the choices leading to the inconsistency, and restores the consistency of I. This process is repeated until I is a stable model candidate or the consistency of I cannot be restored, showing that no stable model can be found. In the first case I is then analyzed by lazy propagators, which perform additional checks on I. If I is consistent under those checks, then the algorithm terminates, otherwise new constraints are added to ground(π) and the algorithm restarts. We refer the reader to (Brewka, Eiter, and Truszczynski 2016) for a gentle overview of ASP.

Loop Unrolling and Dead Code Elimination. We recall two optimizations used by compilers, namely loop unrolling and dead code elimination (Muchnick 1997). Loop unrolling consists of removing loop control instructions by proper replicating the loop body in order to obtain an equivalent code. The following (exemple) portion of code clarifies this: for(i = 0, . . . , n) for(i = 0, . . . , n){ for(j = 0, . . . , 3) a[0] = b[0] + i; if(j < 2) a[j] = b[j] + i; = a[1] = b[1] + i; else b[j] = a[j] + i; b[2] = a[2] + i; } where the code on the left-hand side is transformed resulting in the code reported on the right-hand side. Note that for each iteration of the outermost statement one has to perform 3 n increments of the variable j and 3 n evaluations of the if statement, which are not required after loop unrolling. Clearly, the benefits of loop unrolling can be seen with large values of n. Dead code elimination consists of removing instructions that can never be executed, e.g., the body of statements that cannot be reached. We refer the reader to (Muchnick 1997) for more details.

Compilation of Aggregates Conditions for Splitting and Compiling Programs Given a program π, a sub-program of π is a set of rules λ π. In what follows, we denote with preds(X) the set of predicate names appearing in X where X is a structure (literal, conjunction, rule, program, etc). Moreover, given a set of rules λ, let head(λ) = {a | a Hr, r λ}. Definition 1 Given an ASP program π, the dependency graph of π, denoted DGπ, is a labeled graph (V, E) where V is the set of predicate names appearing in some head of π, and E contains (i) (v1, v2, +), if there is r π | v1 preds(B+ r ) preds(Conj +(Ba r )), v2 preds(Hr); (ii) (v1, v2, ), if there is r π | v1 preds(B r ) preds(Conj (Ba r )), v2 preds(Hr). Definition 2 Given an ASP program π, an ASP subprogram λ π is compilable w.r.t. π if (i) DGλ has no loop in it; (ii) for each p pred(head(λ)), p / pred(π \ λ); (iii) given two rules r1, r2 λ, r1 = r2, preds(Hr1) preds(Hr2) = ; and (iv) for each r λ, |Ba r | 1.

Normalization of the Input Program In the following we describe the main preprocessing steps that are performed to the sub-program to compile. First of all the sub-program λ is analyzed in order to be split in two subprograms, namely λlazy and λeager. This analysis consists of navigating the dependency graph starting from nodes that have no incoming edges and recursively label predicates that appears in the body of a rule whose head predicate has been already labeled. In this way, the rules whose head predicate has not been labeled could be treated in a lazy way (λlazy); other rules are in λeager. For λeager, we perform a rewriting to obtain a normalized form with rules of a specific format, and have a uniform treatment of all the rules to compile. Also, for a structure (set, list, conjunction, etc.) of elements X, let vs(X) be the set of all variables appearing in X.

Step 1. Each rule r λeager of the form (1), with |Ba r | = 1, f({Vars : Conj}) T Ba r , and {<, , >, }, is replaced by the following rules: 1. asr(Vars, ρ) Conj; 2. bdr(ρ, T) Br \ Ba r ; 3. aggr r(ρ, T) dmr(ρ, T), f({Vars : asr(Vars, ρ)}) G, where G = T if { , <}, and G = T + 1 if { , >}; 4. h bdr(ρ, T), aggr r(ρ, T) if {>, } and h bdr(ρ, T), aggr r(ρ, T) if {<, }; where ρ is vs(Conj) vs(Br \ Ba r ). Intuitively, ρ is a set of all variables appearing in both aggregate set and body. Example 1 Let assume r to be the following rule: a(X, W) b(X, Y ), c(Y, W), #sum{Z : d(X, Z), e(Z)} W. Then, r is replaced by the following rules: r1 : asr(Z, X) d(X, Z), e(Z) r2 : bdr(X, W) b(X, Y ), c(Y, W) r3 : aggr r(X, W) dmr(X, W), #sum{Z : asr(Z, X)} W r4 : a(X, W) bdr(X, W), aggr r(X, W)

Step 2. Each rule r λeager of the form (1), with |Ba r | = 1, f({Vars : Conj}) T Ba r , and {=}, is replaced by the rules 1., 2., and by the following rules: 5. aggr 1 r(ρ, T) dmr(ρ, T), f({Vars : asr(Vars, ρ)}) T; 6. aggr 2 r(ρ, T) dmr(ρ, T), f({Vars : asr(Vars, ρ)}) T + 1; 7. h bdr(ρ, T), aggr 1 r(ρ, T), aggr 2 r(ρ, T).

Step 3. Each rule r λeager of the form (1), with |Ba r | = 0, is replaced by the following rules: 8. h aux r(vs(B+ r )); 9. aux r(vs(B+ r )), bi i {1, . . . , m}; 10. Br, aux r(vs(B+ r )). This step is applied also to rules from steps 1 and 2. Example 2 Let assume r to be the following rule: a(Z, X) d(X, Z), e(Z). Then, r is replaced by the following rules: r8 : a(Z, X) aux r(X, Z) r 9 : aux r(X, Z), d(X, Z) r 9 : aux r(X, Z), e(Z) r10 : d(X, Z), e(Z), aux r(X, Z). Intuitively, the normalization ensures that aggregate functions are applied to set of atoms, and rules are subject to a form of completion (Clark 1977). After applying the normalization step the program contains only rules of the form: h b (2) h d, #count({V ars : b}) g (3) h d, #sum({V ars : b}) g (4) c1, ..., cn (5) Thus, the compiler will only have to produce propagators simulating the above-mentioned four rule types. Finally, it is important to emphasize that atoms of the form dmr( ) and aux r( ) do not appear in the head of any rule in the program, and thus the ASP semantics would make them false in all stable models. Therefore, in our approach, they are treated as external atoms (Gebser et al. 2016), whose instantiation and truth values are defined at running time in the propagator when the base Bλeager is determined.

Compilation In this section we present our strategy to compile a subprogram into a propagator focusing on the main compilation procedures for space reasons. In order to present our algorithms we followed the baseline and syntactic conventions described in (Cuteri et al. 2020) with some minor differences. In particular, the compiler transforms a logic program in the pseudo-code of the corresponding propagator. In this presentation the code enclosed between is printed by the compiler as it is, but the code enclosed in JK , is first substituted with its run-time value before being printed. For example, given a rule r of type (2) of the form a(X) b(X), Algorithm 2 at line 3 prints case a :. Given a compilable sub-program λ in input, λ is split in two subprograms, namely λlazy and λeager as explained in previous section. Then λlazy and λeager are compiled in different ways as described in the following.

Algorithm 1 Compile Program

Input : A normalized ASP program P Output: Prints propagator procedure of P propagating l

3 switch pred(l)

4 forall the r P do

5 if r is of type (2) then

6 Compile Rule(r)

7 else if r is of type (3) then

8 Compile Rule With Count(r)

9 else if r is of type (4) then

10 Compile Rule With Sum(r)

11 else if r is of type (5) then

12 forall the c Br do

13 Compile Constraint With Starter(r,c)

14 return Il

Algorithm 2 Compile Rule

Input : A rule r of type (2), i.e., h b Output: Prints propagator procedure for the rule r

2 σ = ϵ u =

3 case Jpred(h)K :

4 forall the i 1, ..., |trm(h)| do

5 if trm(h)[i] is variable then

6 σ = σ { Jtrm(h)[i]K 7 trm(l)[ Ji K ]}

7 T = {p I+| match(σ( Jb K ), p)}

8 U = {p (B \ I)+| match(σ( Jb K ), p)}

9 if |T| == 0 |U| == 1 l I+

10 u = p | p U

11 R = {l} {p I | match(σ( Jb K ), p)}

12 Il = Il (u, R)

13 else if |T| = 0 l I

14 forall p U

16 Il = Il (u, {l})

17 case Jpred(b)K :

18 forall the i 1, ..., |trm(b)| do

19 if trm(b)[i] is variable trm(b)[i] trm(h) then

20 σ = σ { Jtrm(b)[i]K 7 trm(l)[ Ji K ]}

21 T = {p I+| match(σ( Jb K ), p)}

22 U = {p (B \ I)+| match(σ( Jb K ), p)}

24 if σ( Jh K ) (B \ I)+

25 u = σ( Jh K )

26 Il = Il (u, {l})

28 if |T| = 0 |U| = 0 σ( Jh K ) (B \ I)+

29 R = {p I | match(σ( Jb K ), p)}

30 u = σ( Jh K )

31 Il = Il (u, R)

Eager Propagator. Given a compilable sub-program λeager, we first transform it in the normalized counterpart

P, as described in the previous section. Then, Algorithm 1 compiles P as an eager propagator. Recall that a propagator is called to compute the deterministic consequences of one literal at time, which is given by the solver (Cuteri et al. 2020). Thus, in the algorithms the variable l printed in output by the compiler is used to store the literal to propagate in the propagator pseudo-code. Roughly, the propagator matches ground literals to first order literals in the rules of λeager (as in the grounding) and tries to temporarily build the substitution that instantiates that rule, thus it determines where some propagation occurs. In case of inconsistency a reason is computed and passed to the solver for enabling learning (Cuteri et al. 2020). In this process loop unrolling and dead code elimination is performed using the syntactic information on the rule structure. More formally, The algorithm 1 first prints the declaration of an empty implication list, namely Il, where the propagator stores all the propagations caused by the fact that a literal to progagate l is added to the interpretation I. Afterward, according to the predicate name of l, the propagator evaluates the propagations depending on the kind of the rule in which the predicate appears. We concentrate on rules of type (2) and (4), since (3) is analogous to (4), and (5) is the same as in (Cuteri et al. 2020) (full details and examples in supplementary material). In turn, Algorithm 2 prints two different switch cases for checking if l appears in h (line 3) or in b (line 17). In both cases the algorithm also prints the code for substituting variables that are in the head of the rule (lines 4-6 and 18-20, respectively). Moreover, true and undefined atoms matching σ(b) (lines 7-8 and 21-22, respectively) are stored in two sets, namely T and U. Note that σ is a variable substitution that replaces variables occurrences with constants that are mapped to, e.g., consider l = a(X), if σ(X) = 1 then σ(l) = a(1). Then, the algorithm prints the code specific for the case when l appears in h. In particular, if l is positive then h is true w.r.t. I and the propagator has to find a body that can support it (lines 9-12). Otherwise, if l is negative, then h is false w.r.t. I, then the propagator has to set as false all possible body instantiations (lines 13-16). Instead, if the predicate of l appears in b and l is positive, then the body of the rule is true w.r.t. I and then the propagator has to set h as true (lines 24-26). Otherwise, if l is negative and all other body instantiations are false w.r.t. I, then h is derived as false (lines 28-31). For rules of type (4), i.e., rules of the form h d, #sum({V : b}) g, Algorithm 3 prints the propagator code. In particular, it prints two different switch cases for checking if the predicate of l appears in the head of the rule (line 3) or in the aggregate atom (line 20). In both cases the propagator needs to build a variable substitution σ to simulate the rule instantiation. This substitution maps the variables occurring in h with the constants in l (lines 4-7 and 21-24). If the predicate of l appears in h, the propagator first collects true (line 8) and undefined (line 9) atoms w.r.t. I matching σ(b) in T and U, respectively. Next, the propagator computes actual and possible sums as the sum of the weights associated with literal in T and U, respectively (line 10). Then, the propagator has to distinguish two cases. If l is positive (line 11), thus h is true w.r.t. I, then the aggregate must be true in order to support h. This can be

done by checking that the maximal possible sum is always greater than or equal to g. Therefore, if there is a literal, say p, whose falsity would make the maximal possible sum less than g (line 14), then p is derived as true (line 15). Otherwise, if l is negative (line 16), thus h is false w.r.t. I, then the aggregate must be false, i.e., the propagator ensures that the actual sum does not exceed g. Therefore, if there is a literal, say p, whose truth would make the actual sum greater than or equal to g (line 18), then p is derived as false (line 19). If the predicate of l appears in the aggregate, then the code of the propagator is as follows. First, the propagator collects in T (respectively, F) all possible positive (respectively, negative) true w.r.t. I literals matching the variable substitution on the head, and in U all undefined atoms matching the variable substitution on the head (lines 25-27). For each literal, say hl T F U, the propagator considers three different types of propagations. In particular, if hl T or hl F, then the propagator performs similar operations as in lines 8-19 (lines 33-44). Instead, if hl U, then the propagator considers two cases. If the actual sum is greater than or equal to the guard (line 46), therefore the body of the rule is true, and thus the head is derived as true (line 47). If the maximal possible sum is less than the guard (line 48) then the head is derived as false (line 49). Note that the propagator stores in Il also the literals causing the propagation of a literal, i.e., the so-called reason (e.g., line 12 of Algorithm 3). In case of inconsistency, the solver retrieves from Il the reason for propagation used later on for learning.

Lazy Propagator. Lazy propagator instantiates the body of rules by using literals in the model I, and extends I with the heads obtained from such body instantiations. In particular, for each rule r λlazy, the propagator calls Algorithm 4 with r as parameter. The algorithm first reorders the body of r in such a way that the positive body is evaluated before the negative one (line 3). Subsequently, the algorithm calls Algorithm 5 with the reordered body (B), the rule r, and the index 0 as parameters. Then, for each positive literal b in B, Algorithm 5 prints the code to iterate over positive and true w.r.t. I literals that match σ(b) (lines 5-9). For each negative literal n in B, Algorithm 5 prints the code to check if σ(n) is negative and true w.r.t. I (lines 29-30). For each aggregate literal, instead, the algorithm recursively calls itself with the list of literals inside the aggregate, the rule r, and the index j of the aggregate as parameters (line 15). In this way, the algorithm prints nested join loops and if statements that evaluate the aggregate conjunction. After that, the algorithm prints the code that computes the sum of the weights (or count) of the elements in the aggregate set (lines 16-21). Once nested join loops and if statements for the aggregate conjunction are closed, the algorithm prints the code that either checks if the aggregate relation is verified or maps the aggregate guard to the aggregate value. Then, the code returns to the end of Algorithm 4, which prints the code that adds σ(Hr) to the model I (line 6), since nested join loops and if statements for each body literal are printed.

Experiments

In the experiments we considered three different settings.

Algorithm 3 Compile Rule With Sum

Input : A rule r of type (4), h d, #sum({V : b}) g Output: Prints propagator code starting for rule r

2 k = i s.t. trm(b)[i] = V [0], i {1, ..., |trm(b)|}

3 case Jpred(h)K

5 forall the i 1, ..., |trm(h)| do

6 if trm(h)[i] is variable then

7 σ = σ { Jtrm(h)[i]K 7 trm(l)[ Ji K ]}

8 T = {p I+| match(σ( Jb K ), p)}

9 U = {p (B \ I)+| match(σ( Jb K ), p)}

10 act, pos = get Sum(T, U, Jk K )

12 R = {l} {p I | match(σ( Jb K ), p)}

13 forall p U

14 if act + pos trm(p)[ Jk K ] < σ( Jg K )

15 Il = Il (p, R)

17 forall p U

18 if act + trm(p)[ Jk K ] σ( Jg K )

19 Il = Il (p, {l} T)

20 case Jpred(b)K

22 forall the i 1, ..., |trm(b)| do

23 if trm(b)[i] is variable trm(b)[i] trm(h) then

24 σ = σ { Jtrm(b)[i]K 7 trm(l)[ Ji K ]}

25 T = {p I+| match(σ( Jh K ), p)}

26 F = {p I | match(σ( Jh K ), p)}

27 U = {p (B \ I)+| match(σ( Jh K ), p)}

28 forall hl T U F

30 forall the i 1, ..., |trm(h)| do

31 if trm(h)[i] is variable then

32 σh = σh { Jtrm(h)[i]K 7 trm(hl)[ Ji K ]}

33 UB = {p (B\I)+| match(σh( Jb K ), h)}

34 FB = {p I | match(σh( Jb K ), p)}

35 TB = {p I+| match(σh( Jb K ), p)}

36 act, pos = get Sum(TB, UB, Jk K )

38 forall p UB

39 if act + pos trm(p)[ Jk K ] < σh( Jg K )

40 Il = Il (p, {hl} FB)

41 else if hl F

42 forall p UB

43 if act + trm(p)[ Jk K ] σh( Jg K )

44 Il = Il (p, {hl} TB)

46 if act σh( Jg K )

47 Il = Il (hl, TB)

48 else if act + pos < σh( Jg K )

49 Il = Il (hl, FB)

Setting (i). A simple benchmark that we use as a motivating example to show the limits of ground&solve:

Algorithm 4 Compile Lazy Rule

Input : A rule r Output: Prints lazy propagator code for a program P

2 h = Hr // head of r

3 B = body Ordering(Br)

5 Print Nested Join(B, r, 0)

6 I = I {σ(h)}

7 forall the i 1, ..., |B| do 8 σ = σ Ji,0K

Algorithm 5 Print Nested Join

Input : A list of literals B, a rule r, an index i Output: Prints nested join to instantiate B

2 forall the j 1, ..., |B| do 3 σ Jj,i K = σ

4 if B[j] is a positive literal then

5 T Jj,i K = {p I+| match(σ( JB[j]K ), p)}

6 for all t Jj,i K T Jj,i K

7 forall the k 1, ..., |trm(B[i])| do

8 if trm(B[j, i])[k] is variable then

9 σ = σ { Jtrm(B[j])[k]K 7 trm(t Jj,i K )[ Jk K ]}

10 else if B[j] is an aggregate literal then

11 Ba = body Ordering(conj(Ba r ))

12 V = vars(Ba r )

15 Print Nested Join(Ba, r, j)

16 if σ( JV K ) / a s

17 a s = a s σ( JV K )

18 if B[j] is sum aggregate then

19 a v+ = σ( JV [0]K )

21 a v+ = 1

22 for k 1, ..., |conj(Ba)| do 23 σ = σ Jk,j K

24 if B[j] is bound relation then

25 if a v σ( Jguard(Ba r )K )

27 σ = σ { Jguard(Ba r )K 7 a v}

29 t Jj,i K = σ( JB[j]K )

30 if t Jj,i K I

r1 : d(1..k) r2 : {a(X) : d(X); b(Y ) : d(Y )} r3 : #count{X : a(X)} > Y, b(Y ).

r1 is a shortcut for k facts of the form d(i) (i = 1, . . . , k); and r2 contains a choice rule (Calimeri et al. 2020);

Setting (ii). All benchmarks from ASP competitions (Calimeri et al. 2016) including at least one rule with aggregates that can be compiled under our conditions. This setting is useful to analyze the performance of our compilation-based technique on benchmarks that do not present a grounding bottleneck problem. The selected benchmarks are the following: Abstract Dialectical Framework, Bottle Filling Problem, Connected Maximum Density-Still Life, Crossing Minimization, Incremental Scheduling, Partner Units, Solitaire, Weighted Sequence Problem;

Setting (iii). Three grounding-intensive benchmarks taken from the literature, in particular Component Assignment Problem proposed by Alviano, Dodaro, and Maratea (2018), Dynamic In-Degree Counting and Exponential-Save proposed by Bomanson, Janhunen, and Weinzierl (2019).

Hardware and Software. In all the experiments, the compilation-based approach, reported as WASP-COMP, has been compared with the plain version of WASP (Alviano et al. 2015) v. 169e40d and with the state-of-the-art system CLINGO v. 5.4.0 (Gebser et al. 2016). All the tested systems use GRINGO (included in the binary of CLINGO) as grounder. Moreover, for the benchmarks Dynamic In-Degree Counting and Exponential-Save we considered also the system ALPHA (Weinzierl 2017), which is based on lazy-grounding techniques. ALPHA cannot be used for other experiments since it does not support some of the language constructs used in the benchmarks (e.g., choice rules with bounds). For each benchmark, we selected the rules to be compiled by looking at the potential grounding issues. Experiments were executed on Xeon(R) Gold 5118 CPUs running Ubuntu Linux (kernel 5.4.0-77-generic), time and memory are limited to 2100 seconds and 4GB, respectively.

Results. Results of experiments in the setting (i) and setting (ii) are reported in Table 1 and Table 2, respectively. In the tables we report for each solver the number of solved instances (sol.), the sum of running times (sum t) in seconds, and the average used memory (avg mem) in MB. Moreover, concerning WASP-COMP, Table 2 reports an additional col-

k WASP-COMP WASP CLINGO t mem t mem t mem 1000 0 0 1.02 59.6 0.66 40.2 2000 0.1 18.6 4.36 286.5 3.23 303.5 3000 0.24 38.5 9.98 696.3 7.68 709.5 4000 0.53 53.7 18.47 1168.1 13.62 1216.8 5000 0.93 74.6 28.8 2215.4 22.23 1933.3 6000 1.19 109.8 42.47 2807.2 32.73 2871.1 7000 1.44 142.3 58.31 3402 42.88 3576.7 8000 1.96 152 - - - - 9000 2.89 191.6 - - - - 10000 3.87 254.7 - - - - 20000 12.52 898.5 - - - - 30000 26.43 1888.3 - - - - 40000 58.88 3319.6 - - - - 50000 - - - - - -

Table 1: Comparison with WASP and CLINGO on setting (i).

Benchmark # WASP-COMP WASP CLINGO sol. sum t avg mem comp. t sol. sum t avg mem sol. sum t avg mem Abs. Dia. Fram. 200 117 23467.7 118.9 6.47 123 24311.1 117.2 200 1244.6 26.4 Bottle Filling 100 100 2208.3 773.8 11.98 100 545.8 761.8 100 394.0 213.4 Con. Max. Den. 26 6 2166.8 26.4 31.8 6 427.5 31.4 4 85.4 11.1 Crossing Min. 85 84 305.3 16.4 8.97 84 257.3 14.5 51 10013.0 20.4 Incr. Sched. 500 329 25960.7 96.6 6.94 317 42282.4 210.9 345 18952.8 253.7 Partner Units 112 52 35525.7 160.9 12.51 69 29612.5 247.6 80 7147.8 73.8 Solitaire 27 25 601.7 27.0 12.03 25 140.2 18.4 25 273.1 9.8 Weighted Seq. 65 65 6663.4 36.1 8.46 65 4713.5 32.3 65 569.6 14.5 Comp. Assign. 302 188 56137.2 814.4 20.79 70 15325.81 973.3 118 36832.0 1288.6 Dyn. Ind. Cou. 80 80 48.0 62.0 6.48 80 1374.6 619.4 80 1282.1 551.8 Exp.-Save 27 21 2594.1 527.0 * 6 18.5 369.8 7 24.4 365.4

Table 2: Comparison of the compilation-based approach with WASP and CLINGO on instances of settings (ii) and (iii).

umn (comp. t), representing the compile time in seconds. The latter is not included in the sum of the time, since the compilation is done only once for each benchmark (with the exception of Exponential-Save) and, thus, can be done offline. Concerning the setting (i), we observe that CLINGO and WASP cannot solve instances with k = 8000, whereas WASP-COMP can efficiently handle instances up to values of k = 40000. Concerning the setting (ii), we observe that CLINGO obtains the best performance overall, and it is faster than WASP and WASP-COMP on the non-ground-intensive benchmarks (above the double line in Table 2). The impact of the proposed technique can be seen by comparing WASPCOMP and WASP. In this case, we observe that the former is competitive with the latter in all the benchmarks but Abstract Dialectical Framework and Partner Units, where WASP solves 6 and 17 more instances than WASP-COMP. Nonetheless, WASP-COMP performs better than WASP on the benchmark Incremental Scheduling, solving 12 more instances, where the lazy propagator gives a clear advantage. Interestingly, on this benchmark, WASP-COMP also uses less memory than WASP and CLINGO. Indeed, if only 512 MB are available (as reasonable in some case) WASP-COMP solves 57 and 53 instances more than WASP and CLINGO, respectively. Concerning the setting (iii), WASP-COMP outperforms WASP in all the tested benchmarks solving 133 more instances overall. It is important to observe that each instance of Exponential-Save requires to be compiled, since aggregates to be compiled are part of the instances. Therefore, in this benchmark, the solving time includes also the compilation time. Concerning Dynamic In-Degree Counting, WASP-COMP and WASP solve the same number of instances, but WASP-COMP is much faster. Moreover, we observe that WASP-COMP solves 84 more instances than CLINGO overall. Finally, we observe that WASP-COMP is competitive also with ALPHA, since the latter solves 80 instances of Dynamic In-Degree Counting in 492.0 seconds using 649.1 MB, and 27 instances of Exponential-Save in 332.9s using 227.8 MB.

Related Work

The grounding bottleneck is widely recognized as one of the major drawbacks of state-of-the-art ASP systems (Cuteri et al. 2020; Bomanson, Janhunen, and Weinzierl 2019).

Different alternative approaches have been proposed to overcome it, from extensions of the ASP language, as Constraints Answer Set Programming (CASP) (Ostrowski and Schaub 2012; Balduccini and Lierler 2017, 2013; Aziz, Chu, and Stuckey 2013; Cat et al. 2015; Susman and Lierler 2016), and HEX programs (Eiter, Redl, and Sch uller 2016), to lazy grounding (Lef evre and Nicolas 2009; Pal u et al. 2009). Lazy grounding systems perform grounding of the rules during the stable model search, where a rule is instantiated only when its body is satisfied; in this way the grounding is done only for rules used during the search. The stateof-the-art lazy-grounding system ALPHA (Weinzierl 2017) also includes many techniques implemented in traditional ASP systems, such as learning, conflict-based heuristics, restarts, and so on. Bomanson, Janhunen, and Weinzierl (2019) implemented on top of ALPHA a techniques for lazily rewriting aggregates as rules. This latter compared with our approach shows similar performance on the groundingintensive benchmarks supported by both systems. ALPHA differs from our approach since it avoids the grounding the entire program, where we compile as a propagator a subprogram, and automatically integrate it into the solving component of a CDCL-based solver. Note that our approach builds on optimized systems, whereas ALPHA requires to reimplement all existing techniques. Moreover, we mention a recent work (Lierler and Robbins 2021) that is based on the same principles of (Cuteri et al. 2020), where the grounding of some rules is done using a lazy propagator. However, (Lierler and Robbins 2021) does not yet include aggregates.

The grounding bottleneck is a limiting factor for ASP systems based on the ground&solve architecture. Compilationbased approaches proposed by Cuteri et al. (2020) offer the possibility to mitigate this issue in presence of constraints while keeping the benefits of state-of-the-art approaches. In this paper we extend the compilation-based approaches to handle aggregates, a relevant construct of ASP. Experiments confirm that our approach outperforms state-of-the-art systems on several ground-intensive programs with aggregates. Finally, we mention that benchmarks and executables are publicly-available (Dodaro, Mazzotta, and Ricca 2021a,b).

Acknowledgments This work was partially supported by the Italian Ministry of Industrial Development (MISE) under project MAP4ID Multipurpose Analytics Platform 4 Industrial Data , N. F/190138/01-03/X44. During the submission phase the order s name of the authors was not alphabetical in the submission system and it was not possible to fix it before the final submission. The order does not reflect the contribution of the authors to the paper. All authors have contributed equally.

References Alviano, M.; Dodaro, C.; Leone, N.; and Ricca, F. 2015. Advances in WASP. In LPNMR, volume 9345 of Lecture Notes in Computer Science, 40 54. Springer. Alviano, M.; Dodaro, C.; and Maratea, M. 2018. Shared aggregate sets in answer set programming. TPLP, 18(3-4): 301 318. Aziz, R. A.; Chu, G.; and Stuckey, P. J. 2013. Stable model semantics for founded bounds. TPLP, 13(4-5): 517 532. Balduccini, M.; and Lierler, Y. 2013. Integration Schemas for Constraint Answer Set Programming: a Case Study. TPLP, 13(4-5-Online-Supplement). Balduccini, M.; and Lierler, Y. 2017. Constraint answer set solver EZCSP and why integration schemas matter. TPLP, 17(4): 462 515. Bomanson, J.; Janhunen, T.; and Weinzierl, A. 2019. Enhancing Lazy Grounding with Lazy Normalization in Answer-Set Programming. In AAAI, 2694 2702. AAAI Press. Brewka, G.; Eiter, T.; and Truszczynski, M. 2011. Answer set programming at a glance. Commun. ACM, 54(12): 92 103. Brewka, G.; Eiter, T.; and Truszczynski, M. 2016. Answer Set Programming: An Introduction to the Special Issue. AI Mag., 37(3): 5 6. Calimeri, F.; Faber, W.; Gebser, M.; Ianni, G.; Kaminski, R.; Krennwallner, T.; Leone, N.; Maratea, M.; Ricca, F.; and Schaub, T. 2020. ASP-Core-2 Input Language Format. TPLP, 20(2): 294 309. Calimeri, F.; Gebser, M.; Maratea, M.; and Ricca, F. 2016. Design and results of the Fifth Answer Set Programming Competition. Artif. Intell., 231: 151 181. Cat, B. D.; Denecker, M.; Bruynooghe, M.; and Stuckey, P. J. 2015. Lazy Model Expansion: Interleaving Grounding with Search. J. Artif. Intell. Res., 52: 235 286. Clark, K. L. 1977. Negation as Failure. In Logic and Data Bases, Advances in Data Base Theory, 293 322. New York: Plemum Press. Cuteri, B.; Dodaro, C.; Ricca, F.; and Sch uller, P. 2019. Partial Compilation of ASP Programs. TPLP, 19(5-6): 857 873. Cuteri, B.; Dodaro, C.; Ricca, F.; and Sch uller, P. 2020. Overcoming the Grounding Bottleneck Due to Constraints in ASP Solving: Constraints Become Propagators. In IJCAI, 1688 1694. ijcai.org.

Dodaro, C.; Mazzotta, G.; and Ricca, F. 2021a. Benchmarks. https://doi.org/10.5281/zenodo.5752555. Accessed: 202203-25. Dodaro, C.; Mazzotta, G.; and Ricca, F. 2021b. Executables. https://www.mat.unical.it/ dodaro/research/ compilation/. Accessed: 2022-03-25. Dodaro, C.; and Ricca, F. 2020. The External Interface for Extending WASP. TPLP, 20(2): 225 248. Eiter, T.; Redl, C.; and Sch uller, P. 2016. Problem Solving Using the HEX Family. In Computational Models of Rationality, 150 174. College Publications. Erdem, E.; and Oztok, U. 2015. Generating explanations for biomedical queries. TPLP, 15(1): 35 78. Faber, W.; Pfeifer, G.; and Leone, N. 2011. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell., 175(1): 278 298. Gebser, M.; Kaminski, R.; Kaufmann, B.; Ostrowski, M.; Schaub, T.; and Wanko, P. 2016. Theory Solving Made Easy with Clingo 5. In ICLP (Technical Communications), volume 52 of OASICS, 2:1 2:15. Schloss Dagstuhl - Leibniz Zentrum f ur Informatik. Gebser, M.; Leone, N.; Maratea, M.; Perri, S.; Ricca, F.; and Schaub, T. 2018. Evaluation Techniques and Systems for Answer Set Programming: a Survey. In IJCAI, 5450 5456. ijcai.org. Gebser, M.; Maratea, M.; and Ricca, F. 2017. The Sixth Answer Set Programming Competition. J. Artif. Intell. Res., 60: 41 95. Gelfond, M.; and Lifschitz, V. 1991. Classical Negation in Logic Programs and Disjunctive Databases. New Gener. Comput., 9(3/4): 365 386. Kaufmann, B.; Leone, N.; Perri, S.; and Schaub, T. 2016. Grounding and Solving in Answer Set Programming. AI Mag., 37(3): 25 32. Lef evre, C.; and Nicolas, P. 2009. The First Version of a New ASP Solver : ASPe Ri X. In LPNMR, volume 5753 of Lecture Notes in Computer Science, 522 527. Springer. Lierler, Y.; and Robbins, J. 2021. Dual Grounder: Lazy Instantiation via Clingo Multi-shot Framework. In JELIA, volume 12678 of Lecture Notes in Computer Science, 435 441. Springer. Muchnick, S. S. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann. Ostrowski, M.; and Schaub, T. 2012. ASP modulo CSP: The clingcon system. TPLP, 12(4-5): 485 503. Pal u, A. D.; Dovier, A.; Pontelli, E.; and Rossi, G. 2009. GASP: Answer Set Programming with Lazy Grounding. Fundam. Informaticae, 96(3): 297 322. Susman, B.; and Lierler, Y. 2016. SMT-Based Constraint Answer Set Solver EZSMT (System Description). In ICLP (Technical Communications), volume 52 of OASICS, 1:1 1:15. Schloss Dagstuhl - Leibniz-Zentrum f ur Informatik. Weinzierl, A. 2017. Blending Lazy-Grounding and CDNL Search for Answer-Set Solving. In LPNMR, volume 10377 of Lecture Notes in Computer Science, 191 204. Springer.