Answer Set Programming(ASP) is a logic-based formalism for knowledge representation and reasoning. Stateof-the-art ASP systems that adopt the Ground & Solve approach are limited by the grounding bottleneck. This issue arises whenever the grounding produces a large propositional program that cannot be eficiently handled during solving. To overcome this limitation, compilation-based solutions have been introduced which led to the development of alternative ASP systems. However, compilation-based ASP systems generate in advance the propositional atoms required for solving the problem. As a consequence, as soon as a large number of propositional atoms is required, also compilation-based approaches exhibit overhead. To address this issue, we develop a novel compilation technique that enables lazy atom discovery during solving. Preliminary results confirmed the efectiveness of our approach.
Over the last years, compilation-based solvers have been developed as a technique for overcoming the grounding bottleneck problem. The idea at the heart of compilation-based solvers is to encode nonground rules into ad-hoc propagators which are able to simulate rule inferences during solving without materializing any ground instantiation. Several solutions of this type were proposed over the years, starting from systems capable of compiling only constraints [13, 14] to solutions capable of compiling entire programs [15], and up to solutions capable of mixing grounding and compilation [16]. All these techniques tackled the grounding bottleneck efectively, allowing to solve out-of-reach instances for state-of-the-art systems and remaining competitive on solving problems not afected by grounding issues. Despite the fact that such techniques completely avoid rules grounding materialization, they need to generate all propositional atoms required to compute the answer sets of ASP programs. As soon as the number of generated atoms increases, compiled solvers exhibit significant overhead [15].
Among alternative approaches, developed for overcoming the grounding bottleneck, it is worth mentioning lazy-grounding systems [21, 22, 23, 24, 25], hybrid formalism [17, 18, 26, 27], and complexitydriven rewritings [19, 20]. Lazy grounding entirely skips the grounding of the program and generates, during solving, ground rules only when their body is true w.r.t. the current interpretation. Even though these systems efectively addressed the grounding bottleneck they showed poor performance, hardly achieving comparable results w.r.t. state-of-the-art ASP solvers [28]. Hybrid formalisms extend the base ASP language by integrating external sources of computation. Complexity-driven program rewritings encode the original program into a diferent formalism, such as propositional epistemic logic programs, or into a disjunctive program generating smaller ground programs. Even though these encodings are in general easier to evaluate and have shown promising results in some practical scenarios [19], they can be exponential in the worst case.
In this section some basic notions about ASP syntax and semantics are given which will be used for introducing compilation-bases ASP solving.
ASP Syntax. A term can be either constant or a variable. Constants are strings starting with lower case letters or positive integers while variables are terms starting with upper case letters. An atom is an expression of the form (1, ..., ) where is a predicate of arity and 1, ..., are terms. A predicate of arity zero is said to be propositional. A literal is an atom , or its negation where represents negation as failure. A literal is positive if it is of the form , negative otherwise. The negative counterpart of literal is denoted as . If all the terms of are constants is said to be a ground literal. A propositional literal is always ground. Given a literal , () denotes the predicate name of . A rule is an expression of the form: ← 1, ..., . where is a positive literal referred to as head of the rule, while 1, ..., is a conjunction of literals referred to as body of the rule. () represents the set of atoms that appear in the head of the rule(it has a size of at most one). () represents the set of literals that appear in the body of the rule. A rule is ground if both () and () are ground. () is ground if all the literals of () are ground literals. Similarly, () is ground if its atom is ground. An empty set of literals is trivially ground. A rule is a fact if () = ∅, it is a constraint if () = ∅. A program Π is a set of rules. Given an ASP expression (a program, a rule etc.), () and () denote respectively the set of predicates and variables appearing in . Given a rule , ℎ() ⊆ () is the set of predicates appearing in (). This notation extends also to programs, and so ℎ(Π) is the set of predicates appearing in the head of some rules in Π. Given a program Π, the Herbrand Universe Π is the set of constants appearing in Π. The Herbrand Base, Π, of program Π is the set of all possible ground atoms that can be built using predicates in Π and constants in Π. The ground instantiation (Π) of a program Π is the union of all the ground instantiations of rules of Π. The dependency graph of a program Π, Π, is a directed labelled graph where the nodes are predicates appearing in Π, and the set of the edges contains a positive (resp. negative) edge (, ) if there exists a rule ∈ Π where (1, . . . , ) is a positive (resp. negative) literal in the body of and (1, . . . , ) the atom in the head of . The Strongly connected components (SCCs) of Π create a partition of predicates of Π. A program Π is said to be stratified if there is no recursion through negation. In other words, Π is stratified if inside Π there is no cycle that involves a negative edge. The ground dependency graph of Π is a dependency graph defined as above, constructed from rules in (Π). A program Π is tight if its dependency graph Π does not contain cycles, it is locally tight if the ground dependency graph does not contain cycles.
ASP Semantics. Given a program Π, an interpretation is a set of literals whose atoms belong to
Π. A literal is true w.r.t. if ∈ , it is false if ∈ , it is undefined otherwise. An interpretation
is inconsistent when both a literal and its complement belong to ; otherwise it is consistent. An
interpretation is said to be total if for each atom ∈ Π either or belongs to , it is partial otherwise.
An interpretation that is both total and consistent is a model of Π if inside (Π) the head of
each rule is true whenever the body of is true. Given a program Π and an interpretation , the
Gelfond-Lifschitz reduct [
Approaches based on compilation showed promising results by efectively addressing the grounding bottleneck and achieving better performances w.r.t. state-of-the-art systems over groundingintensive benchmarks and yet obtaining fairly good results on benchmarks that are not groundingintensive. Even though efective, compilation-based systems are not a silver bullet for solving all types of ASP programs. First of all, compilation-based techniques proposed so far target only a restricted class of ASP programs (i.e., tight programs). Secondly, proposed techniques present a significant overhead when the number of propositional atoms required to compute an answer set increases. Therefore, my research plan is to study whether it is possible to overcome current limitations of compilation-based ASP systems and extend compilation to the entire ASP-Core-2 standard [29]. The first research direction on which I am currently working is the development of a novel compilation-based technique which avoids upfront atom materialization and postpones atom discovery to the solving phase. In this direction, I will study novel compilation-based techniques for compiling recursive and disjunctive programs. These two classes of programs require considering more involved and even more complex propagation scenarios than those considered so far. Together with these broader classes of ASP programs, it would be interesting to investigate the possibility of leveraging compilation for the evaluation of programs with weak constraints.
In this first phase of the research we focused in improving compilation-based ASP solvers by defining a technique, namely lazy atom discovery, for reducing the amount of propositional atoms that these solvers need to generate before starting the solving phase. Such an approach has been formalized and it has been accepted for publication at JELIA 2025. 5.1. Lazy atom discovery The proasp system. proasp [15] is a compilation-based solver for the class of tight ASP programs. A compiled proasp solver is made of two modules, namely Generator and Propagator that are integrated with the Glucose SAT solver. The execution of a compiled proasp solver for a program Π over an arbitrary instance (i.e., a set of facts) consists of two steps. As a first step the compiled Generator module is responsible for generating atoms that are required for solving the problem. In the second step, instead, theGlucose SAT solver takes as input generated atoms and starts the CDCL algorithm for computing an answer set of Π ∪ . During solving, the absence of ground rules forces the SAT solver to delegate the entire CDCL propagation phase to the compiled Propagator module, which derives inferences from the compiled rules (i.e., those in Π) based on the problem instance . proasp with lazy atom discovery. To enable lazy atom discovery, we first identify a subprogram of an input program Π, namely lazy program split, which complies to some syntactic restrictions needed to postpone its evaluation during solving. In particular, must be a stratified subprogram such that ℎ() ∩ ℎ(Π ∖ ) = ∅. That is, predicates appearing in the head of rules of cannot appear in the head of any rule in Π ∖ . Thus, inferences coming from are deterministic and the subprogram does not afect the compilation pipeline of proasp for the remaining rules, i.e., Π ∖ . Once the lazy program split ⊆ Π has been identified, the program Π ∖ follows the typical compilation process described in [15]. Conversely, is compiled with a novel technique into a post-propagator module (i.e., lower priority propagators). This module, that from now on we will call postP, is responsible for simulating rules in () and for lazily discovering atoms in (). To obtain the postP module, we design a compilation strategy that does two main tasks. The first is to extract additional generation rules that are compiled into the proasp Generator module for generating atoms from predicates in ℎ() that appear in (Π ∖ ). Note that atoms generated through these additional generation rules become decision variables of the solver and therefore the solver can assign a truth value to them. The second is to compile rules from into post-propagators capable of mimicking rules in (). One post-propagator for each of program is compiled. Each SCC post-propagator is made of two components. A fixpoint procedure, for deriving true atoms from , and a propagateToFalse procedure for deriving false atoms from by checking support of atoms over predicates in ℎ(). The architecture of proasp with post-propagators is illustrated in Figure 1. Example of compilation For space reasons only the result of the compilation over an example program is shown. Consider the following subprogram :
(, ) ← (, ), ().
Algorithm 1: Fixpoint for component { }
Input : lits : a set of propagated literals
Output : C: a set of conflictual literals
1 begin
2 = ()
3 = ∅
4 while .() > 0 do
5 0 = .()
6 if (0) = “” then
7 := 0[0]; := 0[
= ∪ ℎ is a stratified program that complies to the above restrictions and therefore it can be compiled into a postP module. Consider now program Π ∖ defined as follows:
(, ) ← (), (, ) (, ). (, ) ← (), (, ) (, ).
← (1, ), ().
As already discussed, generation rules need to be extracted from Π ∖ . In this case, only the constraint in Π ∖ contains a literal in ℎ(), and thus only the following generation rule is extracted.
(1, ) ← ().
The above generation rule produces all the atoms of the predicate rnf that appear in the constraint. As it can be observed, here atoms over predicate are no longer materialized while the predicate is partially generated (i.e., only atoms of the form (1, _)).
In the given example, the postP module is made of two SCC-propagators. We call these SCC propagators PropR and PropRnf, just like the predicates defined by the components.
During solving, the post-propagator module is invoked after proasp propagators reach a fixed point (i.e., the SAT solver made a choice and all deterministic inferences coming from such a choice have been inferred and propagated). First, the fixpoint procedure is invoked for deriving true consequences in program according to the current interpretation. Then, the propagateToFalse procedure is invoked for deriving atoms in that can no longer be supported. Propagations coming from the SAT solver and the Propagator module are cached by postP. Such propagations are shufled (using a watched-like structure) to SCC-propagators which will use them as starters in the fixpoint procedure. A starter is a literal of a rule which is fixed for iterating all ground instantiations of the rule containing such a literal. Each SCC-propagator is interested in propagations of tuples belonging to predicates that appear inside the SCC, both in the body and in the head of its rules. In the example, PropR would be interested in predicates {, , }, while PropRnf would be interested in predicates {, , }. To give an idea of how fixpoint is structured, we provide an example of the fixpoint procedure for component { } in the pseudo-code in Algorithm 1. The example is almost trivial since only one starter is needed and the while loop will never repeat in this case. However, the goal of the example is to show the typical structure of a fixpoint procedure for an SCC without going into the technical details.
Once fixpoint completes for a given SCC, a set of conflictual literals is returned. Whenever such a set is non-empty, the SAT solver enters the learning phase to resolve the conflict and restore consistency, if possible.
If no conflict is generated by the Fixpoint procedures, propagateToFalse is called. propagateToFalse can perform false propagation for atoms defined in by checking all the rules that have as head. If the check succeeds, all rules having as head are false and therefore postP propagates to false. The evaluation of rules from by propagateToFalse is made top-down by entering the rules with as starter. During propagateToFalse, a non-generated atom 1 belonging to the predicate set of some ∈ ℎ() might be encountered. This scenario is plausible since the predicate set of is incomplete. Note that there is a restriction on rules of which guarantees that following a specific rule instantiation order, tuples of that are encountered are bound (the order is: head, then predicates not defined in and then the remaining ones). What we have to do at this point is to generate dummy tuples like 1 to proceed with propagateToFalse.
To provide a meaningful example of the propagateToFalse procedure, we should consider the same program from the previous example in which the rule: becomes:
(, ) ← (, ), (, ).
(, ) ← (), (, ), (, ).
propagateToFalse for component { } is defined as described in the pseudo-code in Algorithm 2. propagateToFalse is also called before starting the solving phase over all atoms s.t. () ∈ ℎ() that were generated by the Generator module. This preliminary call tries to propagate atoms from to false as soon as possible. Atoms propagated to false at this step have no possibility to become true again.
Once the CDCL algorithm starts, the propagateToFalse procedure is invoked just after fixpoint completes without conflicts. The atoms that need to be checked via propagateToFalse are tuples (always from program ) that are true without support. These can be either true choices of the solver that did not yet find a support or tuples that have lost their support after a backjump made by the solver due to a conflict. To understand when a tuple loses its support, we keep the rule that generated it. When a supporting tuple changes truth value, all its supported tuples are marked as to-check. This is not memory-expansive as long as there are multiple rules that might generate the same tuple. Things become much worse when there is a one-to-one mapping between tuples and ground rules of Π. propagateToFalse is both necessary for guaranteeing the correctness of ProASP with postP and a solution for anticipating false propagations in such a way that branches in the search space can be closed at a higher level.
Experiments To assess the impact of lazy atom discovery on proasp performance, we conducted an empirical evaluation over the synthetic benchmarks that were considered in [15] for highlighting strengths and weaknesses of the solver. Experiments were run on an Intel(R) Xeon(R) CPU E5-4610 v2 @ 2.30GHz running Debian Linux (3.16.0-4-amd64), with memory and CPU time (i.e., user+system) limited to 12GB and 1200 seconds, respectively. Each system was limited to run on a single core. Obtained results showed that our technique is capable of improving proasp performances. The introduction of lazy atom discovery in the Synth2 benchmark allowed to improve already good results for proasp. Concerning Synth1, instead we can see that the version of proasp with lazy atom discovery was capable of achieving better results than Ground & Solve systems that on this benchmark were the winners of the comparison.
Algorithm 2: Propagate to false for component {rnf}
Input : a - The atom to propagate, reason - propagation reason
Output : canPropagate : propagation can be done with reason or not
1 begin
2 0 =
3 if (0) = “ ” then
4 := 0[0]
5 := 0[
Traditional ASP systems based on the Ground & Solve approach are afected by the grounding bottleneck which limits the applicability of ASP to many real world scenarios. Recently, compilationbased ASP solvers have proven efective in addressing this issue. Nevertheless, existing compilationbased systems still require the upfront materialization of ground atoms, which can be detrimental in certain cases, as noted by [15]. In this work, we introduced a compilation-based technique that avoids the generation of all atoms in advance. We implemented these techniques on top of proasp. Achieved results showed substantial performance gains. As future work, we plan to extend our technique to support recursive programs that, at the moment, cannot be handled by proasp.
) B G ( m e M n o i t u c e x E ) B G ( m e M n o i t u c e x E clingo wasp proasp proasp-postP
2 4 6
Number of solved instances (a) Synth1: Memory Usage clingo wasp proasp proasp-postP 8 8 ) s ( e m i t n o i t u c e x E ) s ( e m i t n o i t u c e x E 150 100 50 0 0 600 500 400 300 200 100 0 0 clingo wasp proasp proasp-postP clingo wasp proasp proasp-postP
2 4 6
Number of solved instances (b) Synth1: Execution Time
2 4 6
Number of solved instances (d) Synth2: Execution Time 8 8 2 4 6
Number of solved instances (c) Synth2: Memory Usage
The author(s) have not employed any Generative AI tools. [8] M. Gebser, R. Kaminski, A. König, T. Schaub, Advances in gringo series 3, in: LPNMR, volume 6645 of LNCS, Springer, 2011, pp. 345–351. [9] M. Alviano, C. Dodaro, N. Leone, F. Ricca, Advances in WASP, volume 9345 of LNCS, Springer, 2015, pp. 40–54. [10] B. Kaufmann, N. Leone, S. Perri, T. Schaub, Grounding and solving in answer set programming,
AI Mag. 37 (2016) 25–32. [11] J. Marques-Silva, I. Lynce, S. Malik, Conflict-driven clause learning SAT solvers, volume 336 of
Frontiers in Artificial Intelligence and Applications, IOS Press, 2021, pp. 133–182. [12] M. Gebser, N. Leone, M. Maratea, S. Perri, F. Ricca, T. Schaub, Evaluation techniques and systems for answer set programming: a survey, in: IJCAI, ijcai.org, 2018, pp. 5450–5456. [13] B. Cuteri, C. Dodaro, F. Ricca, P. Schüller, Overcoming the grounding bottleneck due to constraints in ASP solving: Constraints become propagators, in: IJCAI, ijcai.org, 2020, pp. 1688–1694. [14] G. Mazzotta, F. Ricca, C. Dodaro, Compilation of aggregates in ASP systems, AAAI Press, 2022, pp. 5834–5841. [15] C. Dodaro, G. Mazzotta, F. Ricca, Compilation of tight ASP programs, volume 372 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2023, pp. 557–564. URL: https://doi.org/10.3233/ FAIA230316. doi:10.3233/FAIA230316. [16] C. Dodaro, G. Mazzotta, F. Ricca, Blending grounding and compilation for eficient ASP solving, in: Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR, 2024. [17] M. Balduccini, Y. Lierler, Constraint answer set solver EZCSP and why integration schemas matter,
TPLP 17 (2017) 462–515. [18] M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, P. Wanko, Theory solving made easy with clingo 5, volume 52 of OASICS, Schloss Dagstuhl, 2016, pp. 2:1–2:15. [19] V. Besin, M. Hecher, S. Woltran, Body-decoupled grounding via solving: A novel approach on the
ASP bottleneck, in: IJCAI, ijcai.org, 2022, pp. 2546–2552. [20] A. Beiser, M. Hecher, K. Unalan, S. Woltran, Bypassing the ASP bottleneck: Hybrid grounding by splitting and rewriting, in: IJCAI, ijcai.org, 2024, pp. 3250–3258. [21] J. Bomanson, T. Janhunen, A. Weinzierl, Enhancing lazy grounding with lazy normalization in answer-set programming, AAAI Press, 2019, pp. 2694–2702. [22] C. Lefèvre, P. Nicolas, The first version of a new ASP solver : Asperix, volume 5753 of LNCS,
Springer, 2009, pp. 522–527. [23] Y. Lierler, J. Robbins, Dualgrounder: Lazy instantiation via clingo multi-shot framework, volume 12678 of LNCS, Springer, 2021, pp. 435–441. [24] A. D. Palù, A. Dovier, E. Pontelli, G. Rossi, GASP: answer set programming with lazy grounding,
Fundam. Informaticae 96 (2009) 297–322. [25] A. Weinzierl, Blending lazy-grounding and CDNL search for answer-set solving, volume 10377 of
LNCS, Springer, 2017, pp. 191–204. [26] M. Ostrowski, T. Schaub, ASP modulo CSP: the clingcon system, TPLP 12 (2012) 485–503. [27] B. Susman, Y. Lierler, Smt-based constraint answer set solver EZSMT (system description), volume 52 of OASIcs, Schloss Dagstuhl, 2016, pp. 1:1–1:15. [28] A. Weinzierl, R. Taupe, G. Friedrich, Advancing lazy-grounding ASP solving techniques - restarts, phase saving, heuristics, and more, TPLP 20 (2020) 609–624. [29] F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, M. Maratea, F. Ricca, T. Schaub, Asp-core-2 input language format, Theory Pract. Log. Program. 20 (2020) 294–309.