Extended Caching and Backjumping for Expressive
                    Description Logics

                  Andreas Steigmiller1 , Thorsten Liebig2 , and Birte Glimm1
            1
                Ulm University, Ulm, Germany, <first name>.<last name>@uni-ulm.de
                        2
                          derivo GmbH, Ulm, Germany, liebig@derivo.de




1      Motivation

Due to the wide range of modelling constructs supported by the expressive DL SROIQ,
the typically used tableau algorithms in competitive reasoning systems such as FaCT++
[16], HermiT,3 or Pellet [14] have a very high worst-case complexity. The development
of tableau optimisations that help to achieve practical efficiency is, therefore, a long-
standing challenge in DL research (see, e.g., [11, 17]). A very effective and widely im-
plemented optimisation technique is “caching”, where one caches, for a set of concepts,
whether they are known to be, or can safely be assumed to be, satisfiable or unsatisfi-
able [4]. If the set of concepts appears again in a model abstraction, then a cache-lookup
allows for skipping further applications of tableau rules. Unfortunately, with increasing
expressivity naively caching become unsound, for instance, due to the possible interac-
tion of inverse roles with universal restrictions [1, Chapter 9].
    With this contribution we push the boundary of the caching optimisation to the
expressive DL SROIQ. The developed unsatisfiability caching method is based on a
sophisticated dependency management, which further enables better informed tableau
backtracking and more efficient pruning (Section 3). Our techniques are grounded in the
widely implemented tableau calculus for SROIQ [9], which makes it easy to transfer
our results into existing implementations. The optimisations are integrated within a
novel reasoning system, called Konclude [13]. Our empirical evaluation shows that the
proposed optimisations result in significant performance improvements (Section 4).


2      Preliminaries

Model construction calculi, such as tableau, decide the consistency of a knowledge
base K by trying to construct an abstraction of a model for K, a so-called “completion
graph”. A completion graph G is a tuple (V, E, L, ,̇), where each node x ∈ V represents
one or more individuals, and is labelled with a set of concepts, L(x), which the individ-
uals represented by x are instances of; each edge hx, yi represents one or more pairs of
individuals, and is labelled with a set of roles, L(hx, yi), which the pairs of individuals
represented by hx, yi are instances of. The relation ,̇ records inequalities, which must
hold between nodes, e.g., due to at-least cardinality restrictions.
 3
     http://www.hermit-reasoner.com
    The algorithm works by initialising the graph with one node for each Abox in-
dividual/nominal in the input KB, and using a set of expansion rules to syntactically
decompose concepts in node labels. Each such rule application can add new concepts
to node labels and/or new nodes and edges to the completion graph, thereby explicat-
ing the structure of a model. The rules are repeatedly applied until either the graph is
fully expanded (no more rules are applicable), in which case the graph can be used to
construct a model that is a witness to the consistency of K, or an obvious contradiction
(called a clash) is discovered (e.g., both C and ¬C in a node label), proving that the
completion graph does not correspond to a model. The input knowledge base K is con-
sistent if the rules (some of which are non-deterministic) can be applied such that they
build a fully expanded, clash free completion graph. A cycle detection technique called
blocking ensures the termination of the algorithm.


2.1   Dependency Tracking

Dependency tracking keeps track of all dependencies that cause the existence of con-
cepts in node labels, roles in edge labels as well as accompanying constrains such as
inequalities that must hold between nodes. Dependencies are associated with so-called
facts, defined as follows:

Definition 1 (Fact) We say that G contains a concept fact C(x) if x ∈ V and C ∈ L(x),
G contains a role fact r(x, y) if hx, yi ∈ E and r ∈ L(hx, yi), and G contains an inequality
fact x ,̇ y if x, y ∈ V and (x, y) ∈ ,̇. We denote the set of all (concept, role, or inequality)
facts in G as FactsG .

Dependencies now relate facts in a completion graph to the facts that caused their exis-
tence. Additionally, we annotate these relations with a running index, called dependency
number, and a branching tag to track non-deterministic expansions:

