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 diferent settings and preliminary results highlight significant improvements in the evaluation of non-stratified programs.
Logic programming is a declarative programming paradigm that can be used to model complex
problems in terms of logical implications [
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.
An empirical evaluation of the proposed approach has been conducted on hard
benchmarks [
In this section, some preliminaries are provided on normal logic programs under the
wellfounded semantics [
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 complement 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.
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
well-founded model is defined as
= +1. Basically, is the least fixed point [
= where ≥ 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) 0 is the smallest ordinal such that
Input : A normal program
Output : Prints evaluation procedure for for all ∈ (, ) do
(, , ) ≪ while _ ̸= ∅ do≫ = _.()≫ switch ()≫ for all ∈ [1, . . . , ||] do for all ∈ (, ) do if ([]) ∈ ∧ [] is positive literal then ≪ ≪ done≫ ≪ do≫ = ⊥≫ for ∈ ℬ do≫ = = ⊥≫ = _.()≫ switch ()≫ done≫ ≪ while == ⊤ ≫ ≪ 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
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 [
is printed by the compiler as it is. Instead, the code
JK enclosed in
, 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.
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 diferent 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, · · · w.r.t. . Thus, if it is the case then the head of the rule is derived as true, otherwise it is derived , are true 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, diferent 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 diferent 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 diferent 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
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 ≪ JK = ≫ 5 if [] is a positive literal then 67 ≪≪ foJrKall = J{K ∈∈( ∪JKℬ)d|o≫ ℎ( ( J[]K ), )}≫ 8 for all ∈ 1, ..., |([])| do 9 if ([])[] is variable then 10 ≪ = ∪ { J([])[]K ↦→ ( JK )[ JK ]}≫ 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 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 ≪ ≪ ≪ ≪ ≪ ≪ ≪ ≪ ≪ ≪ if ≫ ≪ ≪ if ≫ = ∪ {ℎ}≫ ℬ = ℬ ∖ {ℎ}≫ = = ⊤≫ else if ((+
= ⊤≫ ℎ = (
J K )≫ if + ⊆ ∧ (¬− ∩ ℬ) = ∅ ∧ ℎ ∈/ then≫ = ∪ { J()[]K ↦→ ()[ JK ]}≫
∪ ¬− ) ∩ ℬ) ̸= ∅ ∧ ℎ ∈/ then≫ for all ∈ [||, . . . , 1] do if [] is positive literal then else 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 . 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 instantiations have been founded for the atom then it is derived as false (Alg. 7 lines 48-51).
Algorithm 6 Output example compileRuleForHeadDerivation
Input : {(, ), (, ), ()}, ( ), {′′,′ ′}
if == ∅ ∧ + ⊆ ∧ (¬− ∩ ℬ) = ∅ then
=
done
done
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
else
ℬ = ℬ ∪ {ℎ}
_ = _ ∪ {ℎ}
= ∪ { ↦→ ()[
= Algorithm 7 Output example compileRulesForSupportDerivation 1 = { ∈ ( ∪ ℬ) | ℎ( (()), )} done if if = ⊥ ∧ = ⊥ then = ⊤ ℬ = ℬ ∖ {}
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, diferent 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 [
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 diferent 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
competitions that are Knight Tour with Holes, Stable Marriage, and Graph Colouring [
Our approach, labeled wf-comp, was compared with the following tools:
• General-purpose systems that can evaluate Datalog programs: idlv [
20 30 40 50 Number of solved instances 60 1,800
• ASP system dlv2 [
dlv2 wf-comp 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 diference with our tool ( souffle is preferable in complete graphs) is due to diferent data structures and also to the diferent input formats. Indeed, souffle takes as input a numeric format where input facts are organized in files for
dlv2 wf-comp 40 80 120
160
Number of solved instances each input predicate while wf-comp reads plain text files.
Evaluation on Programs with Negation. In the case of programs with negation, we compare 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).
Logic programming is a widely employed programming paradigm for modeling complex
problems in a declarative fashion. Eficient implementations are needed in order to exploit
the strength of such formalism in real-world applications. Compilation-based techniques
were revealed to be efective in tackling diferent issues raised in the evaluation of logic
programs [