Overcoming the Grounding Bottleneck Due to Constraints in ASP Solving: Constraints Become Propagators

1 Introduction

Answer Set Programming (ASP) [Brewka et al., 2011] is a declarative formalism for knowledge representation and reasoning based on the stable model semantics [Gelfond and Lifschitz, 1991]. Efficient implementations of ASP, such as CLINGO [Gebser et al., 2016] and DLV [Alviano et al., 2017], are available, which made possible the development of concrete applications. In the recent years, ASP has been widely used for solving several problems in the context of artificial intelligence, such as game theory [Amendola et al., 2016], natural language processing [Schüller, 2016], natural language understanding [Cuteri et al., 2019b], robotics [Erdem and Patoglu, 2018], scheduling [Dodaro and Maratea, 2017], and more [Erdem et al., 2016]. Therefore, the improvement of ASP systems is an interesting research topic in arti-

∗Contact Author

ficial intelligence. Traditional ASP systems are based on the ground&solve approach [Kaufmann et al., 2016], 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. ASP solvers implement an extension the Conflict Driven Clause Learning (CDCL) algorithm [Kaufmann et al., 2016]. Although the ASP implementations based on ground&solve are known to be effective in many contexts [Erdem et al., 2016], the traditional approach has an intrinsic limitation. In particular, there are classes of programs whose evaluation is not feasible because of the combinatorial blowup of the grounding of some rules. This issue is usually referred to as grounding bottleneck. In many practical cases the grounding bottleneck is due to one or few constraints that model the (non) admissibility of problem solutions [Ostrowski and Schaub, 2012; Calimeri et al., 2016].

In the literature, there are several attempts to solve the grounding bottleneck problem [Gebser et al., 2018]. Some of these are based on language extensions that hybridize ASP with other formalisms (such as constraint programming [Ostrowski and Schaub, 2012; Balduccini and Lierler, 2017], and difference logic [Gebser et al., 2016; Susman and Lierler, 2016]) that can be used to express the hard-to-ground constraints. Hybrid formalism are efficiently evaluated by coupling an ASP systems with a solver for the other theory, thus circumventing the grounding bottleneck. There are also approaches that work on plain ASP, such as lazy grounding techniques, that resulted in several promising systems, such as GASP [Dal Palù et al., 2009], ASPERIX [Lefèvre and Nicolas, 2009] and ALPHA [Weinzierl, 2017]. The idea of lazy grounding is to instantiate a rule only when its body is satisfied. In this way, it is possible 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 [Gebser et al., 2018]. A different approach was proposed in [Cuteri et al., 2017], where problematic constraints are removed from the non-ground input program and the resulting program is provided as input to a modified version of a CDCL-based able to simulate the presence of problematic constraints. In [Cuteri et al., 2017] the authors compared two alternative strategies for extending ASP solvers based on CDCL, 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 satisfies 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. However, both lazy instantiation and propagators were based on procedures written in a imperative language and that are specific for the problem at hand. This approach looses the declarative nature of ASP, and is a time consuming task that can be carried out only by developers expert on system APIs. Recently, Cuteri et al. [Cuteri et al., 2019a] presented a strategy to translate (or compile) some non-ground constraints into a dedicated C++ procedure, which is used by the system to lazily instantiate them in an automatic way. This approach keeps declarativity of ASP and is effective when the problematic constraints are likely to be satisfied by a candidate model (i.e., whenever lazy instantiation is effective cfr. [Cuteri et al., 2017]). However, a significant number of problems, especially hard combinatorial problems from ASP competitions [Calimeri et al., 2016] cannot be handled efficiently by systems relying on lazy instantiation [Cuteri et al., 2017].

In this paper, we push forward the idea of [Cuteri et al., 2017; Cuteri et al., 2019a], and we present a novel strategy for translating (compiling) non-ground constraints into dedicated C++ procedures that are used as propagators during the search of the CDCL algorithm. Differently from [Cuteri et al., 2019a], propagators operate on partial interpretations and require radically different algorithms that are more involved than methods on total interpretations. To assess the performance of our approach, we implemented it on top of WASP [Alviano et al., 2015] and conducted an experimental analysis on different benchmarks proposed in the literature. Results show that our approach outperforms state-of-the-art ASP systems in all tested scenarios.