Definition 2 (Dependency) Let d be a pair in FactsG × FactsG . A dependency is of the
form dn,b with n ∈ IN0 a dependency number and b ∈ IN0 a branching tag.
    We inductively define the dependencies DepG for G: If G is an initial completion
graph, then DepG = ∅. We initialise the beginning for the next dependency numbers nm
with 1 if DepG = ∅; otherwise, nm = 1 + max{n | dn,b ∈ DepG }. Let R be a tableau rule
applicable to a completion graph G. If R is non-deterministic, the next non-deterministic
branching tag bR for R is 1 + max{{0} ∪ {b | dn,b ∈ DepG }}; for R deterministic, bR = 0.
Let G0 be the completion graph obtained from G by applying R with c0 , . . . , ck the facts
to satisfy the preconditions of R and c00 , . . . , c0` the newly added facts in G0 , then
         DepG0 = DepG ∪ {(c0j , ci )n,b | 0 ≤ i ≤ k, 0 ≤ j ≤ `, n = nm + ( j ∗ k) + i,
                                          b = max{{bR } ∪ {b0 | (ci , c)n ,b ∈ DepG }}}.
                                                                         0 0




The branching tag indicates which facts were added non-deterministically:

Definition 3 (Non-deterministic Dependency) For dn,b ∈ DepG with d = (c1 , c2 ), let
Dd = {(c2 , c3 )n ,b | (c2 , c3 )n ,b ∈ DepG }. The dependency dn,b is a non-deterministic
                 0 0              0 0


dependency in G if b > 0 and either Dd = ∅ or max{b0 | (c, c0 )n ,b ∈ Dd } < b.
                                                                  0 0
           a0     L(a0 ) = { (∃r.(A u (∃r.(∀r− .B)))) , (∀r.¬B) , (C t D) , C }

                                     b2,0                                     a1,1
                                                c3,0
             L(ha0 , x1 i) = { r }
                                                               e5,0
                                                       4,0
                                                   d

            x1    L(x1 ) = { (A u (∃r.(∀r− .B))) , ¬B , A , (∃r.(∀r− .B)) , B }

                               g7,0                    f 6,0
                                                                      j10,0
             L(hx1 , x2 i) = { r }                     h8,0
                                                                      k11,0
                                            9,0
                                            i
            x2    L(x2 ) = { (∀r− .B) }


         Fig. 1. Tracked dependencies for all facts in the generated completion graph


    Figure 1 illustrates a completion graph obtained in the course of testing the consis-
tency of a knowledge base with three concept assertions:
              a0 : (∃r.(A u (∃r.(∀r− .B))))     a0 : (∀r.¬B)      a0 : (C t D).
Thus, the completion graph is initialised with the node a0 , which has the three con-
cepts in its label. Initially, the set of dependencies is empty. For the concepts and roles
added by the application of tableau rules, the dependencies are shown with dotted lines,
labelled with the dependency. The dependency number increases with every new de-
pendency. The branching tag is only non-zero for the non-deterministic addition of C to
the label of a0 in order to satisfy the disjunction (C t D). Note the presence of a clash
due to B and ¬B in the label of x1 .


3     Extended Caching and Backtracking
In the following we introduce improvements to caching and backjumping by present-
ing a more informed dependency directed backtracking strategy that also allows for
extracting precise unsatisfiability cache entries.

3.1   Dependency Directed Backtracking
Dependency directed backtracking is an optimisation that can effectively prune irrele-
vant alternatives of non-deterministic branching decisions. If branching points are not
involved in clashes, it will not be necessary to compute any more alternatives of these
branching points, because the other alternatives cannot eliminate the cause of the clash.
To identify involved non-deterministic branching points, all facts in a completion graph
are labelled with information about the branching points they depend on. Thus, the
united information of all clashed facts can be used to identify involved branching points.
A typical realisation of dependency directed backtracking is backjumping [1, 17], where
the dependent branching points are collected in the dependency sets for all facts.
3.2   Unsatisfiability Caching

