Answer Set Programming (ASP) systems following the Ground&Solve approach are afected by the grounding bottleneck problem, where the grounding phase can cause a combinatorial explosion in program size, making solving unfeasible. Compilation-based ASP solving addresses this by simulating rule inferences through ad hoc propagators, avoiding the grounding phase. However, existing approaches require all propositional atoms to be computed upfront, resulting in overhead as the number of generated atoms grows. In this paper, we investigate how compilation-based technique can be enhanced by deferring the evaluation of rules generating large number of atoms, and so enabling atoms to be discovered lazily during solving. Preliminary results demonstrate significant performance improvements over traditional compilation-based solvers.
Answer Set Programming (ASP) [1, 2] is a well-established declarative paradigm based on the stable model semantics [2, 3]. Nowadays, ASP has found extensive applications in a variety of fields, including Planning [4], Scheduling [5, 6, 7], Robotics [8], Natural Language Processing [9, 10, 11, 12], and Databases [13, 14, 15], among many others [16, 17]. The success of ASP stems from the two main strengths of such formalism. First, it provides a highly expressive language that enables the concise modeling of hard combinatorial problems [18]. Second, powerful solvers [19] make it a practical solution for tackling real-world context [17, 20] as well as industrial applications [21, 22, 23, 24].
Standard ASP systems, such as clingo [25] and dlv [26], follow the Ground&Solve approach [27]. Basically, the evaluation of a program is performed in two phases: grounding, which instantiates rules by replacing variables with constants, and solving, where answer sets are computed using CDCL-based algorithms [28]. While this workflow is efective in many scenarios, it sufers from a major limitation known as the grounding bottleneck [19]. In several practical cases [29, 30], the grounding phase causes a combinatorial explosion in the size of the program, making the solving unfeasible. Thus, the optimization of ASP systems continues to be a pivotal research area, as system performance plays a critical role in enabling the development of eficient applications [19].
To overcome this limitation, various techniques have been proposed, including hybrid approaches [31, 25, 30, 32], lazy grounding [33, 34, 35, 36, 37], complexity-aware rewritings [38], and compilation-based solving [39, 40, 41, 42].
Compilation-based techniques tackle the grounding bottleneck by translating non-ground rules into specialized procedures, known as propagators, which simulate rules’ inferences during solving without materializing the corresponding ground rules. Empirical evidence showed that these techniques efectively tackled the grounding bottleneck problem by solving instances that were out-of-reach for state-of-the-art systems [41, 42, 43]. However, compilation-based systems require propositional atoms, needed to compute an answer set, to be generated ahead of solving. As it has been pointed out by Dodaro et al. (2023) when the number of atoms grows large, this upfront computation leads to considerable overhead.
In this paper, we describe by examples a possible strategy to overcome this limitation and apply it to a few use cases. The idea is to discover some of the atoms incrementally during solving. These atoms are created dynamically, only when needed for truth assignment, instead of being precomputed, thus eliminating the overhead of the upfront atom computation. In particular, we propose an implementation of such technique on top of the compilation-based ASP system proasp [42, 43] and preliminary experiments aimed at assessing the impact of the proposed technique. Obtained results show that lazy atom discovery significantly reduces both memory usage and runtime, ofering a scalable and eficient alternative to traditional compilation-based solving.
In this section we provide an overview of the ASP language, focusing on the concepts relevant for understanding the contribution of this paper. A more comprehensive description can be found in the existing literature. [1, 44, 45].
ASP Syntax. A term can either be a variable or a constant. A variable is a string starting with upper case letter, while a constant is a number or a string starting with lowercase letter. An atom is an expression of the form (1, . . . , ) where is a predicate of arity ≥ 0 and 1, . . . , are terms. A literal is either an atom or its negation ∼ , where ∼ represents negation as failure. Given a literal = (resp. ∼ ), denotes the complement of l that is ∼ (resp. ); while () denotes the set of terms appearing in literal . A literal is ground if it does not contain any variable. A positive literal is of the form , where is an atom, while ∼ is a negative literal. For a set of literals , + (resp. − ) denotes the set of positive (resp. negative) literals appearing in . A rule is an expression of the form ℎ ← 1, . . . , where ℎ is an atom referred to as head that can be also omitted, and 1, . . . , , with > 0, is a conjunction of literals referred to as . Given a rule , () is the set of literals appearing in the body of while () is the set of atoms appearing in the head of . A rule is a constraint if () = ∅; or it is a fact if () = ∅. Moreover, is safe if each variable appearing in appears also in ()+. A program Π is a set of safe rules. Given an ASP expression (a program, a rule etc.), () and () denotes 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 occurring in Π, while the Herbrand base Π is the set of ground atoms that can be obtained from predicates of Π and constants in Π. The dependency graph of program Π is a labeled graph Π = ⟨, ⟩, where is the set of predicates appearing in Π and contains a positive (resp. negative) edge from to if there exists a rule ∈ Π such that appears in ()+ (resp. appears in ()− ) and ∈ ℎ(). Program Π is said to be stratified if there exist no loop in Π involving negative edges; tight if Π does not contain positive loops [46]. We focus on tight ASP programs, as this class is suficiently expressive for our purposes while remaining amenable to modeling many complex problems [29], and corresponds to the class supported by proasp [42, 43]. Stable Model Semantics. Given a program Π, an interpretation is a set of literals over atoms in Π. A literal is true w.r.t. (i.e., |= ) if ∈ ; false (i.e. ̸|= ) if ∈ ; undefined otherwise. A conjunction of literals is true w.r.t. (i.e., |= ) if |= for each in ; false (i.e. ̸|= ) if there exists in such that ̸|= ; undefined otherwise. An interpretation is total if for each atom ∈ Π, ∈ or ∼ ∈ . An interpretation is consistent if it does not exist ∈ such that ∈ . An atom ∈ Π is supported in Π w.r.t. if there exists ∈ (Π) such that () = and |= (). Given a rule ∈ (Π), then is satisfied w.r.t. if |= () or ̸|= (). A total and consistent interpretation is a model of Π if all rules in (Π) are satisfied. Let be a model of Π, then is a supported model if each positive literal in is supported in Π w.r.t. . Moreover, is a stable model (or an answer set) of Π if is a ⊂ -minimal model of its Gelfond-Lifschitz reduct [2]. For a program Π, (Π) denotes the set of answer set of Π. For the class of programs considered in this paper (i.e., tight programs) supported models coincide with answer sets.
Standard ASP systems [26, 25] compute stable models of a program Π in two stages. First, a grounder module computes (Π), and then a solver module computes answer sets of Π by implementing an extension of the CDCL (Conflict Driven Clause Learning) with propagators specific for ASP [ 27]. Such an approach is afected by a limitation known as grounding bottleneck. In many cases of practical interest (Π) contains a large number of rules and atoms that cannot be stored in memory, thus preventing the solving stage from even beginning. Compilation-based ASP solvers tackle such an issue by compiling a logic program into an ad-hoc solver, made of rule-specific propagators, that simulate inferences deriving from (Π) without explicitly materializing ground rules. In what follows we recall how the compilation-based ASP solver proasp works and we discuss possible limitations of this approach.
proasp is a compilation-based ASP solver which supports the class of tight ASP programs. The main idea behind the proasp approach is the following: “Given an ASP program Π, we build an ad-hoc solver for evaluating Π. Then, for each set of facts the ad-hoc solver searches for an answer set of Π ∪ .” Consider the following program Π: 1 : () ← (), () 2 : () ← (), () 3 : ← (), ( ), < .
If we consider rules 1 and 2, and a possible constant , then the following propagations may derive from them: • () is true if and only if () is true and () is false.
• () is true if and only if () is true and () is false.
These propagations guarantee that rules 1 and 2 are satisfied and atoms over predicates and are supported w.r.t. Π. On the other hand, if we consider the constraint 3 the following propagation may derive from it: • if there exists such that () is true then for each value > , () must be false; • if there exists such that () is true then for each value < , () must be false. Such propagations guarantee that the constraint 3 is satisfied.
Based on these inferences we can design a rule-specific propagator for each ∈ Π. For space reasons we report only a possible propagator for 1 (Algorithm 1) and 3 (Algorithm 2), since the propagator for 2 is equal to (Algorithm 1) modulo predicate renaming.
Given the set of facts = {(
Classical CDCL implementations follow the choose-propagate-learn pattern starting from an empty interpretation . At each step, a literal is heuristically chosen and added to . Then is propagated for deriving further literals from rules in Π. In our setting propagation is demanded to rule-specific propagators (Algorithms 1 and 2) which infer new literals to be added to . During propagation, if the interpretation becomes inconsistent, then the learn phase is started for analyzing conflicting literals (i.e., ∈ and ∈ ) to restore consistency of . If consistency can be restored, then the process Algorithm 1 Propagator for () ← (), ().
Input : An interpretation , and a literal ∈ 1 begin 2 if () = “a”: 3 := [0] 4 if ∈ +: 5 propagate {(), ∼ ()} 6 else: 7 if () ∈ +: 8 propagate {()} 9 else if ∼ () ∈ − : 10 propagate {∼ ()} Algorithm 2 Propagator for ← (), ( ), < .
Input : An interpretation , and a literal ∈ 1 begin 2 if () = “a” and ∈ +: 3 := [0] 4 for all ∈ Π s.t. > : 5 propagate ∼ () 6 := [0] 7 for all ∈ Π s.t. < : 8 propagate ∼ () back-jumps to the choices that led to the conflict and continues the search. On the other hand, if consistency cannot be restored, then the algorithm stops since program Π has no models. Finally, as soon as is total and consistent then is an answer set of Π ∪ .
The compilation-based ASP solver proasp generalizes the example discussed so far, allowing the compilation of tight ASP programs into ad-hoc solvers [43].
Given a (non-ground) program Π, at compilation stage proasp extracts two subprograms, namely a propagator and generator program from Π. The propagator program is obtained by normalizing rules of Π in specific rule forms which allow to have a uniform compilation approach while preserving inferences of the original program. Conversely, the generator program is made of rules defining the domain of each predicate appearing in the propagator program and so it will be used to generate the subset of relevant atoms needed for computing answer sets of Π. Propagator and generator programs are compiled, respectively, into two modules, namely Propagator and Generator module. The resulting solver, namely Π-solver, is obtained by integrating Propagator and Generator modules together with the SAT Solver Glucose.
As reported in Figure 1, at the solving stage, the Π-solver takes as input a program instance (i.e., a set of facts) and starts by generating ground atoms appearing in the propagator program, by means of the Generator module. Generated atoms are fed into the Glucose SAT solver which starts the CDCL from an empty interpretation . During the CDCL, as soon as a literal is added to , the SAT solver notifies the Propagator which computes new inferences (if any). By proceeding in this way, the SAT solver stops if becomes total, and so is an answer set, or consistency cannot be restored and so Π ∪ does not have any answer set.
Empirical evaluations [41, 42, 43] show that compiled solvers allow to efectively tackle the grounding bottleneck problem by allowing to solve instances that were out-of-reach for standard systems while remaining competitive on problems that do not present grounding issues. However, as it has been pointed out by Dodaro et al. (2023), compiled solvers sufer whenever the number of (auxiliary) atoms obtained in the generation phase increases. In these cases, compiled solvers require a lot of computational resources, even more than standard ones.
To reduce the number of atoms that are generated upfront by proasp, we propose a novel compilationbased technique that postpones the evaluation of problematic rules (i.e., rules generating a large number of atoms) to the solving phase. To present our approach we first introduce the notion of lazy program split which identifies the syntactic restrictions under which rules can be compiled with lazy atom generation.
Definition 1 (Lazy Program Split). Let Π be a program and ⊆ Π . Then is a lazy program split for Π if is stratified and ℎ() ∩ ℎ(Π ∖ ) = ∅.
Intuitively, a lazy program split is a stratified subprogram ⊆ Π such that predicates in the head of some rule in do not appear in the head of any rule of Π ∖ . Stratification is required to ensure that only deterministic inferences can be derived from . The second condition instead allows to separate the evaluation of from the standard proasp pipeline.
To evaluate a program Π, state-of-the-art ASP solvers transform rules in (Π) by applying the well-known Clark’s completion [47]. By means of this transformation, solvers are able to compute supported models by leveraging unit propagation of program clauses. However, this transformation may generate a large number of clauses and requires ground rules to be materialized, which is detrimental when the program is grounding intensive. To avoid such transformation for rules in a lazy program split , it is possible to leverage the Fitting operator [48]. Such an operator guarantees that rules in () are satisfied and that each positive literal in an answer set is supported. Definition 2 (Fitting 1985). is defined as:
Given a program Π and a (partial) interpretation I, the Fitting operator ΦΠ • ΦΠ() = Π() ∪ Π() • Π() = {() | ∈ (Π) ∧ |= ()} • Π() = { ∈ Π | ∀ ∈ (Π) .. () = , ̸|= ()}.
Intuitively, given an interpretation , the operator Π() derives the head of each rule in (Π) having a true body w.r.t. . In this way rules in Π are satisfied and atoms in Π() are supported in Π w.r.t. . On the other hand, Π() derives all those atoms that cannot be supported in Π w.r.t. . Thus, such atoms cannot be true in an answer set of Π that extends .
Based on the aforementioned properties of the Fitting operator, a lazy program split of a program Π can be compiled into ad-hoc propagators, namely Consequence and Support propagators, which mimic, respectively, the application of and on rules in .
More in detail, the Consequence operator is implemented via a bottom-up evaluation that builds instantiations of rules in that have a true body w.r.t. a (partial) interpretation and infers the head of such rules. Conversely, the Support operator is implemented via a top-down evaluation that, given an atom searches for an instantiation of a rule in that () has in the head; and () whose body is not false w.r.t. .
Here we discuss in a more detailed way, how we implemented our techniques on top of the proasp system. To enable lazy atom discovery during solving we extended both the compilation and solving pipelines that are reported in Figures 2 and 3.
Extended Compilation. Let Π be a program and be a lazy program split of Π. Our objective is to compile into ad-hoc propagators that simulate the application of the Fitting operator on rules in . Whereas, the program Π ∖ follows the aforementioned proasp compilation pipeline.
According to the definition of lazy program split, we know that predicates in ℎ() do not appear in the head of any rule of Π ∖ . However, it is important to point out that predicates in ℎ() may appear in the body of some rules in Π ∖ . In this case, proasp propagators require knowledge of the existence of such atoms, and thus, it is required that proasp’s Generator module generates those atoms over predicates in ℎ() appearing in the body of rules of Π ∖ , referred to as interface atoms. To this end, we introduce a rewriting technique which produces the rules needed for generating interface atoms.
Definition 3 (Interface Program). Given a program Π and a lazy program split of Π, then (Π, ) contains, for each ∈ Π ∖ , the following rules: ← () ← () ∀ ∈ ()+ ∀ ∈ ()− where () denotes the conjunction of literals ∈ () such that () ∈ ℎ() and () denotes the conjunction of literals ∈ () such that () ∈ ℎ(Π ∖ ). Example 4.1. Let Π be the following program:
() ← (), ∼ () () ← (), ∼ ()
() ← (), ∼ () () ← (), ∼ () (, ) ← (), ( )
← (1, ), ( ) Let = {(, ) ← (), ( )} then is a lazy program split for Π, since it is stratified and does not appear in the head of any rule of Π ∖ . In this case the interface program (Π, ) contains only the rule (1, ) ← ( ), which is obtained from the constraint ← (1, ), ( ).
However, there could be cases in which rules of the interface program are unsafe. If in program Π from Example 4.1 we add the rule ← (, ), ( ) to Π, then (Π, ) contains also the rule (, ) ← ( ) which is unsafe since variable appears only in the head of the rule. To avoid these cases, we restrict our approach to programs that satisfy a stronger notion of safety, namely lazy safety. Definition 4 (Lazy Safety). Given a program Π and a split , Π is lazy safe if for each rule ∈ Π ( ()) ⊆ ( ()+), where () denotes the conjunction of literals ∈ () such that () ∈ ℎ() and () denotes the conjunction of literals such that () ∈ ℎ(Π ∖ ). Intuitively, lazy safety requires that atoms over predicate in ℎ() are bounded by variables appearing in positive literals not in ℎ(Π ∖ ). If a program is lazy safe then the interface program, (Π, ) only contains safe rules. Note that, this restriction does not introduce any loss of generality since it is possible to use an auxiliary predicate that gives bound to unsafe variables by considering all possible constants in the Herbrand universe. However, this is not ideal since the Generator will produce more atoms than the ones produced by standard grounders such as gringo [49] and i-dlv [50] that perform an intelligent bottom-up grounding.
We are now ready to discuss the extended proasp’s compilation pipeline reported in Figure 2.
Given a program Π, and a lazy program split , the Rewriter module rewrites all the rules in Π ∖ by following the standard proasp methodology [43]. Thus, it produces as output the generator and the propagator program, while rules in remain in their original form.
At this point, the generator program obtained by proasp does not contain any rule defining interface atoms, and this is an issue since such atoms, as it has been previously pointed out, may appear in the body of some rule in Π ∖ . In this case the proasp solver may erroneously consider interface atoms as false whereas they could be discovered lazily during solving.
To this end, the Split Rewriter computes (Π, ) which will be used to generate ad-hoc generator procedures, nested into the Generator module, that are able to produce the interface atoms.
At this point, each ∈ is ready to be compiled into ad-hoc post-propagators which simulate the application of both and operators on the rule . In the following section we report an example of compiled propagators which will clarify how compiled post-propagators work. As a result of the compilation of , we obtain two modules, namely Consequence and Support which will be integrated in the compiled solver for postponing the evaluation of the lazy program split .
Extended Solving. The architecture of the resulting proasp solver is depicted in Figure 3. At the solving stage, the compiled solver takes as input a program instance , that is a set of facts, and the generator module produces the subset of relevant atoms that appear in the propagator program. Among atoms generated by the generator module, we need to distinguish between those over predicates in ℎ(Π ∖ ) and those over predicates in ℎ() (i.e., the interface atoms). Atoms whose predicate is in ℎ(Π ∖ ) are entirely handled by the SAT solver and the propagator module. Conversely, the truth value of atoms whose predicate is in ℎ() must be determined through the Consequence and Support modules. Among possible atoms over predicates in ℎ(), only the interface atoms have been generated while the remaining one are unknown to the solver. Since interface atoms are indeed solver’s decision variables then the solver can decide their truth value; while unknown ones can only be discovered by post-propagators during solving. To guarantee that solver choices are consistent with rules in , at each post-propagator call, the SAT solver uses the Consequence module for deriving both interface and unknown atoms as true. In particular, interface atoms will be assigned into the SAT solver, while unknown atoms are lazily discovered and added to the current interpretation. Unknown atoms that are never derived by the Consequence module can be inferred as false. Note that, in this setting, false atoms can only be derived after that all solver’s decision variables have been assigned to a truth value. Even though this approach guarantees correctness, it is not applicable in practice, since lazy program splits may contain negation and so we may propagate atoms too late during solving. To anticipate such propagations, when some unknown atoms are encountered during bottom-up evaluation of the Consequence module, the Support module is leveraged to infer false unknown atoms. On the other hand, to infer false interface atoms the SAT solver calls Support module at each post-propagator call. As soon as atoms derived either from Consequence or Support module were already assigned by the solver to a diferent truth value (i.e., we obtained an inconsistent interpretation), a conflict is generated. Such a conflict is handled by the SAT solver which resolves it, if possible, by analyzing the literals that derived conflictual literals (i.e., reasons of the propagations). If the conflict can be resolved then the solving restarts up to a total and consistent interpretation is constructed (i.e., an answer set is found) or the incoherence of the program is proved.
In this section we provide an example of compilation of lazy program split into post-propagators. Recall that post-propagators are lower priority propagators that are used in ASP systems to perform additional checks required by stable model semantics [51]. Consider the following program Π: () ← (), ∼ (). () ← (), ∼ ().
() ← (), ∼ ().
() ← (), ∼ (). (, ) ← (), ( ).
← (, 1), ().
In this case, the rule (, ) ← (), ( ) is itself the lazy program split. Thus, we consider = {(, ) ← (), ( )} as the subprogram whose evaluation should be postponed and Π ∖ as the subprogram, made of remaining rules of Π, that follows the standard proasp approach. We now describe how the compiled solver is obtained. As first step of the compilation stage, the compiler takes as input the program Π where rules in are labeled as lazy program split. The rewriting process transforms program Π ∖ into the corresponding Generator and Propagator programs. Note that the generator program is augmented with generation rules in (Π, ). In this case, the predicate appears only in the constraint ← (, 1), () and so the only rule in (Π, ) is (, 1) ← () . At this point, we are ready to compile generator and propagator programs, as well as the lazy program split . The former are compiled into Generator and Propagator modules while the latter is compiled into Consequence and Support modules. More precisely, since only contains the rule (, ) ← (), ( ) then the Consequence module only contains the compiled procedure reported in Algorithm 3. Analogously, the Support module only contains the compiled procedure reported in Algorithm 4. At this point, the compiled solver is obtained by integrating together compiled modules and the Glucose SAT solver.
We are now ready to describe how a program instance is solved by the compiled solver. Let
= {(
Input : An atom , an interpretation , a set of literal
1 begin
2 if pred() = “b”
3 := [0]
4 := [1]
5 if ∼ () ∈/
6 if ∼ () ∈/
7 return ⊥
8 else := ∪ {()}
9 else := ∪ {()}
10 return ⊤
atoms needed to compute an answer set of Π ∪ , that are:
⎧ (
Note that only a part of the domain of predicate is generated. More precisely, only the relevant part that appears in the constraint ← (, 1), ().
Generated atoms in become decision variables of the SAT solver, which starts the CDCL to build an answer set of Π ∪ starting from an empty interpretation .
As first step, the SAT solver adds to and then makes the first heuristic choice. Let us suppose that
the SAT solver chooses (
For measuring the impact of lazy atom discovery on proasp performance, we conducted an empirical evaluation over synthetic benchmarks that were considered by Dodaro et al. (2023) for highlighting strengths and weaknesses of the compiled solver.
The first benchmark we considered is Synth1 on which compilation-based solvers showed significant overhead. More precisely, the compiled program in this benchmark is the following: 1 : 1(, , , ) : −(), ( ), (), ( ), 1(, , , ) 2 : 1(, , , ) : −(), ( ), (), ( ), 1(, , , ) 3 : 2(, , , ) : −(), ( ), (), ( ), 2(, , , ) 4 : 2(, , , ) : −(), ( ), (), ( ), 2(, , , ) 5 : (, , ) : − 1(, _, _, ), 2(, _, _, ) 6 : (, , ) : − 1(, _, _, ), 2(, _, _, ) 7 : : −( 1, , ), (, , 2) Synth1 is made of two four-arity predicates guesses, two rules that compute a join over the guessed predicates and one constraint for trashing a portion of the guessed models. For this benchmark we consider a lazy program split that contains rules 5, 6 and 7. By compiling such a split with our technique into post-propagators, we are able to lazily generate atoms for predicates and . The corresponding version of proasp without lazy atom discovery is forced to generate all and atoms plus the auxiliary atoms produced by the proasp rewriting described in [42].
Conversely, the second benchmark we considered is Synth2 on which compilation resulted to be very efective. The program considered in Synth2 benchmark is the following: 1 : 1(, ) : −(), ( ), 1(, ) 2 : 1(, ) : −(), ( ), 1(, ) . . . 11 : 6(, ) : −(), ( ), 6(, ) 12 : 6(, ) : −(), ( ), 6(, ) 13 : (1, . . . , 7) : − 1(1, 2), 2(2, 3), . . . , 6(6, 7) 14 : (1, . . . , 7) : − 1(1, 2), 2(2, 3), . . . , 6(6, 7) 15 : : −(_, _, _, , , , ), (, , , , _, _, _) As it can be observed, it has a structure that is similar to Synth1, except that this time there is a guess over six two-arity predicates. Also for this benchmark we consider a split which consists of the two rules that define a join over the result of the guessed predicated (namely 13 and 14) and the constraint clingo wasp proasp proasp-postP
2 4 6
Number of solved instances (b) Synth1: Execution Time 600 clingo wasp proasp proasp-postP 8 8 ) 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 12 clingo wasp proasp proasp-postP 8 8 2 4 6 Number of solved instances 2 4 6 Number of solved instances (c) Synth2: Memory Usage (d) Synth2: Execution Time that trashes part of the guessed models. Just like the previous benchmark, the version of proasp with post-propagators able to lazily generate atoms of predicates and . All the 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 performance. In particular, the introduction of lazy atom discovery in the synth2 benchmark allowed to improve already good results obtained by proasp by allowing lazy generation of atoms for predicates and . Concerning Synth1 instead, we can see that the version of proasp with lazy atom discovery was capable not only to improve proasp performance, but to make the system achieve better results w.r.t. Ground & Solve systems that were winners for the benchmark. This is due to two reasons: the first is that atoms for predicates and were lazily generated, and the second is that the compilation of rules defining and into post-propagator allowed to avoid the proasp rewriting that introduces auxiliary atoms.
Tackling the grounding bottleneck in ASP evaluation is a crucial problem which inspired a significant body of literature. Existing proposals tackled the grounding problem in diferent ways and each one present its strengths and limitations. Hybrid formalisms, such as Constraints Answer Set Programming (CASP) [52, 31, 53, 30, 32], ASP Modulo Theories [25], and HEX programs [54], integrate ASP systems with external sources of computation in order to shift the problem out of the ASP systems realm. Conversely, Lazy grounding systems [33, 34, 35, 36, 37], materialize ground rules only when their body is satisfied during solving. Albeit promising, these systems follow a novel solving strategy that still does not match the performance of state-of-the-art systems [55]. The techniques presented in this paper, instead, keeps the well-matured CDCL approach at solving stage but shifts the evaluation of program splits without materializing ground rules.
Complexity-driven program rewritings [38, 56] tackle the grounding bottleneck by translating programs into diferent formalisms, such as propositional epistemic logic programs, or into disjunctive programs. Such translation can be exponential in the worst case but the obtained programs feature smaller ground instantiations.
Compilation-based approaches [39, 40, 41, 42], are at the core of the technique presented in this paper. These approaches mitigate the grounding bottleneck by translating non-ground rules into specialized procedures that simulate inferences avoiding (entirely) the grounding phase [41, 42, 43]. As it has already been discussed in previous sections, these techniques present some overhead when the number of generated atoms increases, but by enabling lazy atom discovery, it is possible to reduce such overhead.
ASP systems based on the Ground & Solve approach are afected by the Grounding Bottleneck. In the last years, proposed compilation-based ASP solvers were able to efectively address this issue. However, existing compilation-based systems still require the upfront materialization of ground atoms, which can be detrimental in certain cases, as noted by [42]. In this work, we describe how to extend the compilation-based technique to avoid the generation of all atoms in advance. We implemented this idea on top of proasp. Achieved results showed substantial performance gains. As future work, we plan to extend our technique and experiments, and also to study how to support recursive programs that at the moment cannot be handled by proasp.
This work was supported by the Italian Ministry of Industrial Development (MISE) under project EITWIN n. F/310168/05/X56 CUP B29J24000680005; and by the Italian Ministry of Research (MUR) under projects: PNRR FAIR - Spoke 9 - WP 9.1 CUP H23C22000860006, and Tech4You CUP H23C22000370006.
The author(s) have not employed any Generative AI tools. [55] A. Weinzierl, R. Taupe, G. Friedrich, Advancing lazy-grounding ASP solving techniques - restarts, phase saving, heuristics, and more, Theory Pract. Log. Program. 20 (2020) 609–624. [56] 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.