2 Preliminaries

2.1 Answer Set Programming

An ASP program π is a finite set of rules of the form h1| . . . |hn :-b1, . . . , bm. where n,m ≥ 0, n+m̸=0, h1, . . . , hn are atoms and represent the head of the rule, while b1, . . . , bm are literals and represent the body of the rule. We denote by body(r) the set of literals appearing in the body of r. In particular, an atom is an expression of the form p(t1, . . . , tk), where p is a predicate of arity k and t1, . . . , tk are terms. Terms are alphanumeric strings and are either variables or constants. According to Prolog conventions, only variables start with uppercase letters. A literal is an atom a or its negation ∼a, where ∼ denotes the negation as failure. A literal is said to be positive if it is an atom and negative if it is the negation of an atom. For an atom a, the complement is a = ∼a, for a negated atom ∼a, the complement is ∼a = a. For a literal l, trm(l) denotes the list of terms in l, and pred(l) is the name of the predicate of l. A rule is called a constraint if n = 0, and a fact if n = 1 and m = 0.

Algorithm 1 ComputeStableModel

Input : A ground programP Output: A stable model for P or ⊥ 1 begin 2 I := ∅; 3 I := Propagate(I); 4 if I is inconsistent then 5 r := CreateConstraint(I) ; 6 I := RestoreConsistency(I); 7 if I is consistent then P := P ∪ {r}; 8 else return ⊥; 9 else if I total then return I; 10 else 11 I := RestartIfNeeded(I); 12 P :=DeleteConstraintsIfNeeded(P); 13 I := I ∪ ChooseLiteral(I); 14 goto 3;

Function Propagate(I)

1 I = I; 2 for ℓ ∈ I do I := I ∪ Propagation(I, ℓ) ; 3 return I;

An object (atom, rule, etc.) is called ground or propositional, if it contains no variables. Rules are safe, that is each variable occurs in a positive literal of the body. Given a program π, let the Herbrand Universe Uπ be the set of all constants appearing in π and the Herbrand Base Bπ be the set of all possible ground atoms which can be constructed from the predicate symbols appearing in π with the constants of Uπ. B denotes Bπ ∪Bπ. Given a rule r, gnd(r) denotes the set of rules obtained by applying all possible substitutions σ from the variables in r to elements of Uπ. For a program π, the ground instantiation gnd(π) of π is the set ⋃r∈π gnd(r). Stable models of a program π are defined using its ground instantiation gnd(π). An interpretation I for π is a set of literals. I is total if ∀a ∈ Bπ, either a ∈ I or ∼a ∈ I and l ∈ I =⇒ l /∈ I. Given an interpretation I, I + denotes the set of positive literals in I and I - denotes the set of negative literals in I. A ground literal l is true w.r.t. I if l ∈ I, otherwise it is false. A total interpretation I is a model for π if, for every r ∈ gnd(π), at least one atom in the head of r is true w.r.t. I whenever all literals in the body of r are true w.r.t. I. The reduct of a ground program π w.r.t. a model I is the ground program πI , obtained from π by (i) deleting all rules r ∈ π whose negative body is false w.r.t. I and (ii) deleting the negative body from the remaining rules. An interpretation I is a stable model of a program π if I is a model of π, and there is no J such that J is a model of πI and J + ⊂ I + . A program π is coherent if it admits at least one stable model, incoherent otherwise.

2.2 Classical CDCL Evaluation

The standard solving approach for ASP is instantiation followed by a procedure similar to CDCL for SAT with extensions specific to ASP [Kaufmann et al., 2016]. The basic algorithm ComputeStableModel (Π) for finding a stable model of program Π is shown in Algorithm 2. The Function 1 combines unit propagation (as in SAT) with some additional ASPspecific propagations, which ensures the model is stable (cf. [Kaufmann et al., 2016]). The algorithm calls for each additional propagator a procedure called Propagation in Function 1. which takes as input a true literal, and the interpretation, and returns as output the extended interpretation with literals that are inferred and their reason.