Another widely used technique to increase the performance of a tableau implementation
is caching. For unsatisfiability caching, one caches sets of concepts that are known to
be unsatisfiable. For such a cache entry, it holds that any superset is also unsatisfiable.
Thus, if, in a future tableau expansion, one encounters a node label that is a superset of
a cache entry, one can stop expanding the branch.
    Analogously to unsatisfiability caching, one can define satisfiability caching and
many systems combine both caches. We focus here, however, on unsatisfiability caching
since the two problems are quite different in nature and the required data structures for
an efficient cache retrieval can differ significantly. Before we define how and when we
create cache entries, we formalise our notion of an unsatisfiability cache.

Definition 4 (Unsatisfiability Cache) Let K be a knowledge base and ConK the set
of (sub-)concepts that occur in K. An unsatisfiability cache UCK for K is a subset of
2ConK such that each cache entry S ∈ UCK is unsatisfiable w.r.t. K. An unsatisfiability
retrieval for UCK and a completion graph G for K takes a set of concepts S ⊆ ConK
from a node label of G as input. If UCK contains a set S⊥ ⊆ S , then S⊥ is returned;
otherwise, the empty set is returned.

    Although node labels can have many concepts that are not involved in any clashes,
most implementations cache complete node labels. One reason for this might be that
the often used backjumping [1, 17] only allows the identification of all branching points
involved in a clash, but there is no information about how the clash is exactly caused. We
refer to this form of caching as label caching. Systems that use label caching typically
also only check whether the exact node label from the current tableau is in the cache.
    The creation of cache entries rapidly becomes difficult with increasing expressivity
of the used DL. Already with blocking for the DL ALC, one can easily generate invalid
cache entries [6]. Apart from a node x with a clash in its label, the question is which
other node labels are also unsatisfiable. For ALC, this is the case for all labels from
x up to the ancestor y with the last non-deterministic expansion. With ALCI, a non-
deterministic rule application on a descendant node of x can be involved in the clash,
which makes it difficult to determine node labels that can be cached. Nevertheless,
caching techniques for ALCI have been proposed [2, 3, 5], but the difficulty further
increases in the presence of nominals and, to the best of our knowledge, the problem
of caching with inverses and nominals has not yet been addressed in the literature. In
order to avoid unsound results, current systems often deactivate caching in presence of
inverse roles or at least in presence of nominals, especially with combined satisfiability
and unsatisfiability caching [14, 17].
    The extraction of a small still unsatisfiable subset of a node label would yield better
cache entries. The use of subset retrieval methods for the cache further increases the
number of cache hits. We call such a technique precise caching. Although techniques
to realise efficient subset retrieval exist [8], unsatisfiability caches that use such subset
retrieval are only implemented in very few DL reasoners [7].
    Going back to the example in Figure 1, for the node x1 the set {¬B, (∃r.(∀r− .B))}
could be inserted into the cache as well as {¬B, (Au(∃r.(∀r− .B)))}. The number of cache
entries should, however, be kept small, because the performance of the retrieval de-
creases with an increasing number of entries. Thus, the insertion of concepts for which
the rule application is cheap (e.g., concept conjunction) should be avoided. Concepts
that require the application of non-deterministic or generating rules are more suitable,
because the extra effort of querying the unsatisfiability cache before the rule applica-
tion can be worth the effort. Optimising cache retrievals for incremental changes further
helps to efficiently handle multiple retrievals for the same node with identical or slightly
extended concept labels.
    The creation of new unsatisfiability cache entries based on dependency tracking
can be done during backtracing, which is also coupled with the dependency directed
backtracking as described next.


3.3   Dependency Backtracing

The dependency tracking defined in Section 2.1 completely retains all necessary infor-
mation to exactly trace back the cause of the clash. Thus, this backtracing is qualified
to identify all involved non-deterministic branching points for the dependency directed
backtracking and also to identify small unsatisfiable sets of concepts that can be used
to create new unsatisfiability cache entries.
    Algorithm 1 performs the backtracing of facts and their tracked dependencies in the
