Answer Set Programming (ASP) is a well-known problemsolving formalism in computational logic. Among the knowledge modeling constructs that make ASP eective in representing complex problems are aggregates. 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. 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 grounding bottleneck has been proposed that is based on ASP program compilation. 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.
Answer Set Programming (ASP) [
A key role in the development of applications is played by system
performance, 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 [
Commons License Attribution 4.0 International (CC BY 4.0).
ASP implementations are eective in many contexts [
Several attempts have been made to solve the grounding bottleneck
problem [
Recently a dierent approach was proposed that is based on the compilation
of problematic constraints as propagators [
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 [
h1j : : : jhn : b1; : : : ; bm: with n + m > 0 where h1j : : : jhn 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 8i 2 f1; : : : ; kg, ti is a constant 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, 2 f=; <; ; >; g is a predened comparison 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 2 f#count; #sumg is an aggregate 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 fT erms : Conjg, 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 Herbrand 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 variables in r to constant in U . Given a program , instead, ground( ) = Sr2 ground(r). An interpretation I is a set of literals. In particular, I is total if 8a 2 B (a 2 I_ a 2 I) ^ (a 2 I ! a 2= I). A literal l is true w.r.t I if l 2 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 multiset [t1j(t1; : : : ; tn) : conj 2 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 = #countf(1 : p(1; 1)); (2 : p(2; 1)); (3 : p(3; 1))g > 1 and let I = fp(1; 1); p(2; 1); p(3; 1)g. 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 8 r 2 ground( )(8 l 2 body(r); l 2 I) ! (9a 2 head(r) : a 2 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 body false w.r.t I. Let I be a model for , I is also a stable model for if 6 9 I0 I such that I0 is a model for I . Given a program , is coherent if it 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 interpretation 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)ja(4): r3 : b(1; 1)jnB(1; 1): r4 : b(1; 2)jnB(1; 2): r5 : b(2; 2)jnB(2; 2): r6 : b(2; 1)jnB(2; 1): r7 : : a(1); #countf1 : b(1; 1); 2 : b(1; 2)g > 1 r8 : : a(2); #countf1 : b(2; 2); 2 : b(2; 1)g > 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:
nB(2; 1) to ensure that the model will be also a stable From r6 is inferred model 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 2 f<; ; >; ; =g, 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 =: #countfX : a(X)g = 3, it will be normalized as follow:
C0 =: #countfX : a(X)g 3; #countfX : a(X)g 4
Note that this normalization is often used in real implementations [
Constraints with aggregates as propagators In this section, we present our strategy for evaluating constraints with aggregates 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. Some notation and code conventions. Let C be a constraint with an aggregate of the form: : b1; :::; bk; #countfV1; : : : ; Vn : l1; : : : ; lmg where g is a constant.
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 jtrm(l)j as the i th element of the list trm(l) (e.g.
let trm(l) = [X; Y; 3], trm(l)[
: 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 appearing 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 9 j (l1) = l2; body(C) as the set fb1; :::; bkg; aggregate(C) as the aggregate literal in the constraint C; aggregateV ars(C) as the set of variables fV1; :::; Vng; aggrLit(C) as the set fl1; :::; lmg; sharedV ars(C) as the set of variables v such that v 2 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 2 I+ _ (ti 2 (B n I)+ ^ ti 2= I)) 8i 2 f1; : : : ; mg where I+ denotes the set of positive literals in I. 9 j 8i 2 f1; : : : ; mg match( (li); ti) where is a possible variable assignment such that 8v 2 vars(aggrLit(C)); (v) is dened.
Given an interpretation I and a join tuple (t1; : : : ; tm) 2 joinT uples projOnSharedV ar((t1; : : : ; tm)) = (trm(ti)[j] : trm(li)[j] 2 sharedV ars(C) with 1 j trm(ti) and 1 i m); Given an interpretation I and a join tuple (t1; : : : ; tm) 2 joinT uples projOnAggrV ar((t1; : : : ; tm)) = (trm(ti)[j] : trm(li)[j] 2 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 [
Input : A constraint C
Output: Prints the propagator for C. 1 begin 2 Il = ; 3 buildAggregateJoin(C) 4 switch pred(l) Algorithm 2 CompilePropagateConstraintStartingFromLiteral
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; : : : ; jtrm(c)j do 3 if trm(c)[k] is variable then 4 = [ ftrm(c)[k] 7! trm(l)[k ]g 5 B = printN estedJoinLoop(C; c) 6 propagateU ndef ined(B; C) 7 forall the i = jBj; : : : ; 1 do 8 = i 9 if u = bi then Compilation procedures. Given a constraint C, Algorithm 1 prints the propagation 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 different 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 substitution 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 2 f1; : : : ; mg undened, that is li 2 (B n I)+ ^ li 2= 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 aggregate 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
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 2 sharedV ars(C) do 4 (v ) 5 ) 6 updateAggregateW ithSharedV ars(C; true) 7 R = flg 8 forall the i = 1; : : : ; jBj do 9 R = R [ fbi g 10 R = R n fug 11 for (l1; : : : ; ljA 12 for j = 1; : : : ; jA j) 2 trueJoin
j 13 R = R [ fljg 14 if u 6= ? then { 15 if aggregate(C) is positive then 16 if jtrueKeyj g then 17 else 18 22 else 23
if jtrueKey [ undef Keyj < g then 19 Il = Il [ (u; R) 20 if aggregate(C) is positive then 21 }else if jtrueKeyj = g 1
}else if jtrueKey [ undef Keyj = g 24 propAggregate(C) 25 updateAggregateW ithSharedV ars(C; f alse)
Input : A constraint C
Output: Prints code to propagate aggregate atom 1 A = aggrLit(C) 2 for (l1; : : : ; ljA j) 2 undef Join 3 if projAggrV ars((l1; : : : ; ljA
)) 2= trueKey then 4 forall the i = 1; : : : ; jAj do 5 if aggregate(C) is positive then 6 if li 2 (B n I)+ ^ ffl1; : : : ; ljAjg n fli gg \ (B n I)+ = ; then 7 else
Il = Il [ (li ; R) if li
2= I then
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 = #countfV1; : : : ; Vn : l1; : : : ; lmg = g. Indeed, during normalization this aggregate literal is transformed in :
A1; A2 where
A1 = #countfV1; : : : ; Vn : l1; : : : ; lmg A2 = not #countfV1; : : : ; Vn : l1; : : : ; lmg g; g + 1
Thus, to support this form of aggregate literal, Algorithm 2 changes as follows. 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. Algorithm 5 CompilePropagateConstraintStartingFromAggregate Input : A constraint C Output: Prints an algorithm that performs the unit propagation of C starting from a ground literal whose predicate is the same of c 1 A=aggrLit(C) 2 = 3 for sharedV arT uple 2 sharedV arKey { 4 forall the i 2 f1; : : : ; jsharedV ars(C)jg 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 jtrueKeyj g then{ 11 else 12
if jtrueKey [ undef Keyj < g then{ 13 while propAggr = F alse _ propBodyLit = F alse do 14 if propBodyLit = T rue then 15 propAggr = T rue else if u = ? then propAggregate(C) forall the i = jBj; : : : ; 1 do
= i if u = bi then
u = ? g if propAggr = F alse then if aggregate(C) is positive then
else if jtrueKeyj = g 1 else
else if jtrueKey [ undef Keyj = g 41 updateAggregateW ithSharedV ars(C; f alse) 42 }
wasp wasp-eager-aggr 10 20 30 40 50
60
Number of instances (a) Combined conguration.
wasp wasp-eager-aggr 20 40 60 80 100
120
(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. 4.1
We started from the baseline system presented in [
Experimental evaluation
We carried our an experimental evaluation to empirically assessed the
performance gain of the proposed approach w.r.t. the base solver wasp. Namely, we
considered two hard benchmarks of the ASP competitions [
In Combined Conguration , the problem is to congure an artifact by combining several sub-components in order to achieve some goals; whereas in Abstract 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
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 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. A.1
Algorithm 6
Detailed description of all algorithms 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:
Aggregate variable and join tuple ( lines 25-42 ) respectively for true and undened aggregate conjunctions. Note that an aggregate conjunction is undened if 9aj such that aj is undened, otherwise is true.
At the end of each join loop, we roll back the variable substitution previous state and close nested join loops( lines 43-46 ). to its 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 ).
Algorithm 6 buildAggregateJoin(C)
Input : A constraint C Output: Prints code that builds join tuples and their projection over aggregate and shared variables 1 trueJ oin = ; 2 undef J oin = ; 3 sharedV arKey = ; 4 trueKey = ; 5 undef Key = ; 6 aggr = 7 uaggr := f alse 8 A = aggrLit(C) 9 forall the j = 1; : : : ; jAj do j aggr = aggr Aj = fa 2 I+ j match( aggr(A[j] ); a)g U Aj = fp 2 (B n I)+ j match( aggr(A[j] ); p) ^ p 2= Ig for aj 2 (Aj [ U Aj ) { if aj 2 U Aj then uaggr = true j uaggr = uaggr forall the k = 1; : : : ; jtrm(A[j])j do if trm(A[j])[k] is variable then
aggr = aggr [ ftrm(A[j])[k] sharedV arKey = sharedV arKey [ f forall the v 2 sharedV ars(C) do aggr(v ) 7! trm(aj )[k ]g 15 8 9 10 11 12 13 14 15 16 17 18 19 20 21 return B 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 ).