=Paper= {{Paper |id=Vol-3428/paper11 |storemode=property |title=Compilation-based Techniques for Evaluating Normal Logic Programs Under the Well-founded Semantics |pdfUrl=https://ceur-ws.org/Vol-3428/paper11.pdf |volume=Vol-3428 |authors=Andrea Cuteri,Giuseppe Mazzotta,Francesco Ricca |dblpUrl=https://dblp.org/rec/conf/cilc/CuteriMR23 }} ==Compilation-based Techniques for Evaluating Normal Logic Programs Under the Well-founded Semantics== https://ceur-ws.org/Vol-3428/paper11.pdf 
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.