presence of inverse roles and nominals. If all facts and their dependencies are collected
on the same node while backtracing, an unsatisfiability cache entry with these facts can
be generated, assuming all facts are concept facts. As long as no nominal or Abox indi-
vidual occurs in the backtracing, the unsatisfiability cache entries can also be generated
while all concept facts have the same node depth. Thus, an important task of the back-
tracing algorithm is to hold as many facts as possible within the same node depth to
allow for the generation of many cache entries. To realise the backtracing, we introduce
the following data structure:

Definition 5 (Fact Dependency Node Tuple) A fact dependency node tuple for G is a
triple hc, dn,b , xi with c ∈ FactsG , dn,b ∈ DepG and x ∈ V. As abbreviation we also write
hC, dn,b , xi if c is the concept fact C(x).

If a clash is discovered in the completion graph, a set of fact dependency node tuples
is generated for the backtracing. Each tuple consists of a fact involved in the clash, an
associated dependency and the node where the clash occurred. The algorithm gets this
set T of tuples as input and incrementally traces the facts back from the node with the
clash to nodes with depth 0 (Abox individuals or root nodes).
    In each loop round (line 3) some tuples of T are exchanged with tuples, whose facts
are the cause of the exchanged one. To identify which tuple has to be traced back first,
the current minimum node depth (line 4) and the maximum branching tag (line 5) are
extracted from the tuples of T . All tuples, whose facts are located on a deeper node and
whose dependencies are deterministic, are collected in the set A. Such tuples will be
directly traced back until their facts reach the current minimum node depth (line 10-
12). If there are no more tuples on deeper nodes with deterministic dependencies, i.e.,
A = ∅, the remaining tuples from deeper nodes with non-deterministic dependencies
Algorithm 1 Backtracing Algorithm
Require: A set of fact dependency node tuples T obtained from clashes
 1: procedure dependencyBacktracing(T )
 2:    pendingUnsatCaching ← f alse
 3:    loop
 4:       minD ←minimumNodeDepth(T )
 5:       maxB ←maximumBranchingTag(T )
 6:       A ← {t ∈ T | nodeDepth(t)> minD ∧ hasDeterministicDependency(t)}
 7:       C←∅
 8:       if A , ∅ then
 9:            pendingUnsatCaching ← true
10:            for all t ∈ A do
11:                T ← (T \ t) ∪ getCauseTuplesByDependency(t)
12:            end for
13:        else
14:            B ← {t ∈ T | nodeDepth(t)> minD ∧ branchingTag(t)= maxB }
15:            if B = ∅ then
16:                if pendingUnsatCaching = true then
17:                     pendingUnsatCaching ←tryCreateUnsatCacheEntry(T )
18:                end if
19:                if hasNoDependency(t) for all t ∈ T then
20:                     pendingUnsatCaching ←tryCreateUnsatCacheEntry(T )
21:                     return
22:                end if
23:                C ← {t ∈ T | branchingTag(t)= maxB }
24:            end if
25:            t ←anyElement(B ∪ C)
26:            if hasDeterministicDependency(t) then
27:                T ← (T \ t) ∪ getCauseTuplesByDependency(t)
28:            else
29:                b ←getNonDeterministicBranchingPoint(t)
30:                if allAlternativesOfNonDetBranchingPointProcessed(b) then
31:                     T ← T ∪ loadTuplesFromNonDetBranchingPoint(b)
32:                     T ← (T \ t) ∪ getCauseTuplesByDependency(t)
33:                     T ←backtraceTuplesBeforeBranchingPoint(T, b)
34:                     pendingUnsatCaching ←tryCreateUnsatCacheEntry(T )
35:                else
36:                     T ←backtraceTuplesBeforeBranchingPoint(T, b)
37:                     saveTuplesToNonDetBranchingPoint(T, b)
38:                     jumpBackTo(maxB )
39:                     return
40:                end if
41:            end if
42:        end if
43:    end loop
44: end procedure
and the current branching tag are copied into B (line 14) in the next round. If B is not
empty, one of these tuples (line 25) and the corresponding non-deterministic branching
point (line 29) are processed. The backtracing is only continued, if all alternatives of
the branching point are computed as unsatisfiable. In this case, all tuples, saved from
the backtracing of other unsatisfiable alternatives, are added to T (line 31). Moreover,
for c the concept fact in the tuple t, t can be replaced with tuples for the fact on which
c non-deterministically depends (line 32).
    For a possible unsatisfiability cache entry all remaining tuples, which also depend