Given a partial interpretation I consisting of literals, and a set of rules Π, unit propagation infers a literal ℓ to be true if there is a rule r ∈ Π such that r can be satisfied only by I ∪ {ℓ}. Given the nogood representation C(r) = {∼a1, . . . , ∼an, b1, . . . , bj, ∼bj+1, . . . , ∼bm} of a rule r, then the negation of a literal ℓ ∈ C(r) is unit propagated w.r.t. I and rule r iff C(r) \ {ℓ} ⊆ I. In the following we refer to C(r) \ {ℓ} as the reason for the inference of ℓ.

Pairs (ℓ, reason of ℓ) are stored during the execution of propagation, and will be used to perform conflict resolution, and more specifically during the UIP computation [Alviano et al., 2015]. We refer to the list of such pairs as the implication list. To ensure that models are supported, unit propagation is performed on the Clark completion of Π or alternatively a support propagator is used [Alviano and Dodaro, 2016].

Example 1 Consider the following ground program Π1

ComputeStableModel(Π1) starts with I = ∅ and does not propagate anything in line 3. I is partial and consistent, so the algorithm continues in line 11. Assume no restart and no deletion is performed, and assume ChooseLiteral returns {a}, i.e., I = {a}. Next, Propagate(I) is called which yields I = {a, b, ∼b} where ∼b comes from unit propagation on g5 and b from unit propagation on g6. I is inconsistent and an analysis yields the reason of the conflict, i.e., CreateConstraint(I) = {g7} with g7 :← a. Intuitively, the truth of a leads to an inconsistent interpretation, thus a must be false. Then, the consistency of I is restored (line 6), i.e., I = ∅, and g7 is added to Π1. The algorithm again restarts at line 3 with I = ∅ and propagates I = {∼a, b}, where ∼a comes from unit propagation on g7, and b from unit propagation on g2. I is partial and consistent, therefore lines 11-13 are executed. Assume again that no restart and no constraint deletion happens, and that ChooseLiteral (I) = {c}. Therefore, the algorithm continues in line 3 with I = {∼a, b, c}. Propagation yields I = {∼a, b, c, ∼d} because ∼d is supportpropagated w.r.t. g3 and I (or unit-propagated w.r.t. the completion of g3 and I). I is total and consistent, therefore the algorithm returns I as the first stable model.

3 Constraints as Propagators

In this section we present our strategy for evaluating constraints with propagators that are automatically generated by a compilation-based approach. In the following, we assume w.l.o.g. that the bodies of constraints never contain

Input : A constraint C Output: Prints the propagator for C. 1 begin 2 «Il = ∅» 3 «switch pred(l) » 4 forall the c ∈ body(C) do 5 « case "pred(c)":» 6 CompilePropagateConstraintWithStarter(c,C) 7 « break» 8 «return Il»

