Compilation-based Techniques for Evaluating Normal Logic Programs Under the Well-founded Semantics Andrea Cuteri, Giuseppe Mazzotta and Francesco Ricca University of Calabria, Rende 87036, Italy Abstract Recent studies have demonstrated that compilation-based techniques can be beneficial for evaluating Datalog and ASP programs. In this paper, we develop a compiler that is able to generate solvers for normal logic programs under the well-founded semantics. The proposed system has been evaluated on different settings and preliminary results highlight significant improvements in the evaluation of non-stratified programs. Keywords Logic Programming, Well-founded semantics, Compilation 1. Introduction Logic programming is a declarative programming paradigm that can be used to model complex problems in terms of logical implications [1]. Logic programs are often evaluated by means of general-purpose systems that implement a given semantics [2, 3]. The need for handling with the same algorithm any possible input, in some cases, makes it impossible to apply specific optimizations that would work only for a subclass of programs. Thus, considerable speedups can be obtained by using ad-hoc evaluation procedures for the program in input. Following this consideration, compilation-based techniques have been recently proposed to speed up the evaluation of Datalog [4] and Answer Set Programming (ASP) [5, 6]. In particular, the idea behind this approach is to compile the input program into a custom system that is optimized by exploiting the syntactic properties of the modeled program and can be used for evaluating different instances of the compiled program. Concerning Datalog, the system soufflΓ© [4] was demonstrated to be very effective, especially for solving tasks connected with software develop- ment, but also other prototypical systems were revealed to be very promising [7]. Concerning ASP, compilation techniques have been successfully employed for the evaluation of grounding- intensive ASP programs outperforming state-of-the-art ASP solvers [6, 8] and reducing both time and memory consumption. However, none of the aforementioned systems support the well-known well-founded semantics [9] when no restriction is posed on the usage of negation. In this paper, we propose a compilation-based technique for evaluating normal logic programs under the well-founded semantics and present a system that is able to generate ad-hoc solvers for programs. CILC’23: 38th Italian Conference on Computational Logic, June 21–23, 2023, Udine, Italy $ cuteri.andrea@gmail.com (A. Cuteri); giuseppe.mazzotta@unical.it (G. Mazzotta); ricca@mat.unical.it (F. Ricca) Β© 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) An empirical evaluation of the proposed approach has been conducted on hard bench- marks [10, 11]. Obtained results demonstrate that the proposed approach is competitive with existing implementations capable of evaluating both Datalog programs (i.e. positive programs) and program with negation. Notably, our approach outperforms dlv2 [12] on normal logic programs with not-stratified negation. 2. Logic Programs Under the Well-founded Semantics In this section, some preliminaries are provided on normal logic programs under the well- founded semantics [9]. 2.1. Syntax A term is a constant or a variable. Constants are strings starting with lowercase letter or integers instead variables are terms starting with uppercase letter. An atom π‘Ž is an expression of the form 𝑝(𝑑1 , ..., 𝑑𝑛 ) where 𝑝 is a predicate of arity 𝑛 and 𝑑1 , ..., 𝑑𝑛 are terms. If all the terms are constants then π‘Ž is a ground atom. A literal is an atom π‘Ž, or its negation π‘›π‘œπ‘‘ π‘Ž where π‘›π‘œπ‘‘ represents default negation. A literal is positive if it is of the form π‘Ž, negative otherwise. Given a literal 𝑙, the com- plement of 𝑙, denoted by 𝑙, is π‘Ž if 𝑙 = π‘›π‘œπ‘‘ π‘Ž, π‘›π‘œπ‘‘ π‘Ž otherwise. A rule π‘Ÿ is an expression of the form: β„Ž ← 𝑏1 , ..., π‘π‘˜ , π‘›π‘œπ‘‘ π‘π‘˜+1 , ..., π‘›π‘œπ‘‘ π‘π‘š . where β„Ž is an atom referred to as head, π»π‘Ÿ , 𝑏1 , ..., π‘›π‘œπ‘‘ π‘π‘š is a conjunction of literals referred to as body of the rule, π΅π‘Ÿ , and π‘š > 0. If π‘š = 0 then π‘Ÿ is a fact. A program Ξ  is a set of rules. Given a set of literals 𝐡, 𝐡 + (resp. 𝐡 βˆ’ ) denotes the set of positive (resp. negative) literals in 𝐡. The dependency graph of a program Ξ , 𝐺Π , is a directed labeled graph where the nodes are predicates appearing in Ξ  and the set of the edges contains a positive (resp. negative) edge (𝑒, 𝑣) if exists a rule 𝑣 ← 𝐡 ∈ Ξ  where 𝑒 appears in 𝐡 + (resp. 𝑒 appears in 𝐡 βˆ’ ). Ξ  is said to be Datalog if it does not contain any negative literals; Datalog with stratified negation if 𝐺Π does not contain cycles with negative edges. 2.2. Well-founded Semantics Given a program Ξ , the Herbrand Universe is the set of constants appearing in Ξ ; the Herbrand Base, 𝐡Π , is the set of possible ground atoms that can be built using predicate in Ξ  and constants in the Herbrand Universe. Given a rule π‘Ÿ ∈ Ξ , π‘”π‘Ÿπ‘œπ‘’π‘›π‘‘(π‘Ÿ) represents all possible instantiations of π‘Ÿ ⋃︀ replacing variables with constants in the Herbrand Universe. Given a program Ξ , π‘”π‘Ÿπ‘œπ‘’π‘›π‘‘(Ξ ) = π‘ŸβˆˆΞ  π‘”π‘Ÿπ‘œπ‘’π‘›π‘‘(π‘Ÿ). An interpretation 𝐼 is a set of literals whose atoms belong to 𝐡Π . 𝐼 is consistent if for each literal 𝑙 ∈ 𝐼, π‘›π‘œπ‘‘ 𝑙 ∈ / 𝐼. 𝐼 is total if for each atom π‘Ž ∈ 𝐡Π either π‘Ž or π‘›π‘œπ‘‘ π‘Ž belongs to 𝐼. Given a consistent interpretation 𝐼, a literal 𝑙 is true (resp. false) w.r.t. 𝐼 if 𝑙 ∈ 𝐼 (resp. π‘›π‘œπ‘‘ 𝑙 ∈ 𝐼). A literal is undefined w.r.t. 𝐼 if it is neither true nor false. A conjunction of literals is true w.r.t. 𝐼 if all the literals are true w.r.t. 𝐼; it is false if at least one literal is false w.r.t. 𝐼; it is undefined otherwise. A set of atoms, π‘ˆΞ  , is an unfounded set w.r.t. 𝐼 if for every atom π‘Ž ∈ π‘ˆΞ  and for every rule π‘Ÿ ∈ π‘”π‘Ÿπ‘œπ‘’π‘›π‘‘(Ξ ) such that π»π‘Ÿ = π‘Ž, π΅π‘Ÿ is false w.r.t. 𝐼 or π΅π‘Ÿ contains some positive literals whose atoms belong to π‘ˆΞ  . Intuitively, all rules defining atoms in π‘ˆΞ  have a false body or depend on atoms in π‘ˆΞ  and so they cannot be inferred as true. The greatest unfounded set, π‘ˆΞ  (𝐼), is the union of possible unfounded sets π‘ˆΞ  . Let 𝑇Π (𝐼) be a transformation defined as the set of atoms π‘Ž such that there exists a rule π‘Ÿ ∈ π‘”π‘Ÿπ‘œπ‘’π‘›π‘‘(Ξ ) where π»π‘Ÿ = π‘Ž and π΅π‘Ÿ is true w.r.t. 𝐼, we define π‘ŠΞ  (𝐼) = 𝑇Π (𝐼) βˆͺ Β¬π‘ˆΞ  (𝐼) where Β¬π‘ˆΞ  (𝐼) = {π‘›π‘œπ‘‘ 𝑙 | 𝑙 ∈ π‘ˆΞ  (𝐼)}. Let 𝐼0 = βˆ…, 𝐼𝛼+1 = π’²πœ‹ (𝐼𝛼 ), with 𝛼 β‰₯ 0, the (partial) well-founded model is defined as π’²πœ‹ = 𝐼𝛽 where 𝛽 β‰₯ 0 is the smallest ordinal such that 𝐼𝛽 = 𝐼𝛽+1 . Basically, π’²πœ‹ is the least fixed point 𝒲𝑃 [9] Algorithm 1 compileProgram Input : A normal program 𝑃 Output : Prints evaluation procedure for 𝑃 1 begin 2 β‰ͺdef π‘π‘œπ‘šπ‘π‘’π‘‘π‘’π‘Š 𝑒𝑙𝑙𝐹 π‘œπ‘’π‘›π‘‘π‘’π‘‘(𝑓 π‘Žπ‘π‘‘π‘ )≫ 3 β‰ͺ 𝐼 = 𝑓 π‘Žπ‘π‘‘π‘ β‰« 4 β‰ͺ ℬ = βˆ…β‰« 5 𝐷𝐺 = π‘π‘œπ‘šπ‘π‘’π‘‘π‘’π·πΊ(𝑃 ) 6 𝑆𝐢𝐢 = π‘π‘œπ‘šπ‘π‘’π‘‘π‘’π‘†πΆπΆ(𝐷𝐺) 7 for all 𝐢 ∈ 𝑆𝐢𝐢 do 8 β‰ͺ𝑑_π‘ π‘‘π‘Žπ‘π‘˜ = 𝐹 = βˆ…β‰« 9 for all π‘Ÿ ∈ π‘π‘œπ‘šπ‘π‘’π‘‘π‘’π‘…π‘’π‘™π‘’π‘ πΉ π‘œπ‘ŸπΆπ‘œπ‘šπ‘π‘œπ‘›π‘’π‘›π‘‘(𝑃, 𝐢) do 10 π‘π‘œπ‘šπ‘π‘–π‘™π‘’π‘…π‘’π‘™π‘’πΉ π‘œπ‘Ÿπ»π‘’π‘Žπ‘‘π·π‘’π‘Ÿπ‘–π‘£π‘Žπ‘‘π‘–π‘œπ‘›(π΅π‘Ÿ , π»π‘Ÿ , 𝐢) 11 β‰ͺ while 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ ΜΈ= βˆ… do≫ 12 β‰ͺ π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ = 𝑑_π‘ π‘‘π‘Žπ‘π‘˜.π‘π‘œπ‘()≫ 13 β‰ͺ switch π‘π‘Ÿπ‘’π‘‘(π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ)≫ 14 for all π‘Ÿ ∈ π‘π‘œπ‘šπ‘π‘’π‘‘π‘’π‘…π‘’π‘π‘’π‘Ÿπ‘ π‘–π‘£π‘’π‘…π‘’π‘™π‘’π‘ (𝑃, 𝐢) do 15 for all 𝑖 ∈ [1, . . . , |π΅π‘Ÿ |] do 16 if π‘π‘Ÿπ‘’π‘‘(π΅π‘Ÿ [𝑖]) ∈ 𝐢 ∧ π΅π‘Ÿ [𝑖] is positive literal then 17 β‰ͺcase Jπ‘π‘Ÿπ‘’π‘‘(π΅π‘Ÿ [𝑖])K ≫ 18 β‰ͺ 𝜎 = πœ–β‰« 19 for all 𝑗 ∈ 1, ..., |π‘‘π‘Ÿπ‘š(π΅π‘Ÿ [𝑖])| do 20 if π‘‘π‘Ÿπ‘š(π΅π‘Ÿ [𝑖])[𝑗] is variable then 21 β‰ͺ 𝜎 = 𝜎 βˆͺ { Jπ‘‘π‘Ÿπ‘š(π΅π‘Ÿ [𝑖])[𝑗]K ↦→ π‘‘π‘Ÿπ‘š(π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ)[ J𝑗K ]}≫ 22 π‘π‘œπ‘šπ‘π‘–π‘™π‘’π‘…π‘’π‘™π‘’πΉ π‘œπ‘Ÿπ»π‘’π‘Žπ‘‘π·π‘’π‘Ÿπ‘–π‘£π‘Žπ‘‘π‘–π‘œπ‘›(π΅π‘Ÿ βˆ– {π΅π‘Ÿ [𝑖]}, π»π‘Ÿ , 𝐢) 23 β‰ͺdone≫ 24 β‰ͺdo≫ 25 β‰ͺ π‘™π‘œπ‘œπ‘ = βŠ₯≫ 26 β‰ͺ for π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ ∈ ℬ do≫ 27 β‰ͺ π‘‘π‘Ÿπ‘’π‘’ = 𝑒𝑛𝑑𝑒𝑓 = βŠ₯≫ 28 β‰ͺ π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ = 𝑠_π‘ π‘‘π‘Žπ‘π‘˜.π‘π‘œπ‘()≫ 29 β‰ͺ switch π‘π‘Ÿπ‘’π‘‘(π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ)≫ 30 π‘π‘œπ‘šπ‘π‘–π‘™π‘’π‘…π‘’π‘™π‘’π‘ πΉ π‘œπ‘Ÿπ‘†π‘’π‘π‘π‘œπ‘Ÿπ‘‘π·π‘’π‘Ÿπ‘–π‘£π‘Žπ‘‘π‘–π‘œπ‘›(π‘π‘œπ‘šπ‘π‘’π‘‘π‘’π‘…π‘’π‘π‘’π‘Ÿπ‘ π‘–π‘£π‘’π‘…π‘’π‘™π‘’π‘ (𝑃, 𝐢), 𝐢) 31 β‰ͺ done≫ 32 β‰ͺwhile π‘™π‘œπ‘œπ‘ == ⊀ ≫ 33 β‰ͺend def ≫ Algorithm 2 compileRuleForHeadDerivation Input : A list of literals 𝐡, an atom π‘Ž, a set of predicates 𝐢 Output : Prints a procedure that instantiates 𝐡 and derives new atoms matching π‘Ž 1 begin 2 π‘π‘œπ‘šπ‘π‘–π‘™π‘’π‘…π‘’π‘™π‘’π΅π‘œπ‘‘π‘¦(𝐡, 𝐢) 3 π‘π‘Ÿπ‘–π‘›π‘‘π»π‘’π‘Žπ‘‘π·π‘’π‘Ÿπ‘–π‘£π‘Žπ‘‘π‘–π‘œπ‘›(𝐡, π‘Ž) 4 for all 𝑖 ∈ [|𝐡|, . . . , 1] do 5 if 𝐡[𝑖] is positive literal then 6 β‰ͺ 𝜎 = 𝜎 J𝑗K ≫ 7 β‰ͺdone≫ 8 else 9 β‰ͺfi≫ 3. Compilation of Well-founded Semantics In this section, we describe the compilation procedure for generating an ad-hoc solver for an input program Ξ . In particular, proposed algorithms (see Algorithms 1-5) describe the compilation of a normal program with not-stratified negation. However, our approach is also able to generate simplified code for the case of Datalog programs with stratified negation that is indeed a particular case. Reported algorithms follow the syntactic convention used in [8]. To recall, the code enclosed between β‰ͺ≫ is printed by the compiler as it is. Instead, the code enclosed in JK , is first substituted with its run-time value and then is printed. For example, let π΅π‘Ÿ [𝑖] = π‘Ž(𝑋), Algorithm 1 at line 17 prints β€œcase β€œπ‘Žβ€ :”. Description of the Compilation Algorithms. As the first step, the compiler builds the dependency graph of Ξ  (Alg. 1 lines 5-6) and computes its strongly connected components SCCs, 𝐢1 , ..., 𝐢𝑛 , that give us a topological order of 𝐺Π such that no paths exist from 𝐢𝑗 to 𝐢𝑖 if 𝑖 < 𝑗. By following that order, the compiler produces for each component 𝐢 the code that evaluates the rules defining atoms in 𝐢 (i.e., whose predicate belongs to 𝐢), referred to as 𝑃𝐢 . Then, each rule π‘Ÿ is compiled into a sub-procedure that iterates over possible instantiations of π΅π‘Ÿ that are either true or undefined w.r.t. 𝐼 βˆͺ ℬ and, successively, derives π»π‘Ÿ (Alg. 1 lines 9-10). Such sub-procedures are generated by means of Algorithm 2. Algorithm 2 starts by calling Algorithm 3 that prints different nested join loops or if statements for each literal in π΅π‘Ÿ . These nested blocks implement iterations over possible rule instantiations (Alg. 3 lines 3-13). Inside the deepest block, the code that collects negative dependencies within the component 𝐢 into the set 𝑛𝑠 is printed (Alg. 3 lines 15-19). Then Algorithm 2 prints the code that derives new atoms matching π»π‘Ÿ by calling Algorithm 4. In particular, the code generated by Algorithm 4 checks if the current body (i.e. 𝑑1 , Β· Β· Β· , 𝑑𝑛 ) is true w.r.t. 𝐼 βˆͺ ℬ. In particular, if all positive literals belong to 𝐼, no negative literals are undefined (i.e. Β¬π‘βˆ’ ∩ ℬ), and no negative literals in the same component occur in the current body (i.e. 𝑛𝑠 = βˆ…), then all literals 𝑑1 , Β· Β· Β· , 𝑑𝑛 are true w.r.t. 𝐼. Thus, if it is the case then the head of the rule is derived as true, otherwise it is derived as undefined (code generated by lines 5 and 10 of Alg. 4). In both cases, derived atoms are collected into the derivation stack in order to be used in the second derivation phase. As the last step, for each literal 𝑙 ∈ π΅π‘Ÿ , if 𝑙 is a positive literal then a nested for-loop is closed by restoring the variable substitution 𝜎 (Alg. 2 lines 5-7). Otherwise, an if-statement scope is closed (Alg. 2 lines 8-9). The second derivation scenario is generated by looking at recursive rules defining atoms whose predicate belongs to 𝐢. In this case, the generated procedure will consume literals collected into 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ and, for each of them, different sub-procedures are executed according to the predicate name of the consumed literal (Alg. 1 lines 11-13). In particular, the compiler, for each rule π‘Ÿ, generates different switch-cases for each literal 𝑙 ∈ π΅π‘Ÿ+ whose predicate belongs to 𝐢 (Alg. 1 lines 15-22). Inside each case, a sub-procedure that evaluates π‘Ÿ starting from a literal, π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ, that matches 𝑙 is generated. Each sub-procedure starts with the initialization of a variable substitution 𝜎 from variables in 𝑙 to constant in π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ (Alg. 1 lines 18-21) and then contains the code that evaluates the remaining part of π΅π‘Ÿ , generated by Algorithm 2. In this way, the generated procedure is able to simulate a semi-naive evaluation of recursive rules. Out of the while-loop scope, the compiler generates the code that derives, if it is possible, undefined atoms either as true or false (Alg. 1 lines 24-32). At this point, atoms in 𝐡Π with predicates in 𝐢 that do not belong to 𝐼 βˆͺ 𝐡 are considered false since no rule instantiations that can derive them exists. Thus, the generated procedure, in this case, will iterate until some undefined atoms (i.e. atoms belonging to ℬ) are derived either as true or false. For each iteration, the generated procedure evaluates possible rules defining remaining atoms in ℬ and so different switch-cases, one for each recursive rule π‘Ÿ, are generated. Each case contains the procedure that evaluates a rule π‘Ÿ starting from an undefined atom π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ that can be substituted to π»π‘Ÿ . These sub-procedures are generated by Algorithm 5 that, for each switch-case, prints the code that initializes a variable substitution 𝜎 from variables in π»π‘Ÿ to constants in π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ (Alg. 5 Algorithm 3 compileRuleBody Input : A list of literals 𝐡, a set of predicate 𝐢 Output : Prints the instantiation procedure for the rule body 𝐡 1 begin 2 β‰ͺ𝜎 = πœ– ≫ 3 for all 𝑗 ∈ 1, ..., |𝐡| do 4 β‰ͺ𝜎 J𝑗K = 𝜎 ≫ 5 if 𝐡[𝑗] is a positive literal then 6 β‰ͺ𝑇 J𝑗K = {𝑝 ∈ (𝐼 βˆͺ ℬ) | π‘šπ‘Žπ‘‘π‘β„Ž(𝜎( J𝐡[𝑗]K ), 𝑝)}≫ 7 β‰ͺfor all 𝑑 J𝑗K ∈ 𝑇 J𝑗K do≫ 8 for all π‘˜ ∈ 1, ..., |π‘‘π‘Ÿπ‘š(𝐡[𝑗])| do 9 if π‘‘π‘Ÿπ‘š(𝐡[𝑗])[π‘˜] is variable then 10 β‰ͺ𝜎 = 𝜎 βˆͺ { Jπ‘‘π‘Ÿπ‘š(𝐡[𝑗])[π‘˜]K ↦→ π‘‘π‘Ÿπ‘š(𝑑 J𝑗K )[ Jπ‘˜K ]}≫ 11 else 12 β‰ͺ𝑑 J𝑗K = 𝜎( J𝐡[𝑗]K )≫ 13 β‰ͺif 𝑑 J𝑗K ∈ / 𝐼 then≫ 14 β‰ͺ𝑏 = βˆ…β‰« 15 β‰ͺ𝑛𝑠 = βˆ…β‰« 16 for all 𝑗 ∈ 1, ..., |𝐡| do 17 β‰ͺ𝑏 = 𝑏 βˆͺ {𝑑 J𝑗K }≫ 18 if 𝐡[𝑗] is a negative literal ∧ π‘π‘Ÿπ‘’π‘‘(𝐡[𝑗]) ∈ 𝐢 then 19 β‰ͺ𝑛𝑠 = 𝑛𝑠 βˆͺ {𝑑 J𝑗K }≫ Algorithm 4 printHeadDerivation Input : An atom π‘Ž Output : Prints the derivation procedure for new atoms matching π‘Ž 1 begin 2 β‰ͺβ„Ž = 𝜎( Jπ‘ŽK )≫ + βˆ’ 3 β‰ͺif 𝑛𝑠 == βˆ… ∧ 𝑏 βŠ† 𝐼 ∧ (¬𝑏 ∩ ℬ) == βˆ… then≫ 4 β‰ͺ 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ = 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ βˆͺ {β„Ž}≫ 5 β‰ͺ 𝐼 = 𝐼 βˆͺ {β„Ž}≫ 6 β‰ͺ ℬ = ℬ βˆ– {β„Ž}≫ 7 β‰ͺelse≫ 8 β‰ͺ if β„Ž ∈ / (𝐼 βˆͺ ℬ)≫ 9 β‰ͺ 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ = 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ βˆͺ {β„Ž}≫ 10 β‰ͺ ℬ = ℬ βˆͺ {β„Ž}≫ 11 β‰ͺ fi≫ 12 β‰ͺfi≫ lines 4-7) and then prints the nested block needed for evaluating π΅π‘Ÿ by means of Algorithm 3. Then, inside the last nested level, the code for head derivation is generated (Alg. 5 lines 9-16). If the conjunction 𝑑1 , Β· Β· Β· , 𝑑𝑛 , with 𝑛 = |π΅π‘Ÿ |, is true w.r.t. 𝐼 βˆͺ ℬ (i.e. all positive literals are in 𝐼 and all atoms appearing in some negative literals are not in ℬ, Alg. 5 line 10) then π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ is derived as true, otherwise a flag variable stating that a ground rule with π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ as head and an undefined body w.r.t. 𝐼 βˆͺ ℬ exists is enabled (Alg. 5 line 15). Then, nested blocks’ scopes are closed (Alg. 5 lines 17-22). After evaluating all switch-cases, if neither π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ has not been derived as true nor the 𝑒𝑛𝑑𝑒𝑓 flag is true then π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ is derived as false (Alg. 5 lines 23-27). Example of Compilation. In order to help understanding the outcome of our compiler, an example is described in the following. Consider the following program Ξ : π‘Ÿ1 : π‘Ž(π‘Œ ) ← 𝑏(𝑋, π‘Œ ), 𝑐(π‘Œ, 𝑍), π‘›π‘œπ‘‘ 𝑑(𝑍) π‘Ÿ2 : π‘Ž(𝑋) ← 𝑓 (𝑋), π‘›π‘œπ‘‘ 𝑔(𝑋) π‘Ÿ3 : 𝑔(𝑋) ← 𝑒(𝑋), π‘›π‘œπ‘‘ π‘Ž(𝑋) The SCCs of 𝐺Π are 𝐢0 = {𝑏}, 𝐢1 = {𝑐}, 𝐢2 = {𝑑}, 𝐢3 = {𝑓 }, 𝐢4 = {𝑒}, 𝐢5 = {π‘Ž, 𝑔}. Since for components 𝐢𝑖 , with 𝑖 from 0 to 4, there are no rules the code produced for them is empty and so let us focus on 𝐢5 . In this case, 𝑃𝐢5 is the entire program so Algorithm 1 prints a sub-procedure for each rule of Ξ . Algorithm 6 reports the code produced by Algorithm 2 for rule π‘Ÿ1. For evaluating π΅π‘Ÿ1 , Algorithm 3 generates an external for-loop that iterates over ground literals 𝑑1 that are not false w.r.t. 𝐼 βˆͺ ℬ and match 𝑏(𝑋, π‘Œ ) (Alg. 6 lines 4-35). For every 𝑑1 , the variable substitution 𝜎 is updated mapping 𝑋 and π‘Œ to the first and the second term of 𝑑1 respectively (Alg. 6 lines 6-7). Nested into this for-loop, another for-loop is printed to iterate over ground literals 𝑑2 matching 𝜎(𝑐(π‘Œ, 𝑍)) (Alg. 6 lines 9-33). Note that the application of 𝜎 to a literal will replace mapped variables with the value they are mapped to (i.e. π‘Œ ↦→ 1 then 𝜎(𝑐(π‘Œ, 𝑍)) = 𝑐(1, 𝑍)). Inside this for-loop 𝜎 is updated by mapping 𝑍 to the second term of 𝑑2 (Alg. 6 lines 11-12). Then, the last literal to evaluate is π‘›π‘œπ‘‘ 𝑑(𝑍) and so, since the value of 𝑍 is already fixed by 𝑑2 then, the last nested block is an if-statement that checks whether Algorithm 5 compileRulesForSupportDerivation Input : A set of rules π‘Ÿπ‘’π‘π‘’π‘Ÿπ‘ π‘–π‘£π‘’π‘…π‘’π‘™π‘’π‘ , a set of predicates 𝐢 Output : Prints a procedure that search for rule body that can support a given atom 1 begin 2 for all π‘Ÿ ∈ π‘Ÿπ‘’π‘π‘’π‘Ÿπ‘ π‘–π‘£π‘’π‘…π‘’π‘™π‘’π‘  do 3 β‰ͺ case Jπ‘π‘Ÿπ‘’π‘‘(π»π‘Ÿ )K ≫ 4 β‰ͺ 𝜎 = πœ–β‰« 5 for all 𝑗 ∈ 1, ..., |π‘‘π‘Ÿπ‘š(π»π‘Ÿ )| do 6 if π‘‘π‘Ÿπ‘š(π»π‘Ÿ )[𝑗] is variable then 7 β‰ͺ 𝜎 = 𝜎 βˆͺ { Jπ‘‘π‘Ÿπ‘š(π»π‘Ÿ )[𝑗]K ↦→ π‘‘π‘Ÿπ‘š(π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ)[ J𝑗K ]}≫ 8 π‘π‘œπ‘šπ‘π‘–π‘™π‘’π‘…π‘’π‘™π‘’π΅π‘œπ‘‘π‘¦(π΅π‘Ÿ , 𝐢) 9 β‰ͺ β„Ž = 𝜎( Jπ‘ŽK )≫ 10 β‰ͺ if 𝑏+ βŠ† 𝐼 ∧ (Β¬π‘βˆ’ ∩ ℬ) = βˆ… ∧ β„Ž ∈ / 𝐼 then≫ 11 β‰ͺ 𝐼 = 𝐼 βˆͺ {β„Ž}≫ 12 β‰ͺ ℬ = ℬ βˆ– {β„Ž}≫ 13 β‰ͺ π‘‘π‘Ÿπ‘’π‘’ = π‘™π‘œπ‘œπ‘ = βŠ€β‰« 14 β‰ͺ else if ((𝑏+ βˆͺ Β¬π‘βˆ’ ) ∩ ℬ) ΜΈ= βˆ… ∧ β„Ž ∈ / 𝐼 then≫ 15 β‰ͺ 𝑒𝑛𝑑𝑒𝑓 = βŠ€β‰« 16 β‰ͺ fi≫ 17 for all 𝑖 ∈ [|π΅π‘Ÿ |, . . . , 1] do 18 if π΅π‘Ÿ [𝑖] is positive literal then 19 β‰ͺ 𝜎 = 𝜎 J𝑗K ≫ 20 β‰ͺdone≫ 21 else 22 β‰ͺfi≫ 23 β‰ͺ if 𝑒𝑛𝑑𝑒𝑓 = βŠ₯ ∧ π‘‘π‘Ÿπ‘’π‘’ = βŠ₯ then≫ 24 β‰ͺ ℬ = ℬ βˆ– {π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ}≫ 25 β‰ͺ 𝐹 = 𝐹 βˆͺ {π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ}≫ 26 β‰ͺ π‘™π‘œπ‘œπ‘ = βŠ€β‰« 27 β‰ͺ fi≫ 𝑑3 = 𝜎(𝑑(𝑍)) is not true w.r.t. 𝐼 (Alg. 6 lines 14-31). At this point the conjunction 𝑑1 , 𝑑2 , 𝑑3 is an instantiation of π΅π‘Ÿ and the generated code should derive the π‘Ž(π‘Œ ) (Alg. 6 lines 20-30). Thus, if the body is true w.r.t. 𝐼 βˆͺ ℬ then β„Ž = 𝜎(π‘Ž(π‘Œ )) is added to 𝐼, otherwise it is added to ℬ. Then, Algorithm 1 produces other two analogues procedures also for π‘Ÿ2 and π‘Ÿ3. Since in this case, recursive rules are π‘Ÿ2 and π‘Ÿ3, but no positive literals have predicates in 𝐢5 then no switch-cases are generated at all and so the while-loop over 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ can be omitted. Thus, Algorithm 1 continues by printing the last derivation scenario as previously described. In particular, Algorithm 7 reports the switch-cases generated by Algorithm 5 for rules π‘Ÿ2 and π‘Ÿ3 w.r.t. the component 𝐢5 . The first switch-case refers to rule π‘Ÿ2 (Alg. 7 lines 2-24) and so it contains the code for evaluating π‘Ÿ2 starting from a literal matching the π‘Ž(𝑋). Thus, 𝜎 is initialized by mapping 𝑋 to the first term of π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ literal (Alg. 7 lines 3-4), and then the nested blocks are generated according to π΅π‘Ÿ2 (Alg. 7 lines 5-13). Inside the last block, the head derivation code has been printed (Alg. 7 lines 14-21). If the body instantiation 𝑑1 , 𝑑2 is true w.r.t. 𝐼 βˆͺ ℬ then β„Ž = π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ is derived as true, otherwise the 𝑒𝑛𝑑𝑒𝑓 flag is enabled. The second switch-case is analogous to the first one but it refers to π‘Ÿ3 and so the evaluation starts from a literal, π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ, matching the atom 𝑏(𝑋). Out of the scope of the switch-statement if no rule in- stantiations have been founded for the atom π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ then it is derived as false (Alg. 7 lines 48-51). Algorithm 6 Output example compileRuleForHeadDerivation Input : {𝑏(𝑋, π‘Œ ), 𝑐(π‘Œ, 𝑍), π‘›π‘œπ‘‘ 𝑑(𝑍)}, π‘Ž(π‘Œ ), {β€² π‘Žβ€² ,β€² 𝑔 β€² } 1 begin 2 𝜎=πœ– 3 𝜎1 = 𝜎 4 𝑇1 = {𝑝 ∈ (𝐼 βˆͺ ℬ) | π‘šπ‘Žπ‘‘π‘β„Ž(𝜎(𝑏(𝑋, π‘Œ )), 𝑝)} 5 for all 𝑑1 ∈ 𝑇1 do 6 𝜎 = 𝜎 βˆͺ {𝑋 ↦→ π‘‘π‘Ÿπ‘š(𝑑1 )[1]} 7 𝜎 = 𝜎 βˆͺ {π‘Œ ↦→ π‘‘π‘Ÿπ‘š(𝑑1 )[2]} 8 𝜎2 = 𝜎 9 𝑇2 = {𝑝 ∈ (𝐼 βˆͺ ℬ) | π‘šπ‘Žπ‘‘π‘β„Ž(𝜎(𝑐(π‘Œ, 𝑍)), 𝑝)} 10 for all 𝑑2 ∈ 𝑇2 do 11 𝜎 = 𝜎 βˆͺ {π‘Œ ↦→ π‘‘π‘Ÿπ‘š(𝑑2 )[1]} 12 𝜎 = 𝜎 βˆͺ {𝑍 ↦→ π‘‘π‘Ÿπ‘š(𝑑2 )[2]} 13 𝜎3 = 𝜎 14 𝑑3 = 𝜎(π‘›π‘œπ‘‘ 𝑑(𝑋)) 15 if 𝑑3 ∈/ 𝐼 then 16 𝑏 = 𝑛𝑠 = βˆ… 17 𝑏 = 𝑏 βˆͺ {𝑑1 } 18 𝑏 = 𝑏 βˆͺ {𝑑2 } 19 𝑏 = 𝑏 βˆͺ {𝑑3 } 20 β„Ž = 𝜎(π‘Ž(π‘Œ )) 21 if 𝑛𝑠 == βˆ… ∧ 𝑏+ βŠ† 𝐼 ∧ (Β¬π‘βˆ’ ∩ ℬ) = βˆ… then 22 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ = 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ βˆͺ {β„Ž} 23 𝐼 = 𝐼 βˆͺ {β„Ž} 24 ℬ = ℬ βˆ– {β„Ž} 25 else 26 if β„Ž ∈ / (𝐼 βˆͺ ℬ) 27 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ = 𝑑_π‘ π‘‘π‘Žπ‘π‘˜ βˆͺ {β„Ž} 28 ℬ = ℬ βˆͺ {β„Ž} 29 fi 30 fi 31 fi 32 𝜎 = 𝜎2 33 done 34 𝜎 = 𝜎1 35 done Algorithm 7 Output example compileRulesForSupportDerivation Input : {𝑔(𝑋) ← 𝑒(𝑋), π‘›π‘œπ‘‘ π‘Ž(𝑋); π‘Ž(𝑋) ← 𝑓 (𝑋), π‘›π‘œπ‘‘ 𝑔(𝑋)}, {β€² π‘Žβ€² ,β€² 𝑔 β€² } 1 begin 2 case ’a’ 3 𝜎=πœ– 4 𝜎 = 𝜎 βˆͺ {𝑋 ↦→ π‘‘π‘Ÿπ‘š(π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ)[1]} 5 𝜎1 = 𝜎 6 𝑇1 = {𝑝 ∈ (𝐼 βˆͺ ℬ) | π‘šπ‘Žπ‘‘π‘β„Ž(𝜎(𝑓 (𝑋)), 𝑝)} 7 for all 𝑑1 ∈ 𝑇1 do 8 𝜎 = 𝜎 βˆͺ {𝑋 ↦→ π‘‘π‘Ÿπ‘š(𝑑1 )[1]} 9 𝑑2 = 𝜎(π‘›π‘œπ‘‘ 𝑔(𝑋)) 10 if 𝑑2 ∈/ 𝐼 then 11 𝑏 = 𝑛𝑠 = βˆ… 12 𝑏 = 𝑏 βˆͺ {𝑑1 } 𝑏 = 𝑏 βˆͺ {𝑑2 } 13 𝑛𝑠 = 𝑛𝑠 βˆͺ {𝑑2 } 14 β„Ž = π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ 15 if 𝑏+ βŠ† 𝐼 ∧ (Β¬π‘βˆ’ ∩ ℬ) = βˆ… ∧ β„Ž ∈ / 𝐼 then 16 𝐼 = 𝐼 βˆͺ {β„Ž} 17 ℬ = ℬ βˆ– {β„Ž} 18 π‘‘π‘Ÿπ‘’π‘’ = π‘™π‘œπ‘œπ‘ = ⊀ 19 else if ((𝑏+ βˆͺ Β¬π‘βˆ’ ) ∩ ℬ) ΜΈ= βˆ… ∧ β„Ž ∈ / 𝐼 then 20 𝑒𝑛𝑑𝑒𝑓 = ⊀ 21 fi 22 fi 23 𝜎 = 𝜎1 24 done 25 case ’g’ 26 𝜎=πœ– 27 𝜎 = 𝜎 βˆͺ {𝑋 ↦→ π‘‘π‘Ÿπ‘š(π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ)[1]} 28 𝜎1 = 𝜎 29 𝑇1 = {𝑝 ∈ (𝐼 βˆͺ ℬ) | π‘šπ‘Žπ‘‘π‘β„Ž(𝜎(𝑒(𝑋)), 𝑝)} 30 for all 𝑑1 ∈ 𝑇1 do 31 𝜎 = 𝜎 βˆͺ {𝑋 ↦→ π‘‘π‘Ÿπ‘š(𝑑1 )[1]} 32 𝑑2 = 𝜎(π‘›π‘œπ‘‘ π‘Ž(𝑋)) 33 if 𝑑2 ∈/ 𝐼 then 34 𝑏 = 𝑛𝑠 = βˆ… 35 𝑏 = 𝑏 βˆͺ {𝑑1 } 𝑏 = 𝑏 βˆͺ {𝑑2 } 36 𝑛𝑠 = 𝑛𝑠 βˆͺ {𝑑2 } 37 β„Ž = π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ 38 if 𝑏+ βŠ† 𝐼 ∧ (Β¬π‘βˆ’ ∩ ℬ) = βˆ… ∧ β„Ž ∈ / 𝐼 then 39 𝐼 = 𝐼 βˆͺ {β„Ž} 40 ℬ = ℬ βˆ– {β„Ž} 41 π‘‘π‘Ÿπ‘’π‘’ = π‘™π‘œπ‘œπ‘ = ⊀ 42 else if ((𝑏+ βˆͺ Β¬π‘βˆ’ ) ∩ ℬ) ΜΈ= βˆ… ∧ β„Ž ∈ / 𝐼 then 43 𝑒𝑛𝑑𝑒𝑓 = ⊀ 44 fi 45 fi 46 𝜎 = 𝜎1 47 done 48 if 𝑒𝑛𝑑𝑒𝑓 = βŠ₯ ∧ π‘‘π‘Ÿπ‘’π‘’ = βŠ₯ then 49 ℬ = ℬ βˆ– {π‘ π‘‘π‘Žπ‘Ÿπ‘‘π‘’π‘Ÿ} 50 π‘™π‘œπ‘œπ‘ = ⊀ 51 fi 4. Implementation and Experiments Implementation Details. The compilation strategy described in the previous section has been entirely implemented in C++ and so both compiler and generated procedures are written in C++. Generated code is built on top of optimized data structures that allow to speed up the whole computation process. In particular, it uses a numerical representation of constant terms that allows a compact and uniform representation. Moreover, different indexing structures are used for each predicate. Indexes are defined on the subset of terms of predicates, for fast retrieval of the list of literals that match a possible tuple. Benchmarks, Systems and Experiments Setup. In order to assess the performances of the proposed approach we conducted an empirical evaluation both on positive programs (i.e., Datalog) and programs with negation. Among positive programs, we considered: β€’ Large-join problem [11] defined as follows: π‘Ž(𝑋, π‘Œ ) ← 𝑏1(𝑋, 𝑍), 𝑏2(𝑍, π‘Œ ). 𝑏1(𝑋, π‘Œ ) ← 𝑐1(𝑋, 𝑍), 𝑐2(𝑍, π‘Œ ). 𝑏2(𝑋, π‘Œ ) ← 𝑐3(𝑋, 𝑍), 𝑐4(𝑍, π‘Œ ). 𝑐1(𝑋, π‘Œ ) ← 𝑑1(𝑋, 𝑍), 𝑑2(𝑍, π‘Œ ). where 𝑑1/2, 𝑑2/2, 𝑐2/2, 𝑐3/2, and 𝑐4/2 are defined as facts that represent an instance of the problem. For this benchmark, we have generated instances of different sizes in a random fashion. More precisely, for each instance, we set the size (number of facts) roughly from 10000 to 10000000 and we randomly divided the number of facts among the previous predicates (around 10-25% for each predicate). Then for each predicate 𝑝, we randomly estimated the max value for each term, 𝑛 and π‘š, in such a way that 𝑛 * π‘š = 𝑠, where 𝑠 is the size of the predicate set of 𝑝. β€’ Reachability problem defined as follows: π‘Ÿπ‘’π‘Žπ‘β„Ž(𝑋, π‘Œ ) ← 𝑒𝑑𝑔𝑒(𝑋, π‘Œ ). π‘Ÿπ‘’π‘Žπ‘β„Ž(𝑋, π‘Œ ) ← π‘Ÿπ‘’π‘Žπ‘β„Ž(𝑋, 𝑍), 𝑒𝑑𝑔𝑒(𝑍, π‘Œ ). Instances of this problem are directed graphs that we have generated varying the number of nodes and the density of the edges. In particular, we considered graphs with a number of nodes from 100 to 2000 and density 20, 40, 60, 80, and 100%. Among programs with negation, instead, we considered three hard benchmarks from asp com- petitions that are Knight Tour with Holes, Stable Marriage, and Graph Colouring [10]. Our approach, labeled wf-comp, was compared with the following tools: β€’ General-purpose systems that can evaluate Datalog programs: idlv [13] and gringo [14] β€’ The soufflΓ© framework [4] for which we have rewritten the encoding to produce a suitable encoding for this framework. In particular, two versions have been considered, the interpreted, souffle, and compiled, souffle-comp, ones. β€’ Compilation-based approach for stratified normal programs wasp-lazy [7]. 1,800 souffle souffle-comp 1,500 gringo idlv Execution Time (s) 1,200 wasp-lazy wf-comp 900 600 300 0 0 10 20 30 40 50 60 Number of solved instances Figure 1: Systems comparison on large-join domain 1,800 souffle souffle-comp 1,500 gringo idlv Execution Time (s) 1,200 wasp-lazy wf-comp 900 600 300 0 0 20 40 60 80 100 Number of solved instances Figure 2: Systems comparison on reachability domain β€’ ASP system dlv2 [12] that can evaluate normal programs under well-founded semantics. All the experiments were executed on a machine equipped with Xeon(R) Gold 5118 CPUs, running Ubuntu Linux (kernel 5.4.0-77-generic). Time and memory were limited to 1800 seconds and 8GB, respectively. Source code and benchmark suite are available at https://osf.io/ g9n2z/?view_only=aeb0777c469e46499247284b56dfb598 Evaluation on Positive Programs. In this comparison, we run the systems on instances of large-join and reachability. Obtained results are summarized by the cactus plots in Figures 1-2. 10 dlv2 wf-comp 8 Execution Time (s) 6 4 2 0 0 50 100 150 200 250 300 350 Number of solved instances Figure 3: Systems comparison on Knight Tour With Holes benchmark 10 dlv2 wf-comp 8 Execution Time (s) 6 4 2 0 0 15 30 45 60 75 Number of solved instances Figure 4: Systems comparison on Stable Marriage benchmark Recall that a cactus plot reports a line for each system and each line contains a point (𝑋, π‘Œ ) if a given system is able to solve 𝑋 within a time limit of π‘Œ seconds. In both cases, wf-comp outperforms state-of-the-art ASP systems gringo and idlv solving more instances (roughly 15 for reachability and 2 for large-join) and in less time overall. Our approach also outperforms wasp-lazy on reachability problem solving 16 more instances than the latter, while wf-comp is comparable on the large-join domain with wasp-lazy. The best method in this comparison is souffle system. The difference with our tool (souffle is preferable in complete graphs) is due to different data structures and also to the different input formats. Indeed, souffle takes as input a numeric format where input facts are organized in files for 35 dlv2 30 wf-comp 25 Execution Time (s) 20 15 10 5 0 0 40 80 120 160 Number of solved instances Figure 5: Systems comparison on Graph Colouring benchmark each input predicate while wf-comp reads plain text files. Evaluation on Programs with Negation. In the case of programs with negation, we com- pare wf-comp and dlv2 (the other methods do not support unrestricted negation). For each considered benchmark we report a cactus plot see Figures 3, 4, and 5. Obtained results highlight the strength of the proposed approach that outperforms dlv2 on considered benchmarks. In particular, both systems are able to solve all problem instances within time and memory limits, but wf-comp significantly reduced the total execution time for each benchmark (33.24% on Graph Colouring, 63.26% on Knight Tour With Holes, and 22.37% on Stable Marriage). 5. Conclusion Logic programming is a widely employed programming paradigm for modeling complex problems in a declarative fashion. Efficient implementations are needed in order to exploit the strength of such formalism in real-world applications. Compilation-based techniques were revealed to be effective in tackling different issues raised in the evaluation of logic pro- grams [4, 7, 6, 8]. In this paper, we proposed a compilation-based approach for logic programs under well-founded semantics. Obtained results demonstrate the effectiveness of the proposed approach both for positive programs and programs with negation. The improvements are significant on programs with negation while in the evaluation of positive programs our imple- mentation is competitive with existing systems. As future works, we planned to extend our technique also to the class of disjunctive programs and to programs with aggregates (again under the well-founded semantics). Also, there is space for improvements in the data structures used for evaluating Datalog programs, where better performance could possibly be achieved (especially on dense graphs) by employing more efficient indexing structures. References [1] J. W. Lloyd, Foundations of Logic Programming, 2nd Edition, Springer, 1987. [2] C. Baral, M. Gelfond, Logic programming and knowledge representation, The Journal of Logic Programming 19 (1994) 73–148. [3] E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov, Complexity and expressive power of logic programming, ACM Comput. Surv. 33 (2001) 374–425. [4] H. Jordan, B. Scholz, P. Subotic, SoufflΓ©: On synthesis of program analyzers, in: S. Chaudhuri, A. Farzan (Eds.), Computer Aided Verification - 28th International Con- ference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, vol- ume 9780 of Lecture Notes in Computer Science, Springer, 2016, pp. 422–430. URL: https: //doi.org/10.1007/978-3-319-41540-6_23. [5] B. Cuteri, C. Dodaro, F. Ricca, P. SchΓΌller, Partial compilation of ASP programs, Theory Pract. Log. Program. 19 (2019) 857–873. URL: https://doi.org/10.1017/S1471068419000231. [6] B. Cuteri, C. Dodaro, F. Ricca, P. SchΓΌller, Overcoming the grounding bottleneck due to constraints in ASP solving: Constraints become propagators, in: C. Bessiere (Ed.), Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, ijcai.org, 2020, pp. 1688–1694. URL: https://doi.org/10.24963/ijcai.2020/234. [7] B. Cuteri, F. Ricca, A compiler for stratified datalog programs: preliminary results, in: S. Flesca, S. Greco, E. Masciari, D. SaccΓ  (Eds.), Proceedings of the 25th Italian Symposium on Advanced Database Systems, Squillace Lido (Catanzaro), Italy, June 25-29, 2017, volume 2037 of CEUR Workshop Proceedings, CEUR-WS.org, 2017, p. 158. URL: http://ceur-ws.org/ Vol-2037/paper_23.pdf. [8] G. Mazzotta, F. Ricca, C. Dodaro, Compilation of aggregates in ASP systems, in: AAAI, AAAI Press, 2022, pp. 5834–5841. [9] A. Van Gelder, K. A. Ross, J. S. Schlipf, The well-founded semantics for general logic programs, J. ACM 38 (1991) 620–650. URL: https://doi.org/10.1145/116825.116838. [10] M. Gebser, M. Maratea, F. Ricca, The sixth answer set programming competition, Journal of Artificial Intelligence Research 60 (2017) 41–95. [11] S. Liang, P. Fodor, H. Wan, M. Kifer, Openrulebench: an analysis of the performance of rule engines, in: J. Quemada, G. LeΓ³n, Y. S. Maarek, W. Nejdl (Eds.), Proceedings of the 18th International Conference on World Wide Web, WWW 2009, Madrid, Spain, April 20-24, 2009, ACM, 2009, pp. 601–610. URL: https://doi.org/10.1145/1526709.1526790. [12] M. Alviano, F. Calimeri, C. Dodaro, D. FuscΓ , N. Leone, S. Perri, F. Ricca, P. Veltri, J. Zangari, The ASP system DLV2, in: Logic Programming and Nonmonotonic Reasoning - 14th International Conference, LPNMR 2017, Espoo, Finland, July 3-6, 2017, Proceedings, volume 10377 of Lecture Notes in Computer Science, 2017, pp. 215–221. URL: https://doi.org/10.1007/ 978-3-319-61660-5_19. [13] F. Calimeri, D. FuscΓ , S. Perri, J. Zangari, I-DLV: the new intelligent grounder of DLV, Intelligenza Artificiale 11 (2017) 5–20. URL: https://doi.org/10.3233/IA-170104. [14] M. Gebser, R. Kaminski, A. KΓΆnig, T. Schaub, Advances in gringo series 3, in: J. P. Delgrande, W. Faber (Eds.), Logic Programming and Nonmonotonic Reasoning - 11th International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings, volume 6645 of Lecture Notes in Computer Science, 2011, pp. 345–351.