on the non-deterministic branching point, have to be traced back until there are no tuples
with facts of some alternatives of this branching point left (line 33). An unsatisfiability
cache entry is only generated (line 34), if all facts in T are concept facts for the same
node or on the same node depth.
    Unprocessed alternatives of a non-deterministic branching point have to be com-
puted before the backtracing can be continued. It is, therefore, ensured that tuples do
not consist of facts and dependencies from this alternative, which also allows for re-
leasing memory (line 36). The tuples are saved to the branching point (line 37) and the
algorithm jumps back to an unprocessed alternative (line 38).
    If B is also empty, but there are still dependencies to previous facts, some tuples
based on the current branching tag have to remain on the current minimum node depth.
These tuples are collected in the set C (line 23) and are processed separately one per
loop round, similar to the tuples of B, because the minimum node depth or maximum
branching tag may change. The tuples of C can have deterministic dependencies, which
are processed like the tuples of A (line 27). If all tuples have no more dependencies to
previous facts, the algorithm terminates (line 21).
    Besides the creation of unsatisfiability cache entries after non-deterministic depen-
dencies (line 34), cache entries may also be generated when switching from a deeper
node to the current minimum node depth in the backtracing (line 9 and 17) or when the
backtracing finishes (line 20). The function that tries to create new unsatisfiability cache
entries (line 17, 20, and 34) returns a Boolean flag that indicates whether the attempt
has failed, so that the attempt can be repeated later.
    For an example, we consider the clash {¬B, B} in the completion graph of Figure 1.
The initial set of tuples for the backtracing is T 1 (see Figure 2). Thus, the minimum node
depth for T 1 is 1 and the maximum branching tag is 0. Because there are no tuples on a
deeper node, the sets A and B are empty for T 1 . Since all clashed facts are generated de-
terministically, the dependencies of the tuples have the current maximum branching tag
0 and are all collected into the set C. The backtracing continues with one tuple t from
C, say t = hB, k11,0 , x1 i. The dependency k of t relates to the fact (∀r− .B)(x2 ), which is a
part of the cause and replaces the backtraced tuple t in T 1 . The resulting set T 2 is used in
the next loop round. The minimum node depth and the maximum branching tag remain
unchanged, but the new tuple has a deeper node depth and is traced back with a higher
priority to enable unsatisfiability caching again. Thus, h(∀r− .B), i9,0 , x2 i is added to the
set A and then replaced by its cause, leading to T 3 . Additionally, a pending creation
of an unsatisfiability cache entry is noted, which is attempted in the third loop round
since A and B are empty. The creation of a cache entry is, however, not yet sensible
and deferred since T 3 still contains an atomic clash. Let t = hB, j10,0 , x1 i ∈ C be the
          T 1 = {h¬B, d4,0 , x1 i, h¬B, e5,0 , x1 i, hB, j10,0 , x1 i, hB, k11,0 , x1 i}
            ↓
          T 2 = {h¬B, d4,0 , x1 i, h¬B, e5,0 , x1 i, hB, j10,0 , x1 i, h(∀r− .B), i9,0 , x2 i}
            ↓
          T 3 = {h¬B, d4,0 , x1 i, h¬B, e5,0 , x1 i, hB, j10,0 , x1 i, h(∃r.(∀r− .B)), g7,0 , x1 i}
            ↓
          T 4 = {h¬B, d4,0 , x1 i, h¬B, e5,0 , x1 i, hr(x1 , x2 ), h8,0 , x1 i, h(∃r.(∀r− .B)), g7,0 , x1 i}
            ↓
          T 5 = {h¬B, d4,0 , x1 i, h¬B, e5,0 , x1 i, h(∃r.(∀r− .B)), g7,0 , x1 i}
            ↓
          T 6 = {h¬B, d4,0 , x1 i, h(∀r.¬B), −, a0 i, h(∃r.(∀r− .B)), g7,0 , x1 i}
            ↓
          T 7 = {hr(a0 , x1 ), b2,0 , x1 i, h(∀r.¬B), −, a0 i, h(A u (∃r.(∀r− .B))), c3,0 , x1 i}
            ↓
          T 8 = {h(∃r.(A u (∃r.(∀r− .B))))−, a0 i, h(∀r.¬B), −, a0 i}

          Fig. 2. Backtracing sequence of tuples as triggered by the clash of Figure 1


