Compilation of Aggregates in ASP: ? Preliminary Results Giuseppe Mazzotta, Bernardo Cuteri, Carmine Dodaro, and Francesco Ricca University of Calabria, Italy Abstract. Answer Set Programming (ASP) is a well-known problem- solving formalism in computational logic. Among the knowledge mod- eling constructs that make ASP eective in representing complex prob- lems are aggregates. Aggregates operate on sets of literals and compute a single value (e.g., count, sum, etc.), thus, making the expression of con- straints in ASP programs very concise. Traditionally, ASP systems are based on the ground&solve approach that suers an intrinsic limitation known as grounding bottleneck: the grounding (variable elimination) can ll all the available memory and then the program cannot be evaluated. This happens also in programs that use aggregate functions. Recently, an alternative approach to evaluate ASP programs that avoids the ground- ing bottleneck has been proposed that is based on ASP program compila- tion. In this paper we present an extension of ASP program compilation that supports constraints containing the aggregate count. Preliminary experimental results demonstrate the viability of the approach. Keywords: Answer Set Programming · Aggregates · Grounding Bottle- neck. 1 Introduction Answer Set Programming (ASP) [7] is a well-known problem-solving formalism in computational logic that is based on the stable model semantics [24]. ASP systems, such as clingo [20] and dlv [1, 3], made possible the development of many real-world applications. In the recent years, ASP has been widely used for solving problems of game theory [5], natural language processing [28], natural language understanding [13], robotics [18], scheduling [16], and more [17]. A key role in the development of applications is played by system perfor- mance, and thus, the improvement of ASP systems is an interesting research topic in computational logic. Traditional ASP systems are based on the ground & solve approach [25], in which a grounder module transforms the input program (containing variables) in its propositional counterpart, whose stable models are subsequently computed by the solver module, which implements an extension of the Conict Driven Clause Learning (CDCL) algorithm [25]. The traditional ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 2 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca ASP implementations are eective in many contexts [17] but suer from an intrinsic limitation: the combinatorial blowup of the grounding of some rules, known as grounding bottleneck. The grounding bottleneck is often due to one or few constraints that model the (non) admissibility of problem solutions [27, 9]. Several attempts have been made to solve the grounding bottleneck prob- lem [22], including language extensions (such as constraint programming [27, 6], and dierence logic [20, 29]) and lazy grounding techniques [14, 26, 30]. Hybrid formalisms are eciently evaluated by coupling an ASP system with a solver for the other theory, thus circumventing the grounding bottleneck. Lazy grounding implementations instantiate a rule only when its body is satised to prevent the grounding of rules which are unnecessary during the search of an answer set. Albeit lazy grounding techniques obtained good preliminary results, their performance is still not competitive with state-of-the-art systems [22]. Recently a dierent approach was proposed that is based on the compilation of problematic constraints as propagators [10, 11]. In this latter approach, prob- lematic constraints are removed from the non-ground input program and the resulting program is provided as input to an extended version of a CDCL-based solver, where the presence of problematic constraints is internally simulated. There are two alternative strategies for implementing such an extension, namely lazy instantiation and propagators. In the lazy instantiation strategy, the solver computes a stable model of the program without problematic constraints. If this stable model satises also the omitted constraints, then it is also a stable model of the original program. Otherwise, the violated instances of these constraints are lazily instantiated, and the search continues. The other strategy relies on an extension of the propagation function by adding custom propagators, whose role is to perform the inferences of missing constraints during the search. Basically, Cuteri et al. [11] proposed to translate (or compile) some non-ground constraints into a dedicated C++ procedure, which is used by the system to generate prop- agators in an automatic way. This approach keeps the declarativity of ASP and is eective when the problematic constraints are likely to be satised by a can- didate model (i.e., whenever lazy instantiation is eective cfr. [10]). Approaches based on compilation revealed to be very promising, outperforming traditional systems in many comparisons [11, 12] However, a signicant number of prob- lems, especially hard combinatorial problems from ASP competitions [9] exploit an advanced language feature that is not supported: aggregates [19]. Aggregates are among the standardized knowledge modeling constructs that make ASP ef- fective in representing complex problems [8, 23]. Indeed, aggregates operate on sets of literals and compute a single value (e.g., count, sum, etc.), thus, making the expression of constraints in ASP programs very concise. In this paper, we push forward the idea of [1012], and we present a novel strategy for translating (compiling) non-ground constraints containing #count aggregates into dedicated C++ procedures that are used as propagators during the search of the CDCL algorithm. We have implemented our extension on top of wasp [4, 2, 15] and conducted an experimental analysis on hard benchmarks from Compilation of Aggregates in ASP: Preliminary Results 3 ASP competitions [9, 23]. Results are encouraging, indeed our implementation improves the performance of wasp in all tested scenarios. 2 Preliminaries 2.1 Answer Set Programming An ASP program π is a set of rules of the form: h1 | . . . |hn : −b1 , . . . , bm . with n + m > 0 where h1 | . . . |hn is a disjunction of atoms and is referred to as head, instead, b1 , . . . , bm is a conjunction of literals and is referred to as body. In particular, if n = 0 the rule is called constraint, instead if m = 0 the rule is called fact. An atom a is an expression of the form p(t1 , . . . , tk ) where p is a predicate of arity k and t1 , . . . , tk are terms. A term is an alphanumeric string that could be either a variable or a constant. According to Prolog, if a term starts with a capital letter is a variable otherwise is constant. If ∀i ∈ {1, . . . , k}, ti is a con- stant the atom a is said ground. A literal is an atom a or its negation ∼ a where ∼ denotes the negation as failure. Given a literal l it is said positive if l = a, negative if l =∼ a. Given a positive literal l = a, we dene the complement, l =∼ a, instead, for a negative literal l =∼ a, l = ∼ a = a. However ASP supports also aggregate atoms. An aggregate atom is of the form f (S)  T , where f (S) is an aggregate function, ∈ {=, <, ≤, >, ≥} is a predened com- parison operator, and T is a term referred to as guard. An aggregate function is of the form f (S), where S is a set term and f ∈ {#count, #sum} is an ag- gregate function symbol. A set term S is a pair that is either a symbolic set or a ground set. A symbolic set is a pair {T erms : Conj}, where Terms is a list of variables and Conj is a conjunction of standard atoms, that is, Conj is of the form a1 , . . . , an and each ai (1 ≤ i ≤ n) is an atom. A ground set, instead, is a set of pairs of the form (t : conj), where t is a list of constants and conj is a conjunction of ground atoms. Given a program π , we dene Uπ , the Her- brand Universe, as the set of all constants appearing in π and Bπ , the Herbrand Base, as the set of all possible ground atoms that can be built using predicate in π and constants in Uπ . B denotes Bπ ∪ Bπ . Given a rule r and the Herbrand Universe Uπ , we dene ground(r) as the set of all possible instantiations of r that can be built assigning S variables in r to constant in Uπ . Given a program π , instead, ground(π) = r∈π ground(r). An interpretation I is a set of literals. In particular, I is total if ∀a ∈ Bπ (a ∈ I∨ ∼ a ∈ I) ∧ (a ∈ I →∼ a ∈/ I). A literal l is true w.r.t I if l ∈ I , otherwise it is false. A ground conjunction conj of atoms is true w.r.t I if all atoms in conj are true, otherwise, if at least one atom is false then conj is false w.r.t. I . Let I(S) denote the multi- set [t1 |(t1 , . . . , tn ) : conj ∈ S ∧ 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). For example let A be an aggregate atom A = #count{(1 : p(1, 1)), (2 : p(2, 1)), (3 : 4 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca p(3, 1))} > 1 and let I = {p(1, 1), p(2, 1), ∼ p(3, 1)}. I(S) = [1, 2], I(f (S)) = 2 since f = #count so the aggregate atom A is true w.r.t. I . I is a model for π if ∀ r ∈ ground(π)(∀ l ∈ body(r), l ∈ I) → (∃a ∈ head(r) : a ∈ I). Given a program π and an interpretation I , we dene the F LP − reduct of π , denoted by π I , as the set of rules obtained from π deleting those rules that has body0 false w.r.t I . Let I be a model for π , I is also a stable model for π if 6 ∃ I ⊂ I such that I is a model for π I . Given a program π , π is coherent if it 0 admits at least one stable model otherwise is incoherent. 2.2 Classical CDCL Evaluation The solving approach for ASP is implemented as conict-driven clause learning for SAT but with ad-hoc extensions for ASP that ensure that the model built is also stable. In particular, the idea behind this approach starts from an empty interpretation I and step-by-step will add to I all the deterministic consequences starting from true literals in I . Once all consequences are inferred if the inter- pretation is not total we will choose heuristically some literals and propagate their deterministic consequences. If we reach the empty clause we come back (conict resolution ) to the last non-deterministic choice and will propagate it deterministically and go forward until I is total and then we have a model or we have no choice and then the program is incoherent. To better understand, let suppose we have the following ground program π : r0 : a(1). r1 : a(2). r2 : a(3)|a(4). r3 : b(1, 1)|nB(1, 1). r4 : b(1, 2)|nB(1, 2). r5 : b(2, 2)|nB(2, 2). r6 : b(2, 1)|nB(2, 1). r7 : : −a(1), #count{1 : b(1, 1), 2 : b(1, 2)} > 1 r8 : : −a(2), #count{1 : b(2, 2), 2 : b(2, 1)} > 1 r9 : : −b(1, 1), b(2, 1), a(3). The algorithm starts with I = ∅. Then a(2) is inferred from r1 , and a(1) is inferred from r0 . Let suppose that from r3 is heuristically chosen b(1, 1). Let consider its deterministic consequences:  From r3 is inferred ∼ nB(1, 1) since, by property of stable models, this is the only way to support b(1, 1)  From r7 is inferred ∼ b(1, 2) since it is the unique way to satisfy r7  From r4 is inferred nB(1, 2) because it is the unique way to satisfy r4 since ∼ b(1, 2) has been previously added to I At this point let suppose that heuristically is chosen b(2, 1). As consequences we have:  From r6 is inferred ∼ nB(2, 1) to ensure that the model will be also a stable model Compilation of Aggregates in ASP: Preliminary Results 5  From r8 is inferred ∼ b(2, 2) since it is the unique way to satisfy r8  From r5 is inferred nB(2, 2) because it is the unique way to satisfy r5 since b(2, 2) has been previously added to I Let suppose that from r2 is chosen a(3). At this point, the algorithm propagates ∼ a(4) and nd a conict in r9 . Since a conict is detected last deterministic consequences are unfolded until the last choice and propagate ∼ a(3) and its consequences, in this case only a(4) from r3 . Now, I is total so we have found a stable model. Thanks to the external interface of WASP, we can customize the CDCL evaluation by dening propagators, which are procedures intended to compute the deterministic consequences of a true literal. In particular, in our approach, we take as input an ASP constraint, possibly containing an aggregate, and create a propagator that computes the deterministic consequences of a true literal w.r.t. the ASP constraint in input. 2.3 Normalization Procedure In order to simplify the compilation of constraint containing an aggregate literal we normalize the aggregate literals, without losing generality, in such a way that the dierent comparison operators are unied to one of them that is ≥ operator. Let C be a constraint with an aggregate A of the form count(S)  g with ∈ {<, ≤, >, ≥, =}, the normalization procedure is the following:  If  equal to ≥ then A remains as it is;  If  equal to > then A will be mapped into #count(S) ≥ g + 1;  If  equal to < then A will be mapped into ∼ #count(S) ≥ g ;  If  equal to ≤ then A will be mapped into ∼ #count(S) ≥ g + 1;  If  equal to = then A will be mapped into the conjunction of two aggregate literals: • A1 = #count(S) ≥ g ; • A2 =∼ #count(S) ≥ g + 1.  If  equal to = and A is negated then C will be mapped in two dierent constraints as follow: • C1 =: −body(C), #count(S) ≥ g + 1; • C2 =: −body(C), ∼ #count(S) ≥ g . For example given constraint C =: −#count{X : a(X)} = 3, it will be normal- ized as follow: 0 C =: −#count{X : a(X)} ≥ 3, ∼ #count{X : a(X)} ≥ 4 Note that this normalization is often used in real implementations [21]. 3 Constraints with aggregates as propagators In this section, we present our strategy for evaluating constraints with aggre- gates using propagators that are automatically generated by a compilation-based approach. Hereafter, to simplify the presentation, we assume w.l.o.g. that the bodies of constraints never contain two literals with the same predicate name and constraints contain at most one aggregate literal in the body. 6 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca Some notation and code conventions. Let C be a constraint with an aggregate of the form: : −b1 , ..., bk , #count{V1 , . . . , Vn : l1 , . . . , lm } ≥ g . where g is a constant. we dene :  Given an ASP expression (term, literal, body, rule, etc.) e, vars(e) as the set of variable terms appearing in e;  Given an ASP expression (term, literal, body, rule, etc.) e, pred(e) as the set of all predicate name appearing in e;  Given a literal l, trm(l) as the list of terms appearing in l;  trm(l)[i] with 1 ≤ i ≤ |trm(l)| as the i − th element of the list trm(l) (e.g. let trm(l) = [X, Y, 3], trm(l)[2] is equal to Y );  σ : vars(C) → Uπ as a possible variable assignment from the variables of the constraint to the constants in Uπ ;  Given an ASP expression e, σ(e) as the substitution of the variables appear- ing in e with the constants which their are mapped to;  match(l1 , l2 ), where l1 is a literal and l2 is a ground literal, as a function that checks if ∃σ | σ(l1 ) = l2 ;  body(C) as the set {b1 , ..., bk };  aggregate(C) as the aggregate literal in the constraint C ;  aggregateV ars(C) as the set of variables {V1 , ..., Vn };  aggrLit(C) as the set {l1 , ..., lm };  sharedV ars(C) as the set of variables v such that v ∈ vars(body(C)) ∩ vars(aggrLit(C));  Given an interpretation I , joinT uples as the set of all tuples of the form (t1 , . . . , tm ) such that following conditions are true: • (ti ∈ I + ∨ (ti ∈ (B \ I)+ ∧ ti ∈ / I)) ∀i ∈ {1, . . . , m} where I + denotes the set of positive literals in I . • ∃σ | ∀i ∈ {1, . . . , m} match(σ(li ), ti ) where σ is a possible variable as- signment such that ∀v ∈ vars(aggrLit(C)), σ(v) is dened.  Given an interpretation I and a join tuple (t1 , . . . , tm ) ∈ joinT uples projOnSharedV ar((t1 , . . . , tm )) = (trm(ti )[j] : trm(li )[j] ∈ sharedV ars(C) with 1 ≤ j ≤ trm(ti ) and 1 ≤ i ≤ m);  Given an interpretation I and a join tuple (t1 , . . . , tm ) ∈ joinT uples projOnAggrV ar((t1 , . . . , tm )) = (trm(ti )[j] : trm(li )[j] ∈ aggregateV ars(C) with 1 ≤ j ≤ trm(ti ) and 1 ≤ i ≤ m). In the algorithms that we present in this section and in the appendix we follow the same pseudo-code convention that is used in [22] to ease readability. In particular, the underlined code is produced by the compiler, instead, the not underlined one (e.g., variables and references) represents the code in the scope of the compiler. If a line contains an underlined part closed between , it means that the code inside will be rst interpreted by the compiler (e.g. variables are substituted by their run-time value) and then is printed in the propagator code. For example, given the constraint : −a(X), c(X, Z), #count{Y : b(X, Y )} > 2 then Algorithm 1 at line 6, prints "case a" and "case c". Compilation of Aggregates in ASP: Preliminary Results 7 Algorithm 1 CompilePropagateConstraintWithAggregate Input : A constraint C Output : Prints the propagator for C . 1 begin 2 Il = ∅ 3 buildAggregateJoin(C) 4 switch pred(l) 5 forall the c ∈ body(C) do 6 case pred(c): 7 CompilePropagateConstraintStartingFromLiteral(c,C) 8 break 9 pred(aggrLit(C)) then if pred(l) ∈ 10 CompilePropagateConstraintStartingFromAggregate(C) 11 return Il Algorithm 2 CompilePropagateConstraintStartingFromLiteral Input : A constraint C , a literal c ∈ C Output : Prints an algorithm that is performs the unit propagation of C starting from a ground literal whose predicate is the same of c 1 σ= 2 forall the k = 1, . . . , |trm(c)| do 3 if trm(c)[k] is variable then 4 σ = σ ∪ {trm(c)[k] 7→ trm(l)[k]} 5 B = printN estedJoinLoop(C, c) 6 propagateU ndef ined(B, C) 7 forall the i = |B|, . . . , 1 do 8 σ = σi 9 if u = bi then 10 u=⊥ 11 } 8 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca Compilation procedures. Given a constraint C, Algorithm 1 prints the propaga- tion procedure for C starting from a true literal l. It starts declaring an empty implication list Il , which will be in charge of accumulating the result of the propagation of a literal l, and then prints the code that builds the set of join tuples by executing Algorithm buildAggregateJoin. This algorithm declares dif- ferent sets that store join tuples, and are used to evaluate the truth value of the aggregate literal (pseudo-code and more detailed description in the appendix, algorithm 6). At this point the propagation procedure, as is shown in Algorithm 1 (lines 4-8), continues with a switch on the predicate name of the literal l. In particular, this switch block has a case for each literal c belonging to body(C) in which is printed, by executing Algorithm 2, the code that evaluates rst all body literal starting from c and at the end the aggregate literal. Instead, if the pred(l) belongs to the set of predicate name that appears inside the aggregate literal the evaluation of C starting from the aggregate literal is printed by executing Algorithm 5. Algorithm 2 starts printing the code that builds a variable substi- tution σ that maps all variables belonging to c to constant in l (Algorithm 2 lines 1-4). Then, executing algorithm 7, dierent nested join loops that iterate over all possible ground instantiations of body literals are printed (detailed description and pseudo-code algorithm in appendix Algorithm 7). Once all nested blocks are printed, we can evaluate the aggregate literal and make some inferences. In particular, by executing Algorithm 3, the code for unit propagation is printed. It starts declaring a list of values "sharedVarTuple" that contains values to which shared variables are mapped, in order to consider only those join tuples that match the value of shared variables (lines 2-6 ). Then we declare the reason R in order to accumulate all true literals that are causing propagation (Algorithm 3 lines 7-13). Once the reason is built, if u 6= ⊥ then we have exactly one undened body literal that can be propagated if the aggregate is true (Algorithm 3 lines 14-19). Otherwise u = ⊥ then all body literals are true and so if the propagation condition for the aggregate literal is true (Algorithm 3 lines 20-24) we could infer something on the aggregate literal. Since the aggregate literal in our example is positive, if the size of truekeys is exactly g − 1 then we can propagate as false those join tuples having exactly one literal li with i ∈ {1, . . . , m} undened, that is li ∈ (B \ I)+ ∧ li ∈/ I (algortihm 4 lines 6-7). In this way, we ensure that we do not reach the upper bound g and so the constraint is not violated. In the end, we need to roll back the aggregate join structures by executing algorithm 8. Algorithm 5, instead, prints the code that executes a constraint evaluation starting from the aggregate. In particular, the propagator iterates over possible variables assignment for variables belonging to sharedV ars(C) line 3. For each variable assignment, rst of all, we should update the previously declared ag- gregate join structures in order to discard those join tuples that do not share the values of the shared variables by executing algorithm 8 and then check if the aggregate literal is true (lines 9-12 ). If the aggregate is true the propagator has to build body joins, and so, as is shown in Algorithm 2, nested join loops are printed by executing algorithm 7. Once the last join loop is reached, if there is a body literal undened (algorithm 5 lines 26-27 ) it will be propagated and Compilation of Aggregates in ASP: Preliminary Results 9 Algorithm 3 propagateUndened Input : List of body literals B , and a constraint C Output: Prints code for unit propagation. 1 A = aggrLit(C) 2 sharedV arT uple = ( 3 forall the v ∈ sharedV ars(C) do 4 σ(v) 5 ) 6 updateAggregateW ithSharedV ars(C, true) 7 R = {l} 8 forall the i = 1, . . . , |B| do 9 R = R ∪ {bi } 10 R = R \ {u} 11 for (l1 , . . . , l|A| ) ∈ trueJoin 12 for j = 1, . . . , |A| 13 R = R ∪ {lj } 14 if u 6= ⊥ then { 15 if aggregate(C) is positive then 16 if |trueKey| ≥ g then 17 else 18 if |trueKey ∪ undef Key| < g then 19 Il = Il ∪ (u, R) 20 if aggregate(C) is positive then 21 }else if |trueKey| = g − 1 22 else 23 }else if |trueKey ∪ undef Key| = g 24 propAggregate(C) 25 updateAggregateW ithSharedV ars(C, f alse) 10 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca Algorithm 4 propAggregate Input : A constraint C Output : Prints code to propagate aggregate atom 1 A = aggrLit(C) 2 for (l1 , . . . , l|A| ) ∈ undef Join 3 if projAggrV ars((l1 , . . . , l A  )) ∈ | / trueKey then 4 forall the i = 1, . . . , |A| do 5 if aggregate(C) is positive then 6 + + if li ∈ (B \ I) ∧ {{l1 , . . . , l|A| } \ {li }} ∩ (B \ I) = ∅ then 7 Il = Il ∪ (li , R) 8 else 9 if l i ∈ / I then 10 Il = Il ∪ (li , R) then we can close each join loop. Now what we need is an else if block where the propagator enters if the aggregate literal is false and the propagation condition is true (algorithm 5 lines 36-40 ). In this else-if block, since we want to make inferences on the aggregate, we need to verify that the body without aggregate is true. In order to do this, we need nested join loops, which are printed again by executing algorithm 7, to build possible body join. In the last join loop, if all body literals are true (line 29-30 ) then the propagator makes inferences on the aggregate atom by executing algorithm 4. In the end, before passing to the next shared variables values, aggregate join structures are restored by executing again algorithm 8. Note that both algorithm 2 and 5 remain as it is for constraints with one aggregate literal but as we describe in section 2.3 there is one special case in which the aggregate literal is transformed into two aggregate literals and their conjunction is equivalent to the original aggregate literal. The case aggregates with equality guard. The algorithms presented above can be easily updated to handle aggregates of the form A = #count{V1 , . . . , Vn : l1 , . . . , lm } = g . Indeed, during normalization this aggregate literal is trans- formed in : −A1 , A2 where A1 = #count{V1 , . . . , Vn : l1 , . . . , lm } ≥ g, A2 = not #count{V1 , . . . , Vn : l1 , . . . , lm } ≥ g + 1 Thus, to support this form of aggregate literal, Algorithm 2 changes as fol- lows. The code remains identical for processing A1 but the following lines have to be modied to compile A2 :  At line 18 and 24 we will print an if block to ensure that also A2 is true. Compilation of Aggregates in ASP: Preliminary Results 11 Algorithm 5 CompilePropagateConstraintStartingFromAggregate : A constraint C Input : Prints an algorithm that performs the unit propagation of C starting Output from a ground literal whose predicate is the same of c 1 A=aggrLit(C) 2 σ= 3 for sharedV arT uple ∈ sharedV arKey { 4 forall the i ∈ {1, . . . , |sharedV ars(C)|} do 5 σ = σ ∪ (sharedVars(C)[i], sharedV arT uple[i]) 6 updateAggregateW ithSharedV ars(C, true) 7 propAggr = F alse 8 propBodyLit = F alse 9 if aggregate(C) is positive then 10 if |trueKey| ≥ g then{ 11 else 12 if |trueKey ∪ undef Key| < g then{ 13 while propAggr = F alse ∨ propBodyLit = F alse do 14 if propBodyLit = T rue then 15 propAggr = T rue 16 propBodyLit = T rue 17 B = printN estedJoinLoop(C, N one) 18 R = {l} 19 forall the i = 1, . . . , |B| do 20 R = R ∪ {bi } 21 R = R \ {u} 22 for (l1 , . . . , l | A | ) ∈ trueJoin 23 for j = 1, . . . , |  A | 24 R = R ∪ {lj } 25 if propAggr = F alse then 26 if u 6= ⊥ then 27 Il = Il ∪ (u, R) 28 else 29 if u = ⊥ then 30 propAggregate(C) 31 forall the i = |B|, . . . , 1 do 32 σ = σi 33 if u = b i then 34 u=⊥ 35 } 36 if propAggr = F alse then 37 if aggregate(C) is positive then 38 else if |trueKey| = g − 1 39 else 40 else if |trueKey ∪ undef Key| = g 41 updateAggregateW ithSharedV ars(C, f alse) 42 } 12 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca 600 wasp Execution time (s) 480 wasp-eager-aggr 360 240 120 0 0 10 20 30 40 50 60 Number of instances (a) Combined conguration. 600 wasp Execution time (s) 480 wasp-eager-aggr 360 240 120 0 0 20 40 60 80 100 120 Number of instances (b) Abstract dialectical frameworks. Fig. 1: Experimental results.  At the end is needed an other else if block in which evaluate if A2 can be propagated and if it can be propagated, then, the propagator will check that the A1 is true and nally it makes propagation on A2 . at the same time, Algorithm 5 should be changed as follows:  At line 27 and 40, an if block that check if A2 is true must be added;  A copy of the code described so far must be duplicated so to check rst A2 and then A1 (the entire algorithm 5 contains two twin parts obtained by swapping the role of the two aggregates). This is needed because all possible propagation paths have to be considered. Compilation of Aggregates in ASP: Preliminary Results 13 4 Implementation and Experiments 4.1 Implementation We started from the baseline system presented in [12] that has been extended to support the compilation of the propagation of aggregates. In particular, the implementation follows the execution presented in pseudo-code in algo- rithms of Section 3. The resulting compiler has been implemented in C++, and its output is also C++ code compliant to the wasp propagator interface, and is loaded in the ASP solver as a C++ dynamic library. Moreover, even though, in the compiler pseudo-code, we assumed that there is no repetition of predicates names we explicitly handle the case of duplicated predicates in the real implementation. Basically, when we have two literals with the same predicate name, we have to distinguish the data structure that will be de- clared for both literals in the nested join loops. The latest release is available at https://github.com/WaspWithCompilation/WASP_C. 4.2 Experimental evaluation We carried our an experimental evaluation to empirically assessed the perfor- mance gain of the proposed approach w.r.t. the base solver wasp. Namely, we considered two hard benchmarks of the ASP competitions [9] where there are some constraints containing #count aggregates. The two considered benchmarks are Combined Conguration and Abstract Dialectical Frameworks. In Combined Conguration, the problem is to congure an artifact by com- bining several sub-components in order to achieve some goals; whereas in Ab- stract Dialectical Frameworks the problem is to nd all statements which are necessarily accepted or rejected in a given abstract argumentation framework. In both benchmarks we compile all constraints with aggregates supported by our implementation (i.e. constraints with exaclty one #count aggregate). The experiments were run on an Intel Xeon CPU E7-8880 v4 @ 2.20GHz, time and memory were limited to 10 minutes and 4 GB, respectively. The results are presented in Figure 1a and Figure 1b as two cactus plots. Overall, our approach is able to boost the performance of wasp, with the result of obtaining smaller execution times, on average, and more solved instances (3 more instances for Combined Conguration and 7 more for Abstract Dialectical Frameworks ). The results are very promising, also considering the fact that the benchmarks in the ASP competitions are more oriented towards the evaluation of solving techniques. 5 Conclusion In this paper, we have extended the approach for the automatic compilation of constraints into propagators by adding support for the #count aggregate and we implemented it on top of the ASP solver wasp. Our tool has been empirically 14 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca validated on hard benchmarks from ASP competitions and demonstrate to be eective on improving the base solver wasp both in terms of number of solved instances and in raw speed. Concerning future work, we plan to extend our implementation for supporting constraints containing more than one aggregate, all the other aggregate functions of the ASP Core 2 standard, and possibly aggregates in rules. References 1. Adrian, W.T., Alviano, M., Calimeri, F., Cuteri, B., Dodaro, C., Faber, W., Fuscà, D., Leone, N., Manna, M., Perri, S., Ricca, F., Veltri, P., Zangari, J.: The ASP system DLV: advancements and applications. Künstliche Intell. 32(2-3), 177179 (2018) 2. Alviano, M., Amendola, G., Dodaro, C., Leone, N., Maratea, M., Ricca, F.: Evalu- ation of disjunctive programs in WASP. In: LPNMR. Lecture Notes in Computer Science, vol. 11481, pp. 241255. Springer (2019) 3. Alviano, M., Calimeri, F., Dodaro, C., Fuscà, D., Leone, N., Perri, S., Ricca, F., Veltri, P., Zangari, J.: The ASP system DLV2. In: LPNMR. LNCS, vol. 10377, pp. 215221. Springer (2017). https://doi.org/10.1007/978-3-319-61660- 5_19, https://doi.org/10.1007/978-3-319-61660-5_19 4. Alviano, M., Dodaro, C., Leone, N., Ricca, F.: Advances in WASP. In: LPNMR. LNCS, vol. 9345, pp. 4054. Springer (2015) 5. Amendola, G., Greco, G., Leone, N., Veltri, P.: Modeling and reasoning about NTU games via answer set programming. In: IJCAI. pp. 3845. IJCAI/AAAI Press (2016) 6. Balduccini, M., Lierler, Y.: Constraint answer set solver EZCSP and why integration schemas matter. TPLP 17(4), 462515 (2017). https://doi.org/10.1017/S1471068417000102, https://doi.org/10.1017/S1471068417000102 7. Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92103 (2011) 8. Calimeri, F., Faber, W., Gebser, M., Ianni, G., Kaminski, R., Krennwall- ner, T., Leone, N., Maratea, M., Ricca, F., Schaub, T.: Asp-core-2 in- put language format. Theory Pract. Log. Program. 20(2), 294309 (2020). https://doi.org/10.1017/S1471068419000450 9. Calimeri, F., Gebser, M., Maratea, M., Ricca, F.: Design and results of the fth answer set programming competition. Artif. Intell. 231, 151181 (2016) 10. Cuteri, B., Dodaro, C., Ricca, F., Schüller, P.: Constraints, lazy constraints, or propagators in ASP solving: An empirical analysis. TPLP 17(5-6), 780799 (2017) 11. Cuteri, B., Dodaro, C., Ricca, F., Schüller, P.: Partial com- pilation of ASP programs. TPLP 19(5-6), 857873 (2019). https://doi.org/10.1017/S1471068419000231 12. Cuteri, B., Dodaro, C., Ricca, F., Schüller, P.: Overcoming the grounding bot- tleneck due to constraints in ASP solving: Constraints become propagators. In: IJCAI. pp. 16881694. ijcai.org (2020). https://doi.org/10.24963/ijcai.2020/234 13. Cuteri, B., Reale, K., Ricca, F.: A logic-based question answering system for cul- tural heritage. In: JELIA. Lecture Notes in Computer Science, vol. 11468, pp. 526541. Springer (2019) Compilation of Aggregates in ASP: Preliminary Results 15 14. Dal Palù, A., Dovier, A., Pontelli, E., Rossi, G.: GASP: answer set programming with lazy grounding. Fundam. Inform. 96(3), 297322 (2009) 15. Dodaro, C., Alviano, M., Faber, W., Leone, N., Ricca, F., Sirianni, M.: The birth of a WASP: preliminary report on a new ASP solver. In: CILC. CEUR Workshop Proceedings, vol. 810, pp. 99113. CEUR-WS.org (2011) 16. Dodaro, C., Maratea, M.: Nurse scheduling via answer set programming. In: LP- NMR. LNCS, vol. 10377, pp. 301307. Springer (2017) 17. Erdem, E., Gelfond, M., Leone, N.: Applications of answer set programming. AI Magazine 37(3), 5368 (2016) 18. Erdem, E., Patoglu, V.: Applications of ASP in robotics. KI 32(2-3), 143149 (2018). https://doi.org/10.1007/s13218-018-0544-x 19. Faber, W., Pfeifer, G., Leone, N.: Semantics and complexity of recursive ag- gregates in answer set programming. Artif. Intell. 175(1), 278298 (2011). https://doi.org/10.1016/j.artint.2010.04.002 20. Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Wanko, P.: Theory solving made easy with clingo 5. In: ICLP TCs. OASICS, vol. 52, pp. 2:12:15 (2016) 21. Gebser, M., Kaminski, R., König, A., Schaub, T.: Advances in gringo series 3. In: LPNMR. LNCS, vol. 6645, pp. 345351. Springer (2011) 22. Gebser, M., Leone, N., Maratea, M., Perri, S., Ricca, F., Schaub, T.: Evaluation techniques and systems for answer set programming: a survey. In: IJCAI. pp. 5450 5456. ijcai.org (2018) 23. Gebser, M., Maratea, M., Ricca, F.: The seventh answer set programming com- petition: Design and results. Theory Pract. Log. Program. 20(2), 176204 (2020). https://doi.org/10.1017/S1471068419000061 24. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Comput. 9(3/4), 365386 (1991) 25. Kaufmann, B., Leone, N., Perri, S., Schaub, T.: Grounding and solving in answer set programming. AI Magazine 37(3), 2532 (2016) 26. Lefèvre, C., Nicolas, P.: The rst version of a new ASP solver: Asperix. In: LPNMR. LNCS, vol. 5753, pp. 522527. Springer (2009) 27. Ostrowski, M., Schaub, T.: ASP modulo CSP: the clingcon system. TPLP 12(4-5), 485503 (2012) 28. Schüller, P.: Modeling variations of rst-order horn abduction in answer set pro- gramming. Fundam. Inform. 149(1-2), 159207 (2016) 29. Susman, B., Lierler, Y.: SMT-based constraint answer set solver EZSMT (system description). In: ICLP TCs. OASICS, vol. 52, pp. 1:11:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016) 30. Weinzierl, A.: Blending Lazy-Grounding and CDNL Search for Answer-Set Solving. In: LPNMR. LNCS, vol. 10377, pp. 191204 (2017) 16 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca A Detailed description of all algorithms A.1 Algorithm 6 Algorithm 6, declares dierent sets, that accumulate the aggregate conjunctions (lines 1-5 ), and an empty variable substitution function σ . In order to build possible ground conjunctions of the form l1 , . . . , lm , we need a nested join loop for every lj . Given the nesting level j , the propagator iterates over ground literals aj that are true or undened w.r.t I and update the variable substitution σ mapping variables in A[j] to constant in aj (lines 17-19 ). Once the last nested join is reached (line 20 ), the propagator has to store new values for:  Shared variables (lines 20-23 );  Aggregate variable and join tuple (lines 25-42 ) respectively for true and undened aggregate conjunctions. Note that an aggregate conjunction is undened if ∃aj such that aj is undened, otherwise is true. At the end of each join loop, we roll back the variable substitution σ to its previous state and close nested join loops(lines 43-46 ). A.2 Algorithm 7 Algorithm 7,prints the code that computes all possible body joins. In order to do this,rst reorders body literal with the function computeBodyOrdering that returns a new list B where negative literals are always at the end of B , and c is not in B if c is not None. Once the list of literals B is computed, the algorithm prints a nested join loop for each B[j] such that B[j] is positive and a nested if for each B[j] such that B[j] is negative. Each nested join loop iterates on true literals belonging to I + that match σ(B[j]) and on undened literals that match σ(B[j]) (lines 6-10 ) and update the variable substitution σ with variables in B[j] (lines 13-15 ). For each nested if, since positive literal was already evaluated and so we have a bound for every variable in negative literals (safeness), checks only if σ(B[j]) is true or undened (lines 17-20 ). Compilation of Aggregates in ASP: Preliminary Results 17 Algorithm 6 buildAggregateJoin(C) Input : A constraint C Output : Prints code that builds join tuples and their projection over aggregate and shared variables 1 trueJoin = ∅ 2 undef Join = ∅ 3 sharedV arKey = ∅ 4 trueKey = ∅ 5 undef Key = ∅ 6 σaggr =  7 uaggr := f alse 8 A = aggrLit(C) 9 forall the j = 1, . . . , |A| do 10 j σaggr = σaggr 11 Aj = {a ∈ I + | match(σaggr (A[j]), a)} 12 U Aj = {p ∈ (B \ I)+ | match(σaggr (A[j]), p) ∧ p ∈ / I} 13 for a j ∈ (Aj ∪ U Aj ) { 14 if a j ∈ U Aj then 15 uaggr = true 16 u j = u aggr aggr 17 forall the k = 1, . . . , |trm(A[j])| do 18 if trm(A[j])[k] is variable then 19 σaggr = σaggr ∪ {trm(A[j])[k] 7→ trm(aj )[k]} 20 sharedV arKey = sharedV arKey ∪ { 21 forall the v ∈ sharedV ars(C) do 22 σaggr (v) 23 } 24 25 if uaggr is f alse then 26 trueKey = trueKey ∪ { 27 forall the v ∈ aggregateV ars(C) do 28 σaggr (v) 29 } 30 trueJoin = trueJoin ∪ {( 31 forall the z = 1, . . . , |A| do 32 az 33 )} 34 else 35 undef Key = undef Key ∪ { 36 forall the v ∈ aggregateV ars(C) do 37 σaggr (v) 38 } 39 undef Join = undef Join ∪ {( 40 forall the z = 1, . . . , |A| do 41 az 42 )} 43 forall the j = |A|, . . . , 1 do 44 j σaggr = σaggr 45 j uaggr = uaggr 46 } 18 G. Mazzotta, B. Cuteri, C. Dodaro, F. Ricca Algorithm 7 printNestedJoinLoop Input : A constraint C , a literal c ∈ C that can be also None Output : Return the list of body literals ordered starting from c 1 B = computeBodyOrdering(C, c) 2 u := ⊥ 3 forall the j = 1, . . . , |B| do 4 σj = σ 5 if B[j] is positive then 6 Tj = {t ∈ I+ | match(σ(B[j]), t)} 7 Uj = ∅ 8 if u = ⊥ then 9 Uj = {p ∈ (B \ I)+ | match(σ(B[j]), p) ∧ p ∈ / I} 10 for b j ∈ (Tj ∪ Uj ) { 11 if b j ∈ Uj then 12 u = bj 13 forall the k = 1, . . . , |trm(B[j])| do 14 if trm(B[j])[k] is variable then 15 σ = σ ∪ {trm(B[j])[k] 7→ trm(bj )[k]} 16 else 17 bj = σ(B[j]) 18 if b j ∈ I ∨ (u = ⊥ ∧ bj ∈ (B \ I)){ then 19 if u = ⊥ ∧ b j ∈ (B \ I) then 20 u = bj 21 return B Compilation of Aggregates in ASP: Preliminary Results 19 A.3 Algorithm 8 Algorithm 8, instead, prints the code that discards those join tuples that do not share the values of the shared variables or rolls back the join tuple structures to their previous state. In particular, lines 2-20 are printed if we want to discard join tuples. In this case, rst, we save the previous state in fresh structures lines 2-6 and then we modify the existing ones line 7-20. Otherwise, if we need to roll back join tuples we assign previous state structures to the current ones (lines 22-26 ). Algorithm 8 updateAggregateWithSharedVars Input : A constraint C , a boolean value d Output : Prints code to discard those join tuples that don't match a value of shared variables or restore the initial set of join tuples 1 if d is true then 2 trueJoinP revious = trueJoin 3 undef JoinP revious = undef Join 4 sharedV arKeyP revious = sharedV arKey 5 trueKeyP revious = trueKey 6 undef KeyP revious = undef Key 7 trueKey = ∅ 8 for t ∈ trueJoin { 9 if projOnSharedV ars(t) 6= sharedV arT uple then 10 trueJoin = trueJoin \ {t} 11 else 12 trueKey = trueKey ∪ projOnAggrV ars(t) 13 } 14 undef Key = ∅ 15 for t ∈ undef Join { 16 if projOnSharedV ars(t) 6= sharedV arT uple then 17 undef Join = undef Join \ {t} 18 else 19 undef Key = undef Key ∪ projOnAggrV ars(t) 20 } 21 else 22 trueJoin = trueJoinP revious 23 undef Join = undef JoinP revious 24 sharedV arKey = sharedV arKeyP revious 25 trueKey = trueKeyP revious 26 undef Key = undef KeyP revious