# optimised_maintenance_of_datalog_materialisations__54cb294f.pdf Optimised Maintenance of Datalog Materialisations Pan Hu, Boris Motik, Ian Horrocks Department of Computer Science, University of Oxford Oxford, United Kingdom firstname.lastname@cs.ox.ac.uk To efficiently answer queries, datalog systems often materialise all consequences of a datalog program, so the materialisation must be updated whenever the input facts change. Several solutions to the materialisation update problem have been proposed. The Delete/Rederive (DRed) and the Backward/Forward (B/F) algorithms solve this problem for general datalog, but both contain steps that evaluate rules backwards by matching their heads to a fact and evaluating the partially instantiated rule bodies as queries. We show that this can be a considerable source of overhead even on very small updates. In contrast, the Counting algorithm does not evaluate the rules backwards , but it can handle only nonrecursive rules. We present two hybrid approaches that combine DRed and B/F with Counting so as to reduce or even eliminate backward rule evaluation while still handling arbitrary datalog programs. We show empirically that our hybrid algorithms are usually significantly faster than existing approaches, sometimes by orders of magnitude. 1 Introduction Datalog (Abiteboul, Hull, and Vianu 1995) is a rule language that is widely used in modern information systems. Datalog rules can declaratively specify tasks in data analysis applications (Luteberget, Johansen, and Steffen 2016; Piro et al. 2016), allowing application developers to focus on the objective of the analysis that is, on specifying what needs to be computed rather than how to compute it (Markl 2014). Datalog can also capture OWL 2 RL (Motik et al. 2009) ontologies possibly extended with SWRL rules (Horrocks et al. 2004). It is implemented in systems such as Web PIE (Urbani et al. 2012), VLog (Urbani, Jacobs, and Kr otzsch 2016), Oracle s RDF Store (Wu et al. 2008), OWLIM (Bishop et al. 2011), and RDFox (Nenov et al. 2015), and it is extensively used in practice. When performance is critical, datalog systems usually precompute the materialisation (i.e., the set of all consequences of a program and the explicit facts) in a preprocessing step so that all queries can later be evaluated directly over the materialisation. Recomputing the materialisation from scratch whenever the explicit facts change can be Copyright c 2018, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. expensive. Systems thus typically use an incremental maintenance algorithm, which aims to avoid repeating most of the work. Fact insertion can be effectively handled using the semina ıve algorithm (Abiteboul, Hull, and Vianu 1995), but deletion is much more involved since one has to check whether deleted facts have derivations that persist after the update. The Delete/Rederive (DRed) algorithm (Gupta, Mumick, and Subrahmanian 1993; Staudt and Jarke 1996), the Backward/Forward (B/F) algorithm (Motik et al. 2015), and the Counting algorithm (Gupta, Mumick, and Subrahmanian 1993) are well-known solutions to this problem. The DRed algorithm handles deletion by first overdeleting all facts that depend on the removed explicit facts, and then rederiving the facts that still hold after overdeletion. The rederivation stage further involves rederiving all overdeleted facts that have alternative derivations, and then recomputing the consequences of the rederived facts until a fixpoint is reached. The algorithm and its variants have been extensively used in practice (Urbani et al. 2013; Ren and Pan 2011). In contrast to DRed, the B/F algorithm searches for alternative derivations immediately (rather than after overdeletion) using a combination of backward and forward chaining. This makes deletion exact and avoids the potential inefficiency of overdeletion. In practice, B/F often, but not always, outperforms DRed (Motik et al. 2015). Both DRed and B/F search for derivations of deleted facts by evaluating rules backwards : for each rule whose head matches the fact being deleted, they evaluate the partially instantiated rule body as a query; each query answer thus corresponds to a derivation. This has two consequences. First, one can examine rule instances that fire both before and after the update, which is redundant. Second, evaluating rules backwards can be inherently more difficult than matching the rules during initial materialisation: our experiments show that this step can, in some cases, prevent effective materialisation maintenance even for very small updates. In contrast, the Counting algorithm (Gupta, Mumick, and Subrahmanian 1993) does not evaluate rules backwards , but instead tracks the number of distinct derivations of each fact: a counter is incremented when a new derivation for the fact is found, and it is decremented when a derivation no longer holds. A fact can thus be deleted when its counter drops to zero, without the potentially costly backward rule evaluation. The algorithm can also be made optimal in the The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18) sense that it considers precisely the rule instances that no longer fire after the update and the rule instances that only fire after the update. The main drawback of Counting is that, unlike DRed and B/F, it is applicable only to nonrecursive rules (Nicolas and Yazdanian 1983). Recursion is a key feature of datalog, allowing one to express common properties such as transitivity. Thus, despite its favourable properties, the Counting algorithm does not provide us with a general solution to the materialisation maintenance problem. Towards the goal of developing efficient general-purpose maintenance algorithms, in this paper we present two hybrid approaches that combine DRed and B/F with Counting. The former tracks the nonrecursive and the recursive derivations separately, which allows the algorithm to eliminate all backward rule evaluation and also limit overdeletion. The latter tracks nonrecursive derivations only, which eliminates backward rule evaluation for nonrecursive rules; however, recursive rules can still be evaluated backwards to eagerly identify alternative derivations. Both combinations can handle recursive rules, and they exhibit pay-as-you-go behaviour in the sense that they become equivalent to Counting on nonrecursive rules. Apart from the modest cost of maintaining counters, our algorithms never involve more computation steps than their unoptimised counterparts. Thus, our algorithms combine the best aspects of DRed, B/F, and Counting: without incurring a significant cost, they eliminate or reduce backward rule evaluation, are optimal for nonrecursive rules, and can also handle recursive rules. We have implemented our hybrid algorithms and have compared them with the original DRed and B/F algorithms on several synthetic and real-life benchmarks. Our experiments show that the cost of counter maintenance is negligible, and that our hybrid algorithms typically outperform existing solutions, sometimes by orders of magnitude. Our test system and datasets are available online.1 2 Preliminaries We now introduce datalog with stratified negation. We fix countable, disjoint sets of constants and variables. A term is a constant or a variable. A vector of terms is written t, and we often treat it as a set. A (positive) atom has the form P(t1, . . . , tk) where P is a k-ary predicate and each ti, 1 i k, is a term. A term or an atom is ground if it does not contain variables. A fact is a ground atom, and a dataset is a finite set of facts. A rule r has the form B1 Bm not Bm+1 not Bn H, where m 0, n 0, and Bi and H are atoms. The head h(r) of r is the atom H, the positive body b+(r) of r is the set of atoms B1, . . . , Bm, and the negative body b (r) of r is the set of atoms Bm+1, . . . , Bn. Rule r must be safe: each variable occurring in r must occur in a positive body atom. A substitution σ is a mapping of finitely many variables to constants. For α a term, literal, rule, conjunction, or a vector or set thereof, ασ is the result of replacing each occurrence of a variable x in α with σ(x) (if the latter is defined). 1http://krr-nas.cs.ox.ac.uk/2017/counting/ A stratification λ of a program Π maps each predicate of Π to a positive integer such that, for each rule r Π with h(r) = P( t), (i) λ(P) λ(R) for each atom R( s) b+(r), and (ii) λ(P) > λ(R) for each atom R( s) b (r). Program Π is stratifiable if a stratification λ of Π exists. A rule r with h(r) = P( t) is recursive w.r.t. λ if an atom R( s) b+(r) exists such that λ(P) = λ(R); otherwise, r is nonrecursive w.r.t. λ. For each positive integer s, program Πs = {r Π | λ(h(r)) = s} is the stratum s of Π, and programs Πs r and Πs nr are the recursive and the nonrecursive subsets, respectively, of Πs. Finally, Os is the set of all facts that belong to stratum s that is, Os = {P( c) | λ(P) = s}. Rule r is an instance of a rule r if a substitution σ exists mapping all variables of r to constants such that r = rσ. For I a dataset, the set instr[I] of instances of r obtained by applying a rule r to I, and the set Π[I] of facts obtained by applying a program Π to I are defined as follows. instr[I] = {rσ | b+(r)σ I and b (r)σ I = } (1) r Π {h(r ) | r instr[I]} (2) We often say that each instance in instr[I] fires on I. We are now ready to define the semantics of stratified datalog. Given a dataset E of explicit facts and a stratification λ of Π with maximum stratum index number S, we define the following sequence of datasets: let I0 = E; let Is 0 = Is 1 for index s with 1 s S; let Is i = Is i 1 Πs[Is i 1] for each integer i > 0; and let Is = i 0 Is i . Set IS is called the materialisation of Π w.r.t. E and λ. It is well known that IS does not depend on λ, so we usually write it as mat(Π, E). In this paper, we consider the problem of maintaining mat(Π, E): given mat(Π, E) and datasets E and E+, our algorithm computes mat(Π, (E \ E ) E+) incrementally while minimising the amount of work. 3 Motivation and Intuition As motivation for our work, we next discuss how evaluating rules backwards can be a significant source of inefficiency during materialisation maintenance. We base our discussion on the DRed algorithm for simplicity, but our conclusions apply to the B/F algorithm as well. 3.1 The DRed Algorithm To make our discussion precise, we first present the DRed algorithm (Gupta, Mumick, and Subrahmanian 1993; Staudt and Jarke 1996). Let Π be a program with a stratification λ, let E be a set of explicit facts, and assume that the materialisation I = mat(Π, E) of Π w.r.t. E has been computed. Moreover, assume that E should be updated by deleting E and inserting E+. The DRed algorithm efficiently modifies the old materialisation I to the new materialisation I = mat(Π, (E \ E ) E+) by deleting some facts and adding others; we call such facts affected by the update. Due to the update, some rule instances that fire on I will no longer fire on I , and some rule instances that do not fire on I will fire on I ; we also call such rule instances affected by the update. A key problem in materialisation maintenance is to identify the affected rule instances. Clearly, the body of each affected rule instance must contain an affected fact. Based on this observation, the affected rule instances can be efficiently identified by the following generalisation of the operators instr[I] and Π[I] from Section 2. In particular, let Ip, In, P, and N be datasets such that P Ip and N In = ; then, let instr[Ip, In P, N] = {rσ | b+(r)σ Ip and b (r)σ In = , and b+(r)σ P = or b (r)σ N = } (3) Π[Ip, In P, N] = r Π {h(r ) | r instr[Ip, In P, N]}. Intuitively, the positive and the negative rule atoms are evaluated in Ip and In; sets P and N identify the affected positive and negative facts; instr[Ip, In P, N] are the affected instances of r; and Π[Ip, In P, N] are the affected consequences of Π. We define instr[Ip, In] and Π[Ip, In] analogously to above, but without the condition b+(r)σ P = or b (r)σ N = . We omit for readability In whenever Ip = In, and furthermore we omit N when N = . Sets Π[Ip, In] and Π[Ip, In P, N] can be computed efficiently in practice by evaluating the body of each rule r Π as a conjunctive query and instantiating the head as needed. Algorithm 1 formalises DRed. The algorithm processes each stratum s and accumulates the necessary changes to I in the set D of overdeleted and the set A of added facts. The materialisation is updated in line 6, so, prior to that, I and (I \ D) A are the old and the new materialisation, respectively. The computation proceeds in three phases. In the overdeletion phase, D is extended with all facts that depend on a deleted fact. In line 8 the algorithm identifies the facts that are explicitly deleted (E Os) or are affected by deletions in the previous strata (Πs[I D \ A, A \ D]), and then in lines 9 13 it computes their consequences. It uses a form of the semina ıve strategy, which ensures that each rule instance is considered only once during overdeletion. In the one-step rederivation phase, R is computed as the set of facts that have been overdeleted, but that hold nonetheless. To this end, in line 4 the algorithm considers each fact F in D Os, and it adds F to R if F is explicit or it is rederived by a rule instance. The latter involves evaluating rules backwards : the algorithm identifies each rule r Πs whose head can be matched to F, and it evaluates over the new materialisation the body of r as a query with the head variables bound; fact F holds if the query returns at least one answer. As we discuss shortly, this step can be a major source of inefficiency in practice, and the main contribution of this paper is eliminating backward rule evaluation and thus significantly improving the performance. In the insertion step, in line 15 the algorithm combines the one-step rederived facts (R) with the explicitly added facts (E+ Os) and the facts added due to the changes in the previous strata (Πs[(I \ D) A A \ D, D \ A]), and then in lines 16 20 it computes all of their consequences and adds them to A. Again, the semina ıve strategy ensures that each rule instance is considered only once during insertion. Algorithm 1 DRED(Π, λ, E, I, E , E+) 1: D := A := , E = (E E) \ E+, E+ = E+ \ E 2: for each stratum index s with 1 s S do 3: OVERDELETE 4: R := {F D Os | F E \ E or there exist r Πs and r instr[I \ (D \ A), I A] with F = h(r )} 5: INSERT 6: E := (E \ E ) E+, I := (I \ D) A 7: procedure OVERDELETE 8: ND := (E Os) Πs[I D \ A, A \ D] 9: loop 10: ΔD := ND \ D 11: if ΔD = then break 12: ND := Πs r [I \ (D \ A), I A ΔD] 13: D := D ΔD 14: procedure INSERT 15: NA := R (E+ Os) Πs[(I \ D) A A \ D, D \ A] 16: loop 17: ΔA := NA \ ((I \ D) A) 18: if ΔA = then break 19: A := A ΔA 20: NA := Πs r [(I \ D) A ΔA] 3.2 Problems with Evaluating Rules Backwards The one-step rederivation in line 4 of Algorithm 1 evaluates rules backwards . In this section we present two examples that demonstrate how this can be a major source of inefficiency. Both examples are derived from datasets we used in our empirical evaluation that we present in Section 6; hence, these problems actually arise in practice. Our discussion depends on several details. In particular, we assume that all facts are indexed so that all facts matching any given atom (possibly containing constants) can be identified efficiently. Moreover, we assume that conjunctive queries corresponding to rule bodies are evaluated left-toright: for each match of the first conjunct, we partially instantiate the rest of the body and match it recursively. Finally, we assume that query atoms are reordered prior to evaluation to obtain an efficient evaluation plan. Example 1. Let Π and E be the program and the dataset as specified in (4) and (5), respectively. R(x, y1) R(x, y2) S(y1, y2) (4) E = {R(ai, b), R(ai, ci) | 1 i n} (5) The materialisation mat(Π, E) consists of E extended with facts S(b, b), S(b, ci), S(ci, b), and S(ci, ci) for 1 i n. During materialisation, the body of rule (4) can be evaluated efficiently left-to-right: we match R(x, y1) to either R(ai, b) or R(ai, ci); this instantiates R(x, y2) as R(ai, y2), and we use the index to find the matching facts R(ai, b) and R(ai, ci). Thus, R(x, y1) has 2n matches, each of which contributes to two matches of R(x, y2), so the overall cost of rule matching is O(n). The rule body is symmetric, so reordering the body atoms has no effect. Now assume that we delete all R(ai, ci) with 1 i n. DRed then overdeletes all S(b, ci), S(ci, b) and S(ci, ci) facts in lines 8 13, and this can be done efficiently as in the previous paragraph. Next, in one-step rederivation, the algorithm will match these facts to the head of the rule (4) and obtain queries R(x, b) R(x, ci), R(x, ci) R(x, b), and R(x, ci) R(x, ci). All but the last of these queries contain atom R(x, b) and, no matter how we reorder the body atoms of (4), we have n queries where R(x, b) is evaluated first. Each of these n queries identifies n candidate matches R(ai, b) using the index only to find out that the second atom cannot be matched. Thus, R(x, b) is matched to n2 facts in total, so the cost of one-step rederivation is O(n2) one degree higher than for materialisation. Example 1 shows that evaluating a rule backwards can be inherently more difficult than evaluating it during materialisation, thus giving rise to a dominating source of inefficiency. In fact, evaluating a rule with m body atoms backwards can be seen as answering a query with m + 1 atoms, where the head of the rule is an extra query atom; since the number of atoms determines the complexity of query evaluation, this extra atom increases the algorithm s complexity. Our next example shows that this problem is exacerbated if the space of admissible plans for queries corresponding to rule bodies is further restricted. This is common in systems that provide built-in functions. In particular, to facilitate manipulation of concrete values such as strings or integers, datalog systems often allow rule bodies to contain built-in atoms of the form (t := exp), where t is a term and exp is an expression constructed using constants, variables, functions, and operators as usual. For example, a built-in atom can have the form (z := z1 + z2), and it assigns to z the sum of z1 and z2. The set of supported functions vary among implementations, but a common feature is that all values in exp must be bound by prior atoms before the built-in atom can be evaluated. As we show next, this can be problematic. Example 2. Let program Π consist of rules (6) and (7). If we read B(s, t, n) as saying that there is an edge from node s to node t of length n, then the program entails D(s, n) if there exists a path of length n from node a to node s. B(a, y, z) D(y, z) (6) D(x, z1) B(x, y, z2) (z := z1 + z2) D(y, z) (7) Let E be the dataset as specified below. E = {B(a, b1, 1), B(a, ci, 1), B(bi, dj, 1) | 1 i, j n} During materialisation, rule (6) first derives D(b1, 1) and all D(ci, 1) with 1 i n, so the cost of this step is O(n). Next, atom D(x, z1) in rule (7) is matched to n facts D(ci, 1) without deriving anything. Atom D(x, z1) is also matched to D(b1, 1) once, so atom B(x, y, z2) is instantiated to B(b1, y, z2) and matched to n facts B(b1, dj, 1), deriving n facts D(dj, 2). Thus, the cost of rule matching is O(n). Now assume that B(a, b1, 1) is deleted. Then, D(b1, 1) and all D(dj, 2) can be efficiently overdeleted as in the previous paragraph, but trying to prove them is much more difficult. Matching each D(dj, 2) to the head of (6) produces a query B(a, dj, 2), which does not produce a rule instance. Moreover, matching D(dj, 2) to the head of (7) produces a query D(x, z1) B(x, dj, z2) (2 := z1 + z2). Now, as we discussed earlier, z1 and z2 must both be bound before we can evaluate the built-in atom (2 := z1 + z2). If we evaluate B(x, dj, z2) first, then we try n facts B(bi, dj, 1) with 1 i n; for each of them, atom D(x, z1) is instantiated as D(bi, z1) and is not matched in the surviving facts. In contrast, if we evaluate D(x, z1) first, then we try n facts D(ci, 1); for each of them, atom B(x, dj, z2) is instantiated as B(ci, y, z2) and is not matched. Thus, regardless of how we reorder the body of (7), the first atom considers a total of n2 facts, so the cost of one-step rederivation is O(n2). To overcome this, one might rewrite the built-in atom as (z1 := z z1) or (z2 := z z2) so that it can be evaluated immediately after z and either z1 or z2 are bound. Either way, one-step rederivation still takes O(n2) steps on our example. Also, built-in expressions are often not invertible. 4 Combining DRed with Counting We now address the inefficiencies we outlined in Section 3. Towards this goal, in Section 4.1 we first present the intuitions, and then in Section 4.2 we formalise our solution. 4.1 Intuition As we already mentioned in Section 1, the Counting algorithm (Gupta, Mumick, and Subrahmanian 1993) does not evaluate rules backwards ; instead, it tracks the number of derivations of each fact. The main drawback of Counting is that it cannot handle recursive rules. We now illustrate the intuition behind our DRedc algorithm, which combines DRed with Counting in a way that eliminates backward rule evaluation, while still supporting recursive rules. The DRedc algorithm associates with each fact two counters that track the derivations via the nonrecursive and the recursive rules separately. The counters are decremented (resp. incremented) when the associated fact is derived in overdeletion (resp. insertion), which allows for two important optimisations. First, as in the Counting algorithm, the nonrecursive counter always reflects the number of derivations from facts in earlier strata; hence, a fact with a nonzero nonrecursive counter should never be overdeleted because it clearly remains true after the update. This optimisation captures the behaviour of Counting on nonrecursive rules and it also helps limit overdeletion. Second, if we never overdelete facts with nonzero nonrecursive counters, the only way for a fact to still hold after overdeletion is if its recursive counter is nonzero; hence, we can replace backward rule evaluation by a simple check of the recursive counter. Note, however, that the recursive counters can be checked only after overdeletion finishes. This optimisation extends the idea of Counting to recursive rules to completely avoid backward rule evaluation. The following example illustrates these ideas and compares them to DRed. Example 3. Let Π be the program containing rule (8). A(x) B(x, y) A(y) (8) Moreover, let E be defined as follows: E = {A(a), A(b), A(d), B(a, c), B(b, c), B(c, d), B(d, e)} T1: (1,0) T2: (0,0) T3: (0,0) A(a) A(b) T1: (1,0) T2: (1,0) T3: (1,0) T1: (0,2) T2: (0,1) T3: (0,1) A(c) T1: (1,1) T2: (1,0) T3: (1,1) A(d) T1: (0,1) T2: (0,1) T3: (0,1) A(e) Figure 1: Derivations for Example 3 The materialisation mat(Π, E) extends E with A(c) and A(e). Figure 1 shows the dependencies between derivations using arrows. For clarity, we do not show the B-facts. Now assume that A(a) is deleted. The standard DRed algorithm first overdeletes A(a), A(c), A(d), and A(e); it rederives A(d) since the fact is in E \ E ; it rederives A(c) by evaluating rule (8) backwards ; and it derives A(d) and A(e) from the rederived facts. Now consider applying the DRedc to the same update. For each fact, Figure 1 shows a pair consisting of the nonrecursive and the recursive counter before the update (row T1), after overdeletion (row T2), and after the update (row T3). Note that the presence of a fact in E is akin to a nonrecursive derivation, so facts A(a), A(b), and A(d) have nonrecursive derivation counts of one before the update. Now A(c) is derived from A(a) and A(b) using the recursive rule (8), so the recursive counter for A(c) is two. Analogously, A(d) and A(e) have just one recursive derivation each. During overdeletion, A(a) is first removed from E, so the nonrecursive counter of A(a) is decremented to zero and the fact is deleted. Since A(a) derives A(c) via rule (8), the recursive counter of A(c) is decremented; since the nonrecursive counter of A(c) is zero, the fact is overdeleted. Since A(c) derives A(d) via rule (8), the recursive counter of A(d) is decremented. Now the nonrecursive counter of A(d) is nonzero, so we know that A(d) holds after the update; hence, the fact is not overdeleted, and the overdeletion phase stops. Thus, while DRed overdeletes four facts, DRedc overdeletes only A(a) and A(c), and does not touch A(e). Next, DRedc proceeds to one-step rederivation. The recursive counter of A(c) is nonzero, which means that the fact has a recursive derivation (from A(b) in this case) that is not affected. Thus, DRedc rederives A(c) without any backward rule evaluation. Finally, DRedc applies insertion. Since A(c) derives A(d) via (8), the recursive counter of A(d) is incremented. Fact A(d), however, was not overdeleted, so insertion stops. By avoiding backward rule evaluation, DRedc removes the dominating source of inefficiency on Examples 1 and 2. In fact, on the nonrecursive program from Example 1, the recursive counter is never used and DRedc performs the same inferences as the Counting algorithm. 4.2 Formalisation We now formalise our DRedc algorithm. Our definitions use the standard notion of multisets a generalisation of sets where each element is associated with a positive integer called the multiplicity specifying the number of the element s occurrences in the multiset. Moreover, is the multiset union operator, which adds the elements multiplicities. If an operand of is a set, it is treated as a multiset where all elements have multiplicity one. Finally, we extend the notion of rule matching to correctly reflect the number of times a fact is derived: for Ip, In, P, and N datasets with P Ip and N In = , we define Π Ip, In P, N as the multiset containing a distinct occurrence of h(r ) for each rule r Π and its instance r instr[Ip, In P, N]. This multiset can be computed analogously to Π[Ip, In P, N]. Just like DRed, the DRedc takes as input a program Π, a stratification λ, a set of explicit facts E and its materialisation I = mat(Π, E), and the sets of facts E and E+ to remove from and add to E. Additionally, the algorithm also takes as input maps Cnr and Cr that associate each fact F with its nonrecursive and recursive counters Cnr[F] and Cr[F], respectively. These maps should correctly reflect the relevant numbers of derivations. Formally, Cnr and Cr must be compatible with Π, λ, and E, which is the case if Cnr[F] = Cr[F] = 0 for each fact F I, and, for each fact F I and s the stratum index such that F Os (i.e., s is the index of the stratum that F belongs to), Cnr[F] is the multiplicity of F in E Πs nr I , and Cr[F] is the multiplicity of F in Πs r I . For simplicity, we assumes that Cnr and Cr are defined on all facts, and that Cnr[F] = Cr[F] = 0 holds for F I; thus, we can simply increment the counters for each newly derived fact in procedure INSERT. In practice, however, one can maintain counters only for the derived facts and initialise the counters to zero for the freshly derived facts. DRedc is formalised in Algorithm 2. Its structure is similar to DRed, with the following main differences: instead of evaluating rules backwards , one-step rederivation simply checks the recursive counters (line 24); a fact is overdeleted only if the nonrecursive derivation counter is zero (line 34); and the derivation counters are decremented in overdeletion (lines 29 32 and 36 37) and incremented in insertion (lines 41 44 and 49 50). The algorithm also accumulates changes to the materialisation in sets D and A by iteratively processing the strata of λ in three phases. In the overdeletion phase, DRedc first considers explicitly deleted facts or facts affected by the changes in earlier strata (lines 29 32). This is analogous to line 8 of DRed, but DRedc must distinguish Πs nr from Πs r so it can decrement the appropriate counters. Next, DRedc identifies the set ΔD of facts that have not yet been deleted and whose nonrecursive counter is zero (line 34): a fact with a nonzero nonrecursive counter will always be part of the new materialisation. Note that recursive derivations can be cyclic, so we cannot use the recursive counter to further constrain overdeletion at this point. Then, in lines 35 38 the algorithm propagates consequences of ΔD just like Algorithm 1, with additionally decrementing the recursive counters in line 37. Algorithm 2 DREDc(Π, λ, E, I, E , E+, Cnr, Cr) 21: D := A := , E = (E E) \ E+, E+ = E+ \ E 22: for each stratum index s with 1 s S do 23: OVERDELETE 24: R := {F D Os | Cr[F] > 0} 25: INSERT 26: E := (E \ E ) E+, I := (I \ D) A 27: procedure OVERDELETE 28: ND := 29: for F (E Os) Πs nr I D \ A, A \ D do 30: ND := ND {F}, Cnr[F] := Cnr[F] 1 31: for F Πs r I D \ A, A \ D do 32: ND := ND {F}, Cr[F] := Cr[F] 1 33: loop 34: ΔD := {F ND \ D | Cnr[F] = 0} 35: if ΔD = then break 36: for F Πs r I \ (D \ A), I A ΔD do 37: ND := ND {F}, Cr[F] := Cr[F] 1 38: D := D ΔD 39: procedure INSERT 40: NA := R 41: for F (E+ Os) Πs nr (I \ D) A A \ D, D \ A do 42: NA := NA {F}, Cnr[F] := Cnr[F] + 1 43: for F Πs r (I \ D) A A \ D, D \ A do 44: NA := NA {F}, Cr[F] := Cr[F] + 1 45: loop 46: ΔA := NA \ ((I \ D) A) 47: if ΔA = then break 48: A := A ΔA 49: for F Πs r (I \ D) A ΔA do 50: NA := NA {F}, Cr[F] := Cr[F] + 1 In the one-step rederivation phase, instead of evaluating rules backwards , DRedc just checks the recursive counter of each fact F D Os (line 24): if Cr[F] = 0, then some derivations of F were not touched by overdeletion so F holds in the new materialisation. Conversely, if Cr[F] = 0, then F D guarantees that Cnr[F] = 0 holds as well, so F is not one-step rederivable by a rule in Π. The insertion phase of DRedc just uses the semina ıve evaluation while incrementing the counters appropriately. Without recursive rules, DRedc becomes equivalent to Counting, and it is optimal in the sense that only affected rule instances are considered during the update. Moreover, the computational complexities of both DRedc and DRed are the same as for the semi-naive materialisation algorithm: Exp Time in combined and PTime in data complexity (Dantsin et al. 2001). Finally, DRedc never performs more inferences than DRed and is thus more efficient. Theorem 1 shows that our algorithm is correct, and its proof is given in an extended technical report (Hu, Motik, and Horrocks 2017). Theorem 1. Algorithm 2 correctly updates I = mat(Π, E) to I = mat(Π, E ) for E = (E \ E ) E+, and it updates Cnr and Cr so they are compatible with Π, λ, and E . 5 Combining B/F with Counting The B/F algorithm by Motik et al. (2015) uses a combination of backward and forward chaining that makes the deletion phase exact. More specifically, when a fact F ΔD is considered during deletion, the algorithm uses a combination of backward and forward chaining to look for alternative derivations of F, and it deletes F only if no such derivation can be found. Backward chaining allows B/F to be much more efficient than DRed on many datasets, and this is particularly the case if a program contains many recursive rules. Thus, we cannot hope to remove all backward rule evaluation without eliminating the algorithm s main advantage. Still, there is room for improvement: backward chaining involves backward evaluation of both nonrecursive and recursive rules, and we can use nonrecursive counters to eliminate the former. Algorithm 3 formalises B/Fc our combination of the B/F algorithm by Motik et al. (2015) with Counting. The main difference to the original B/F algorithm is that B/Fc associates with each fact a nonrecursive counter that is maintained in lines 59 60 and 89 90, and, instead of evaluating nonrecursive rules backwards to explore alternative derivations of a fact, it just checks in line 79 whether the nonrecursive counter is nonzero. We know that a fact holds if its nonrecursive counter is nonzero; otherwise, we apply backward chaining to recursive rules only.We next describe the algorithm s steps in more detail. Procedure DELETEUNPROVED plays an analogous role to the overdeletion step of DRed and DRedc. The procedure maintains the nonrecursive counter for each fact in the same way as DRedc, and the main difference is that a fact F is deleted (i.e., added to ΔD) in line 66 only if no alternative derivation can be found using a combination of backward and forward chaining implemented in functions CHECK and SATURATE. If an alternative derivation is found, F is added to the set P of proved facts. A call to CHECK(F) searches for the alternative derivations of F using backward chaining. The function maintains the set C of checked facts, which ensures that each F is checked only once (line 71 and 78). The procedure first calls SATURATE(F) to determine whether F follows from the facts considered thus far; we discuss this step in more detail shortly. If F is not proved, the procedure then examines in lines 73 76 each instance r of a recursive rule that derives F in the old materialisation, and it tries to prove all body atoms of r from the current stratum. This involves evaluating rules backwards and, as we already discussed in Section 5, this is the main advantage of the B/F algorithm over DRed on a number of complex inputs. The function terminates once F is successfully proved (line 76). Set P accumulates facts that are checked and successfully proved, and it is computed in function SATURATE using forward chaining. Given a fact F that is being checked, it first verifies whether F has a nonrecursive derivation. In the original B/F algorithm, this is done by evaluating the nonrecursive rules backwards in the same way as in line 4 of DRed. In contrast, B/Fc avoids this by simply checking whether the nonrecursive counter is nonzero (line 79): if that is the case, then F is known to have nonrecursive derivations and it is added to P via lines 80 and 82. If F is proved, the proce- dure propagates its consequences (line 80 85). In particular, the procedure ensures that each consequence F of P, the facts in the new materialisation in the previous strata, and the recursive rules is added to P if F C, or is added to the set Y of delayed facts if F C. Intuitively, set Y contains facts that are proved but that have not been checked yet. If a fact in Y is checked at a later point, it is proved in line 79 without having to apply the rules again. Since the deletion step of B/Fc is exact in the sense that it deletes precisely those facts that no longer hold after the update, rederivation is not needed. Thus, DELETEUNPROVED is directly followed by INSERT, which is the same as in DRed and DRedc, with the only difference that B/Fc maintains only the nonrecursive counters. Algorithm 3 is correct in the same way as B/F since checking whether a fact has a nonzero nonrecursive counter is equivalent to checking whether a derivation of the fact exists by evaluating nonrecursve rules backwards . 6 Evaluation We have implemented the unoptimised and optimised variants of DRed and B/F and have compared them empirically. Benchmarks We used the following benchmarks for our evaluation: UOBM (Ma et al. 2006) is a synthetic benchmark that extends the well known LUBM (Guo, Pan, and Heflin 2005) benchmark; Reactome (Croft et al. 2013) models biological pathways of molecules in cells; Uniprot (Bateman et al. 2015) describes protein sequences and their functional information; Chem BL (Gaulton et al. 2011) represents functional and chemical properties of bioactive compounds; and Claros describes archeological artefacts. Each benchmark consists of a set of facts and an OWL 2 DL ontology, which we transformed into datalog programs of different levels of complexity and recursiveness. More specifically, the upper bound (U) programs were obtained using the complete but unsound transformation by Zhou et al. (2013), and they entail all consequences of the original ontology but may also derive additional facts. The recursive (R) programs were obtained using the sound but incomplete transformation by Kaminski, Nenov, and Grau (2016), and they tend to be highly recursive. For Claros, the lower bound extended (LE) program was obtained by manually introducing several hard rules, and it was already used by Motik et al. (2015) to compare DRed with B/F. Finally, to estimate the effect of built-in literals on materialisation maintenance, we developed a new synthetic benchmark SSPE (Single-Source Path Enumeration). Its dataset consists of a randomly generated directed acyclic graph of 100 k nodes and 1 M edges, and its program traverses paths from a single source analogously to rules (6) (7). All the tested programs are recursive, although the percentage of the recursive rules varies. Table 1 shows the numbers of facts (|E|), strata (S), the nonrecursive rules (|Πnr|), and the recursive ones (|Πr|) for each benchmark. Test Setup We conducted all experiments on a Dell Power Edge R720 server with 256GB RAM and two Intel Xeon E5-2670 2.6GHz processors, running Fedora 24, kernel version 4.8.12-200.fc24.x86 64. All algorithms handle insertions using the semina ıve evaluation. The only overhead is in Algorithm 3 B/Fc(Π, λ, E, I, E , E+, Cnr) 51: D := A := , E = (E E) \ E+, E+ = E+ \ E 52: for each stratum index s with 1 s S do 53: C := P := Y := 54: DELETEUNPROVED 55: INSERT 56: E := (E \ E ) E+, I := (I \ D) A 57: procedure DELETEUNPROVED 58: ND := 59: for F (E Os) Πs nr I D \ A, A \ D do 60: ND := ND {F}, Cnr[F] := Cnr[F] 1 61: ND := ND Πs r [I D \ A, A \ D] 62: loop 63: ΔD := 64: for F ND \ D do 65: CHECK(F) 66: if F P then ΔD := ΔD {F} 67: if ΔD = then break 68: ND := Πs r [I \ (D \ A), I A ΔD] 69: D := D ΔD 70: function CHECK(F) 71: if F C then 72: if SATURATE(F) = f then 73: for each r Πs r and each r instr[I \ ((D ΔD) \ A), I A] s.t. h(r ) = F do 74: for G b+(r ) Os do 75: CHECK(G) 76: if F P then return 77: function SATURATE(F) 78: C := C {F} 79: if F Y or Cnr[F] > 0 then 80: NP := {F} 81: loop 82: ΔP := (NP C) \ P, Y := Y NP \ C 83: if ΔP = then return t 84: P := P ΔP 85: NP := Πs r [P (O