tuple from T 3 that is traced back next. In the fourth round, the creation of a cache entry
is attempted again, but fails because not all facts are concepts facts. The backtracing
of hr(x1 , x2 ), h8,0 , x1 i then leads to T 5 . In the following round an unsatisfiability cache
entry is successfully created for the set {¬B, (∃r.(∀r− .B))}. Assuming that now the tuple
h¬B, e5,0 , x1 i is traced back, we obtain T 6 , which includes the node a0 . Thus, the mini-
mum node depth changes from 1 to 0. Two more rounds are required until T 8 is reached.
Since all remaining facts in T 8 are concept assertions, no further backtracing is possible
and an additional cache entry is generated for the set {(∃r.(A u (∃r.(∀r− .B)))), (∀r.¬B)}.
     If a tuple with a dependency to node a0 had been traced back first, it would have
been possible that the first unsatisfiability cache entry for the set {¬B, (∃r.(∀r− .B))}
was not generated. In general, it is not guaranteed that an unsatisfiability cache entry
is generated for the node where the clash is discovered if there is no non-deterministic
rule application and if the node is not a root node or an Abox individual. Furthermore,
if there are facts that are not concept facts, these can be backtraced with higher priority,
analogous to the elements of the set A, to make unsatisfiability cache entries possible
again. To reduce the repeated backtracing of identical tuples in different rounds, an
additional set can be used to store processed tuples for the alternative for which the
backtracing is performed.
     The backtracing can also be performed over nominal and Abox individual nodes.
However, since Abox and absorbed nominal assertions such as {a} v C have no previous
dependencies, this can lead to a distributed backtracing stuck on different nodes. In this
case, no unsatisfiability cache entries are possible.
     A less precise caching can lead to an adverse interaction with dependency directed
backtracking. Consider the example of Figure 3, where the satisfiability of the combina-
tion of the concepts (∃r.(∃s.(AuB))), ((C1 u∀r.C)t(C2 u∀r.C)), and ((D1 u∀r.(∀s.¬A))t
(D2 u∀r.(∀s.¬A))) is tested. Note that, in order to keep the figure readable, we no longer
show complete dependencies, but only the branching points for non-deterministic deci-
sions. First, the two disjunctions are processed. Assuming that the alternative with the
disjuncts (C1 u ∀r.C) and (D1 u ∀r.(∀s.¬A)) is considered first (shown on the left-hand
side of Figure 3), an r-successor x1 with label {(∃s.(A u B)), C 1 , (∀s.¬A)2 } is gener-
ated. The branching points indicate which concepts depend on which non-deterministic
          L(x0 ) = {(∃r.(∃s.(A u B))), ((C1 u ∀r.C) t (C2 u ∀r.C)),
                                                                              b. backjumping
          ((D1 u ∀r.(∀s.¬A)) t (D2 u ∀r.(∀s.¬A)))}
                                                                x0
                                                 t1                           t1
    L(x0 ) ∪ {(C1 u ∀r.C)1 }      x0                                                           x0
                 t2                             t2
 x0                                                          x0       L(x0 ) ∪ {(D2 u
           L(x0 ) ∪ {(D1 u ∀r.(∀s.¬A))2 }
                                                                       ∀r.(∀s.¬A))2 }
     r                                                        r                         a. backjumping

                                                                   a. entire label cached,
 x1       L(x1 ) = {(∃s.(A u B)), C 1 , (∀s.¬A)2 }           x1
                                                                      dependency set {1, 2}
      s                                        backjumping
                                                                  b. concepts precisely cached,
 x2       L(x2 ) = {(A u B), A, B, ¬A }2                             dependency set {2}
          clash {A, ¬A}, dependency set {2}