two literals with the same predicate name. Algorithms 34 present the pseudo-code of the compiler generating propagators from constraints. To ease readability, we write in red the code that is produced by the compiler, and in black the code (e.g., variables and references) that are in the scope of the compiler. Thus, red lines, written inside the symbols « and », represent the code that is printed by the compiler, and black references in gray lines denote the fact that the compiler is printing the value of such variables. For example, «case "pred(C)"» is equivalent to the C++ instruction printf(�case \"%s\"�,pred(C)). Algorithm 3 takes as input a non-ground ASP constraint C and prints the code of the propagator for C. It starts by declaring in the propagator code an empty implication list (line 2) which will be in charge of accumulating the result of the propagation of a literal l (the literal in input to the propagator), which we call starting literal. Depending on the predicate name of l, the propagator code must evaluate one of the |body(C)| possible join orders. To do so, it writes a switch on the predicate name of l, writing one case for each literal in the constraint. In each case, it prints a dedicated code that is able to propagate l calling algorithm 4. The evaluation is written as a nested join loop, which is a cascade of for and if blocks.

We now describe what is happening in algorithm 4, which receives a constraint C and a literal c ∈ C. First it builds a substitution σ that will be used and updated in the whole nested join. Initially, σ is set to the empty substitution ϵ (line 1). Then, from line 2 to 4 the compiler writes the code that adds to σ a mapping from the variables in c (known at compilation time, thus black in the algorithm) to the constants in l (ground literal known at execution time). Recall that trm(x) returns the list of terms of a literal x. The square notation, commonly used in C++ programming, denotes the access of a list to a specific (one-based) index (e.g. if the list is trm(c) = [X, 2, Y ], then trm(c)[1] is X). At line 5, the algorithm reorders the body of C in a new list B where negative literals are always at the end of B, and c is not in B.

In the propagator code, u will be the complement of the literal that is unit propagated, and it is initialized to ⊥ to denote that it is not known at the beginning. The printing of the code of the nested join loop starts at line 8. Essentially, at each iteration i we either print a for loop if B[i] is positive and an if statement if it is negative. Each subsequent for or if is nested inside the previous one. When B[i] is positive, the propagator will first collect in the set Ti the true literals that match (read it as has a substitution to) σ(B[i]), i.e. the current body literal Bi to which the building substitution σ is applied (line 10). Such true literals are joining the current substitution, and in case of propagation, will build the reason of the propagation. Moreover, if the undefined literal is still ⊥ (line 12) it means the join must also collect the undefined literals that match σ(B[i]), line 11. At line 14 the propagator iterates with a variable bi the union of the true literals and eventually undefined literals just collected. When bi is undefined, u becomes bi (lines 15 - 16). At this point, σ is extended with the variables of the current body literal B[i], by mapping them to the constants in bi (line 17), similarly to what was done before with c and l. On the other hand, when B[i] is negative (line 20) the compiler iterates over a negative literal of the constraint. In such case, all variables have a mapping in σ (because of safety condition of ASP and negative literals are at the end of B). The propagator will determine the ground literal bi = σ(B[i]). At this point, the join can continue either if bi is true, or the undefined u is still ⊥ and bi is undefined (line 22). In the second case, u will be set to be equal to bi. Once the compiler completes the writing of the cascade of nested for and if blocks, and it is in the most nested block, it can write the code that collects the successful match of the constraint as an additional pair in the implication list of the propagator (lines 25-29). The literal l is always part of the reason R (line 25), and the propagator will also add to R all the true literals in the join (all bi, beside bi = u). The complement of u which is a propagated literal, together with its reason R are added to the implication list (29). Finally, from line 30 to line 34, the compiler writes the code that rolls back sigma to its previous state (at the end of each block), and eventually sets u back to ⊥ in case it is equal to bi and closes the parenthesis of the nested for and if blocks. In rough terms, the compiler produces that code of a procedure that is able to find an instantiation of the constraint with a single undefined literal to be unit propagated.

3.1 Compilation Example

To better understand what the compiler actually prints, in algorithm 5 we provide an example of a generated propagator for a small constraint. The compiled constraint C in the example is b(X), c(X,Y), ∼ d(X,1). The input of the propagator is an interpretation I and a starting literal l, and the output is the implication list containing literals to be propagated with their reasons.

First the propagator switches on the predicate name of the starting literal l (line 2). There is a case for each predicate name appearing in C, i.e., "b", "c" and "d". For the sake of readability we present the single case for predicate name "b" (lines 4-36). The propagator creates the substitution σ, where the variable X is mapped to the first (and only) constant of l (lines 4 and 5). Then the literal u is initialized to ⊥ and σ is stored in σ1 so that it can be rolled back at each iteration of the next loop. Subsequently, the propagator collects all the true atoms of c(X, Y ), where X is first replaced by the constant in l by the application of σ, as well as all the undefined atoms of c(X, Y ) analogously. Then, the propagator iterates over true and undefined atoms at line 12, continuing the join.

For each b1 in T1 ∪ U1, the propagator checks whether b1 is undefined and eventually updates u, if no undefined has been found up to now. Then σ is extended by the mappings of X and Y respectively to the first and second constants in b1 (lines 16-17). At this point, in line 18, the propagator handles the negative literal ∼d(X, 1), which becomes a ground literal b2 after the substitution with σ; and the propagator checks whether b2 is the first undefined (and updates u), or b2 is true and a complete substitution is found. In these cases the propagator execution would reach the innermost code (from line 24) where it adds a propagation to the output implication list. In particular, if u = b1, b1 is the propagated literal and the reason is R ∪ {b2}, otherwise (u = b2), b2 is the propagated literal and the reason is R ∪ {b1}. At lines 30 to 32 and 33 to

36, the propagator restores the state of σ and eventually the undefined literal to ⊥ and closes a nested code block.

3.2 Implementation

The implementation follows the execution presented in pseudo-code in algorithms 3 and 4. The 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. Several optimization have been implemented, some of them discussed in the following.

Nested loops are made efficient by using proper indexes on terms, for which we use hash-maps to access matching ground literals. This is possible since the order of evaluation is fixed and the predicates extensions can be indexed statically (index terms are known at compilation time). For example, if we evaluate :- a(X,Y), b(Y,Z) with a as starter, we can benefit from indexing the extension of the predicate b on the first term (variable Y). By using a predicate-wise split of the interpretation and indexes, we highly optimize the propagator code related to interpretation access (e.g. lines 10, 13 and 22 of algorithm4). Moreover, even though, in the compiler pseudo-code, we assumed that there is no repetition of predicates names, we explicitly handle such cases in the implementation: basically, we detect when the same undefined literal is used more than once in the same nested join. The implementation also supports built-in arithmetic comparisons, and features a heuristic to employ a smart body ordering (line 5 of Algorithm 3). At the moment aggregates cannot be compiled. The latest release is available at https://github.com/wasp-eager/wasp-eager together with the experiments benchmarks.

4 Experiments

In order to empirically assess the impact of the proposed technique, we considered several benchmarks used in previous editions of the ASP Competitions [Calimeri et al., 2016] or proposed in the literature, namely Incremental Scheduling, Natural Language Processing (NLP) using three different objective functions (cardinality, coherence and weighted abduction), Packing, and Partner Units. All benchmarks contain at least one constraint whose grounding is expensive from a computational point of view. We used as reference for the state-of-the-art the traditional ASP system CLINGO [Gebser et al., 2016] and the lazy-grounding based ASP system ALPHA [Weinzierl, 2017]. It is important to observe that some of the encodings include features that are not currently supported by ALPHA, e.g., weak constraints. For such benchmarks, the performance of ALPHA is not reported. Moreover, we included in the comparison the solver WASP [Alviano et al., 2015] and the version of WASP implementing the lazy propagator as described in [Cuteri et al., 2019a] referred to as WASP-LAZY. In the following, our implementation is referred to as WASP-EAGER. All versions of WASP use CLINGO as grounder (executed with the option �output=smodels). WASP-LAZY and WASP-EAGER compile as lazy and eager propagators, respectively, all constraints that do not contain aggregates in the encodings, and therefore such constraints are not grounded in advance. Note that compilation is done only once for each benchmark and its running time is negligible (less than 2 seconds). The experiments were run on an Intel Xeon CPU E7-8880 v4 @ 2.20GHz, time and memory were limited to 2 hours and 5 GB, respectively.

An overview of the obtained results is given in Table 1: we report the number of solved instances, N/A indicates that the

Input : An interpretation I and a literal l to propagate Output: An implication list 1 Il = ∅ 2 switch pred(l) do 3 case "b" 4 σ = ϵ 5 σ = σ ∪ {X ↦→ trm(l)[1]} 6 u = ⊥ 7 σ1 = σ 8 T1 = {t ∈ I + | match(σ(c(X, Y ), t))} 9 U1 = ∅ 10 if u = ⊥ then 11 U1 = {p ∈ (B\I)+ | match(σ(c(X, Y ), p)} 12 forall the b1 ∈ T1 ∪ U1 do 13 { 14 if b1 ∈ U1 then 15 u = b1 16 σ = σ ∪ {X ↦→ trm(b1)[1]} 17 σ = σ ∪ {Y ↦→ trm(b1)[2]} 18 b2 = σ(∼d(X, 1)); 19 σ2 = σ 20 if b2 ∈ I ∨ (u = ⊥ ∧ b2 ∈ (B \ I)) then 21 { 22 if u = ⊥ ∧ b2 ∈ (B \ I) then 23 u = b2; 24 R = {l}; 25 R = R ∪ {b1}; 26 R = R ∪ {b2}; 27 R = R \ {u}; 28 Il = Il ∪ {(u, R)}; 29 σ = σ2; 30 if u = b2 then 31 u = ⊥ 32 } 33 σ = σ1 34 if u = b1 then 35 u = ⊥ 36 } 37 case "c" 38 . . . ; // analogous to previous case 39 break 40 case "d" 41 . . . ; // analogous to previous case 42 break 43 return Il

solver does not support the encoding of the benchmark. As a first comment, it is possible to observe that WASP-EAGER outperforms all other tested systems, solving 71, 73, and 79 more instances than CLINGO, WASP, and WASP-LAZY, respectively. Interestingly, WASP-EAGER outperforms the traditional systems CLINGO and WASP in all benchmarks. In particular, we observe that CLASP and WASP often exceed the memory limit in many of the unsolved instances due to the large number of constraints produced during the grounding step, whereas WASP-EAGER does not instantiate such constraints. This is particularly evident in Packing, where no instance can be grounded within the allotted memory limit and therefore the solving step of CLINGO and WASP does not even start. Concerning WASP-LAZY, we observe that it is competitive with WASP-EAGER only on NLP as shown also in [Cuteri et al., 2017]. This behavior can be explained by the fact that WASP-LAZY lazily instantiates the problematic constraints whenever they are violated by a stable model candidate. In NLP, WASP-LAZY performs a small number of failing stable model checks (on average less than 100 checks are required). Instead, in other problems, each stable model contains many violations of constraints, leading the solver to inefficient search in harder instances. Finally, we report that ALPHA solves no instance within the allotted time and memory. However, ALPHA exceeds the time limit in 22 out of 47 Packing instances, where as CLINGO and WASP exceed the memory limit for all unsolved instances. This confirms that lazy grounding systems, like ALPHA, can use less memory than ground&solve systems, even if in this benchmark ALPHA is not competitive with WASP-EAGER.

Concerning solving times, we show aggregated results in the cactus plot of Figure 1. We recall that in a cactus plot a line is reported for each combination of tested system; where instances are ordered by solving time and a point (i, j) in the graph represents that the i-th instance is solved in j seconds. It is possible to observe that WASP-EAGER can solve the majority of the instances (217 out of 231) within 1200 seconds and it in general scales better than all other tested systems, solving more instances with lower running times.

5 RelatedWork

Traditional ASP systems, like CLINGO [Gebser et al., 2016] and DLV [Alviano et al., 2017], are based on the ground&solve approach. Grounding is performed using semi-naïve database evaluation techniques [Ullman, 1988] for avoiding duplicate work during grounding, whereas solvers are nowadays based on the CDCL algorithm [Kaufmann et al., 2016]. These approaches intrinsically suffer from the grounding bottleneck. The only alternative to the traditional approach working on plain ASP is lazy grounding, as implemented by GASP [Dal Palù et al., 2009], ASPERIX [Lefevre et al., 2017], and ALPHA [Weinzierl, 2017]. In lazy grounding a rule is instantiated only when its body is satisfied in the current assignment of the search process.

Our approach extends traditional systems to avoid the grounding bottleneck due to constraints, and can be viewed as a hybrid solution between traditional and lazy grounding systems. Indeed, given a non-ground input program Π and a set of constraints C ⊂ Π, it uses the ground&solve approach on Π \ C, whereas constraints in C are not instantiated but simulated by propagators automatically integrated in the CDCL. An important difference with lazy grounding is that in our approach the problematic constrains are never instantiated.

Our strategy is similar in principle with the lazy approach presented in [Cuteri et al., 2019a]. However, constraints in C are not compiled into propagators but they are instantiated when they are violated by a stable model of Π \ C. Moreover, the lazy approach works only on total interpretations, whereas our propagator-based approach works also on partial interpretations. This has a huge impact on the performance as shown in [Cuteri et al., 2017] and in our experiments. Notably, our approach needs no language extension as CASP [Balduccini and Lierler, 2017; Ostrowski and Schaub, 2012], ASPMT [Bartholomew and Lee, 2014] and DLVHEX [Redl, 2016].

6 Conclusion

In this paper, we presented a novel approach for the automatic compilation of constraints into propagators and we implemented it on top of the ASP solver WASP. The performance of our tool has been empirically validated on benchmarks whose evaluation was not feasible due to the combinatorial blowup of the grounding of some constraints. Results show that our solution outperforms state-of-the-art systems on benchmarks modeling AI problems. Concerning future work, we plan to extend our implementation for supporting also other ASP constructs, such as aggregates.

Acknowledgments

This work was partially supported by MISE under PON MAP4ID Prog. n. F/190138/01-03/X44.