Fig. 3. More pruned alternatives due to dependency directed backtracking and precise caching
(case b.) in contrast to label caching (case a.)


decision. For example, C is in L(x1 ) due to the disjunct (C1 u ∀r.C) of the first non-
deterministic branching decision (illustrated in Figure 3 with the superscript 1). In
the further generated s-successor x2 a clash is discovered. For the only involved non-
deterministic branching point 2, we have to compute the second alternative. Thus, an
identical r-successor x1 is generated again for which we can discover the unsatisfia-
bility with a cache retrieval. If the entire label of x1 was inserted to the cache, the
dependent branching points of all concepts in the newly generated node x1 would have
to be considered for further dependency directed backtracking. Thus, the second alter-
native of the first branching decision also has to be evaluated (c.f. Figure 3, case a.,
label caching). In contrast, if the caching was more precise and only the combination of
the concepts (∃s.(A u B)) and (∀s.¬A) was inserted into the unsatisfiability cache, the
cache retrieval for the label of node x1 would return the inserted subset. Thus, only the
dependencies associated to the concepts of the subset could be used for further back-
jumping, whereby it would not be necessary to evaluate the remaining alternatives (c.f.
Figure 3, case b., precise caching).


4         Evaluation
Our Konclude reasoning system implements the enhanced optimisation techniques for
SROIQ described above. We evaluate dependency directed backtracking and unsatis-
fiability caching with the help of concept satisfiability tests from the well-known DL
98 benchmark suite [10] and spot tests from [12]. An extended evaluation and a com-
parison of Konclude with other reasoners can be found in the accompanying technical
report [15]. From the DL 98 suite we selected satisfiable and unsatisfiable test cases
(with _n resp. _p postfixes) and omitted those for which unsatisfiability caching is ir-
relevant and tests that were too easy to serve as meaningful and reproducible sample.
processed alternatives                                  precise caching   label caching   without caching


 100000



    10000



     1000



     100




       Fig. 4. Log scale comparison of processed alternatives for different caching methods


    We distinguish between precise caching and label caching as described in Sec-
tion 3.2. To recall, precise caching stores precise cache entries consisting of only those
backtraced sets of concepts that are explicitly known to cause an unsatisfiability in com-
bination with subset retrieval, while label caching stores and returns only entire node
labels.
    Konclude implements precise unsatisfiability caching based on hash data struc-
tures [8] in order to efficiently facilitate subset cache retrieval. Figure 4 shows the total
number of processed non-deterministic alternatives for precise caching, label caching
and without caching for a selection of test cases solvable within one minute.
    Note that runtime is not a reasonable basis of comparison since the label caching
has been implemented (just for the purpose of evaluation) on top of the built-in and
computationally more costly precise caching approach. System profiling information,
however, strongly indicate that building and querying the precise unsatisfiability cache
within Konclude is negligible in terms of execution time compared to the saved pro-
cessing time for disregarded alternatives. However, we have experienced an increase of
memory usage by a worst-case factor of two in case of dependency tracking in compar-
ison to no dependency handling.
    Figure 4 reveals that precise caching can, for some test cases, reduce the number
of non-deterministic alternatives by two orders of magnitude in comparison to label
caching. Particularly the test cases k_path_n/p are practically solvable for Konclude
only with precise caching for larger available problem sizes.


5     Conclusions

We have presented an unsatisfiability caching technique that can be used in conjunction
with the very expressive DL SROIQ. The presented dependency management allows
for more informed backjumping, while also supporting the creation of precise cache
unsatisfiability entries. In particular the precise caching approach can reduce the num-
ber of tested non-deterministic branches by up to two orders of magnitude compared
to standard caching techniques. The optimisations are well-suited for the integration
into existing tableau implementations for SROIQ and play well with other commonly
implemented optimisation techniques.

References
 1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The De-
    scription Logic Handbook: Theory, Implementation, and Applications. Cambridge Univer-
    sity Press, second edn. (2007)
 2. Ding, Y., Haarslev, V.: Tableau caching for description logics with inverse and transitive
    roles. In: Proc. 2006 Int. Workshop on Description Logics. pp. 143–149 (2006)
 3. Ding, Y., Haarslev, V.: A procedure for description logic ALCF I. In: Proc. 16th Euro-
    pean Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TAB-
    LEAUX’07) (2007)
 4. Donini, F.M., Massacci, F.: EXPTIME tableaux for ALC. J. of Artificial Intelligence 124(1),
    87–138 (2000)
 5. Goré, R., Widmann, F.: Sound global state caching for ALC with inverse roles. In: Proc.
    18th European Conf. on Automated Reasoning with Analytic Tableaux and Related Methods
    (TABLEAUX’09). LNCS, vol. 5607, pp. 205–219. Springer (2009)
 6. Haarslev, V., Möller, R.: Consistency testing: The RACE experience. In: Proceedings, Auto-
    mated Reasoning with Analytic. pp. 57–61. Springer-Verlag (2000)
 7. Haarslev, V., Möller, R.: High performance reasoning with very large knowledge bases: A
    practical case study. In: Proc. 17th Int. Joint Conf. on Artificial Intelligence (IJCAI’01). pp.
    161–168. Morgan Kaufmann (2001)
 8. Hoffmann, J., Koehler, J.: A new method to index and query sets. In: Proc. 16th Int. Conf. on
    Artificial Intelligence (IJCAI’99). pp. 462–467. Morgan Kaufmann (1999)
 9. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc. 10th Int.
    Conf. on Principles of Knowledge Representation and Reasoning (KR’06). pp. 57–67. AAAI
    Press (2006)
10. Horrocks, I., Patel-Schneider, P.F.: DL systems comparison. In: Proc. 1998 Int. Workshop on
    Description Logics (DL’98). vol. 11, pp. 55–57 (1998)
11. Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. of Logic
    and Computation 9(3), 267–293 (1999)
12. Liebig, T.: Reasoning with OWL – system support and insights –. Tech. Rep. TR-2006-04,
    Ulm University, Ulm, Germany (September 2006)
13. Liebig, T., Steigmiller, A., Noppens, O.: Scalability via parallelization of OWL reasoning.
    In: Proc. Workshop on New Forms of Reasoning for the Semantic Web: Scalable & Dynamic
    (NeFoRS’10) (2010)
14. Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL rea-
    soner. J. of Web Semantics 5(2), 51–53 (2007)
15. Steigmiller, A., Liebig, T., Glimm, B.: Extended caching, backjumping
    and merging for expressive description logics. Tech. Rep. TR-2012-01,
    Ulm University, Ulm, Germany (2012), available online at http://www.uni-
    ulm.de/fileadmin/website_uni_ulm/iui/Ulmer_Informatik_Berichte/2012/UIB-2012-01.pdf
16. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Proc.
    3rd Int. Joint Conf. on Automated Reasoning (IJCAR’06). LNCS, vol. 4130, pp. 292–297.
    Springer (2006)
17. Tsarkov, D., Horrocks, I., Patel-Schneider, P.F.: Optimizing terminological reasoning for ex-
    pressive description logics. J. of Automated Reasoning 39, 277–316 (2007)