Recently, modular techniques have been employed for optimising Description Logic reasoning, speci cally to enable incremental reasoning and improve overall classi cation time. Classifying a module of an ontology should be signi cantly easier than reasoning in the whole ontology. However, we observed in previous work that neither it is generally true that modular reasoning techniques have a reliable positive e ect, nor even that the classi cation time of a module is less than or equal to the classi cation time of the whole ontology. One possible explanation for the latter could be that counter-productive optimisations are triggered within the reasoner when dealing with the sub-module, and thus individual subsumption tests get harder when parts of the ontology are missing. The goal of this paper is to understand the contribution of subsumption tests to the hardness of classi cation. The contribution is twofold: (1) We analyse the impact of subsumption test hardness on DL classi cation by analysing a well known corpus of ontologies, and (2) we present a novel approach based on modularity to robustly detecting subsumption tests that are too hard.
Reasoning in popular, very expressive Description Logics (DL) is very di cult
(e.g., SROIQ is N2Exptime-complete) [
Using locality-based modules to optimise Description Logic classi cation
experienced a resurgence in recent years [
The goal of this paper is to understanding the contribution of subsumption
tests (ST) to the hardness of classi cation. The contribution is twofold: (1)
We analyse the impact of ST hardness on DL classi cation by characterising
a well known corpus of ontologies, and (2) we present a novel approach based
on modularity to robustly detecting subsumption tests that are potentially too
hard. As a result, we re-con rm the almost 20 years old results by Horrocks [
Understanding the experimental design and methodology presented here does
not require more than a cursory understanding of the syntax, semantics, and
proof theories implemented. The most prominent families of reasoning algorithms
for description logics are tableau (incl. hyper-tableau) and consequence-based. In
our work, we are mainly concerned with tableau-based algorithms. The
reasoners under investigations in this paper are designed to implement key reasoning
services for the Web Ontology Language (OWL), most importantly classi cation
and consistency checking. Given an ontology (a set of axioms) O, the signature
of an ontology Oe is the set names appearing in the axioms in O. We use CT (O)
(classi cation time) and CT (M) respectively to denote the time of computing
the set of atomic subsumptions (i.e., statements of the form A v B where A and
B are properties or classes in the signature) or classi cation of O. For brevity,
we refer to overall classi cation time as OCT and subsumption test time as STT.
While subsumption testing, and therefore classi cation, is in theory intractable,
highly optimised reasoners do fairly well in practice. The observed e ciency
despite the worst case complexity is in principle down to four factors. (1) Real
ontologies are bounded in size. That means that even an exponential algorithm
might fully classify an ontology, from a user perspective, in an acceptable amount
of time. (2) Many ontologies fall into tractable fragments of OWL, and can be
classi ed using e cient polynomial algorithms such as the ones from the family
of consequence-based algorithms. (3) The last 20 years brought a plethora of
di erent optimisations to make satis ability checks easier [
Current modular classi cation approaches use so-called syntactic
localitybased ?-modules [
Very recently, reasoner developers have started to utilise modularity for
classi cation. They either are (1) using modules for incremental reasoning [
Attempts to understand DL reasoning performance are, up until today, rarely
systematic or comprehensive. Recently, the ORE reasoner competition tries to
establish the methodological foundations for more reliable comparisons [
The phenomenon under investigation is subsumption test hardness in the context of classi cation. A subsumption test is a question asked by the reasoner to determine whether A v B. The subsumption test hardness is the time it takes to compute the answer, operationalised as wall-clock time. In this work the answer to a test is either yes or no. Note however, that for any implementation (1) more than just a binary answer will be provided (i.e., cached models, derived subsumptions) and (2) no guarantee is given that the answer is correct (bugs in the reasoner). \In the context of classi cation" means that we are not exploring individual \cold" tests, i.e. letting the reasoner compute whether A v B for any A; B from outside the classi cation process, because we want to understand the contribution of subsumption testing to classi cation as a whole, with all the optimisations involved.
Our model of subsumption test hardness with respect to sub-modules is based on the following intuition: Given a positive ST ST , it should be the case that for every two modules M1,M2 with M1 M2 O in which the ST is triggered, the hardness of ST always stays the same. The reason for that are module properties: every justi cation for an entailment is part of every module that entails it. Thus, every way that the entailment holds is contained in the module, no \new" information about the entailment exists in the rest of the ontology. Intuitively, additional \stu " can make it harder to gure out the entailment, but not make it easier. This makes this metric a possible indicator of counter-productive optimisations: If we nd that ST M2 is harder than ST M1 , we might conclude that the reasoner is doing some unnecessary extra work in M2 (case 1); if ST M1 is harder than ST M2 , there is a possibility that a counterproductive optimisation may have been triggered (case 2). Only the second case is truly pathological: A test should never get harder when irrelevant axioms are removed from the ontology. The rst case might simply occur because if M grows, it gets harder to identify the irrelevant axioms. One possibility to explain both cases may be the inherent stochasticity of classi cation as implemented by current OWL Reasoners. For example, a random factor might (for example by changing the test order) simply shift the load of ST in M1 to another ST ST 2 that consecutively makes ST easier. Another reason for a test becoming easier in a sub-module might be the exploitation of partial results from negative tests (e.g. caching).
Our empirical investigation of subsumption tests has two parts: (A) a broad characterisation of the landscape of subsumption testing and (B) an in-depth characterisation of non-easy subsumption tests. We treat a test as non-easy if it takes longer than 100 ms . The rst part A will attempt to answer the following questions: What is the impact of subsumption testing on reasoning performance in general (RQ1)? How many tests are positive or negative and how do they di er in hardness (RQ2)? How hard are real tests actually (RQ3)?
Part B serves as an in-depth characterisation that attempts to address questions related to the general stability of the measurements (intra-module) and the e ect of modularity (inter-module). Is ST hardness a stable phenomenon (RQ4)? This is important in order to judge how reliably we can trace a single subsumption test through di erent sub-modules of an ontology, and may also give a warning sign for triggered non-determinism, for example in the case that a test appears or disappears given a particular ontology-reasoner pair across runs. We will address this problem mainly by looking at the coe cient of variation (COV) of subsumption test hardness. The COV is a statistical, standardised measure of dispersion of a distribution (for example the distribution of test hardness) dened as the ratio of the standard deviation to the mean and is used to compare the variation of one data series to another, even if they are on a di erent scale. What are the reasons for instability (RQ5)? We will not conclusively try to answer this problem, but we will collect some evidence for stochasicity by looking at intra-module variation of test counts, a strong indicator of non-determinism.
Does modularity change the hardness of tests (RQ6)? In order to answer this question, we will classify tests by analysing how modularity a ects their hardness. This happens as follows: We identify all super and submodule combinations M1; M2 as described earlier. For each test triggered in both M1 and M2, we determine: (1) was the e ect positive on average (across runs), (2) what was the magnitude of the e ect and (3) was the e ect stable? We de ne stability of an e ect as follows: given a subsumption test ST that occurs in two modules M1; M2 with M1 M2, and two sets of measurements X(ST M1 ) and X(ST M2 ) (a) measurements M E 2 X(ST M1 ) are either all harder or all easier than measurements M E 2 X(ST M2 ) (strong stability) or (b) the overlap of the ranges of X(ST M1 ) and X(ST M2 ) is less than 10% of the range of X(ST M1 ) u X(ST M1 ).
We group ST hardness into the following bins: Very Hard (more than 100 seconds), Hard (>10 sec), Medium Hard (>1 sec), Medium (>100 ms), Medium Easy (>10 ms), Easy (>1 ms), Very Easy (>100 s.), Trivial (<100 s). The upper bound of each bin corresponds to the lower bound of the previous one. 5
We conducted our study on a corpus of 339 OWL API (3.5.0)-parsable BioPortal ontologies, obtained through the BioPortal REST Services1 (January 2015 snaphshot). All ontologies were serialised into OWL/XML, with merged imports closure. A minimum amount of repair (injecting missing declarations, dropping empty n-ary axioms, etc.) was applied to ensure that trivial violations do not impair DLness.
For all our experiments, we use four OWL reasoners that implement the OWL API interface: HermiT 1.3.8, Pellet 2.3.1, JFact 1.2.3 and FaCT++ 1.6.3. All four are among the most heavily used reasoners for OWL 2 DL. The reasoners have been modi ed for the benchmark: When a subsumption test is conducted, the start and end timestamps, the sub and super class under consideration and the result of the test are recorded. While we can use this approach to compare results for each reasoner, interpretation of comparisons between reasoners might be misleading due to implementational details. For example, methods that test for subsumption and ultimately satis ability may be nested. See companion website for more information (Section 6). Because we are interested in real life behaviour, we allowed the reasoner to fall into states like the deterministic part of HermiT for Horn-SHIQ or Pellets internal EL-Reasoner. That said, we cannot claim to measure all subsumption tests a reasoner does. We can, however, establish a lower bound and are con dent that we capture the vast majority of the hard tests, because the sum of test times occasionally account for almost 100% of the OCT for all reasoners.
A set of four equal-spec Mac Minis with Mac OS X Lion 10 (64 bit), 16 GB RAM and 2.7 GHz Intel Core i764-bit was used for the benchmarking. Every single classi cation was done in a separate isolated virtual machine (Java 7, -Xms2G, -Xmx12G). In order to reduce potential bias induced by run order (unaccounted for background processes kicking in, runtime optimisations), we fully randomise the run order and evenly distribute the experiment run jobs across the four machines.
Experimental Pipeline: For the rst experiment we execute a single run of all reasoners across the entire corpus, with a timeout of 60 minutes per run. Due to technical details, the timeout is a lower bound and might not be triggered until some minutes later. Note that we include every ontology in the corpus, including the ones not strictly in OWL DL (53). The reason for that is that these ontologies do form part of the landscape, and reasoners are used on them. The main sources of violations are uses of reserved vocabulary (37% of all violations across the corpus), illegal punning (32%) and uses of datatypes not on the OWL 2 datatype map (11%).
For the second experiment, we select a set of reasoner-ontology pairs for
which, according to the results of experiment 1, at least one test was measured
that was harder than 100 milliseconds. Because of the various claims we have
with respect to modules, we also excluded ontologies that do not fall under
OWL 2 DL. Runtime limitations forced us to exclude the NCIt from the sample,
due to the extreme number of measured subsumption tests (JFact 751,907 tests,
Pellet 461,831, FaCT++ 605,481). For this experiment, we rst obtain random
cumulative subsets from the ontologies in our narrowed down sample, similar to
Goncalves et al. [
Supporting materials, datasets and scripts can be found online2. Percentages in this section are subject to appropriate rounding. 6.1
Out of the 1356 attempted classi cation runs (4 reasoners and 339 ontologies), 1136 (85%) completed successfully. 322 ontologies were dealt with by at least one reasoner (95%) within the 60 minute timeout. Reasons for failure include hitting the timeout, unsupported datatypes (FaCT++), and lack of DLness (mainly HermiT). From the 322 ontologies successfully processed, 186 did not have any subsumption tests measured by any of the three reasoners. By reasoner, FaCT++ did not test in 177 cases, HermiT in 189, JFact in 191 and Pellet did not re a ST during 218 successful classi cations. For the remaining 136, at least one reasoner conducted a ST as described in Section 5. One interesting observation 100000 1000
10 100000 1000 10
T VE E MEMDMH H VH T VE E MEMDMH H VH T VE E MEMDMH H VH T VE E MEMDMH H VH is that most positive tests are of only trivial hardness, while negative tests are generally harder. While subsumption testing dominates the OCT only in a few cases, it occasionally accounts for more than 80%. Very rarely we can observe a single test accounting for more than 10% of the OCT. The maximum impact for a single test by Pellet is 11.3%, HermiT 23.1%, JFact 24.8% and FaCT++ 9.2%. The distribution of subsumption test hardness across all runs according to our hardness scale (Sec. 4) is shown in Figure 1.
6.2
From the previous experiment, according to the process detailed in Section 5, 3 ontologies were selected for FaCT++, 13 for HermiT, 5 for JFact and 4 for Pellet. The full ontologies have OCT's ranging from 7.31 seconds to 1211.00 seconds (median: 103.20, mean: 210.70). Out of the 1200 (16 modules per ontology, 3 runs per module, 25 ontology reasoner pairs) attempted classi cations (timeout 60 minutes), 1093 (91%) successfully terminated. Out of the possible 400 modules (16 modules, 25 ontology-reasoner pairs) across the entire set, we obtain 371 records from the intra-module analysis, 358 out of which were obtained from three distinct measurements, 6 are comprised of two distinct measurements and 7 by only one. Since we are interested in observing variability, we discard the latter 7 and stick with 364 partially or fully complete records. Variability is determined using the coe cient of variation (COV). From the module perspective, we look at three distinct sources of variation: overall classi cation time (OCT), sum of all subsumption test times (SUMST) and the total number of tests conducted (CTT). Across modules, only 3 module OCT varies by more than 30%, 12 by more than 20% and 19 by more than 10%. The module with the worst variation corresponds to a module taken from a 126 th of the Biotop ontology, classi ed by JFact (min=38.49 sec, max=194.22 sec). A more detailed picture of the overall variation can be taken from Figure 2. In terms of test count, the variation is surprisingly large. 246 out of 364 cases (68%) show di erences in the number of test measured across runs. Only 118 (32%) do not vary at all. 20 modules vary by more than 10% in the number of subsumption tests.
Across all 371 modules, we measured the hardness of 2,536,339 distinct ST's. Only 89% of the tests are measured more than once and we discard the rest. As can be seen in Figure 2, the coe cient of variation is generally log10-normally distributed (here reported in percent rather than in proportions of 1), but varies considerably across reasoners. On average, measurements deviate as much as 13.22% and 13.96% for Pellet and HermiT respectively, while measurements for and JFact deviate by 3.5%, and FaCT++ only 2.83%. The maximum variation for any test measurement for Pellet is 172.65%, for HermiT 172.50%, for FaCT++ 167.87% and for JFact 169.07%.
For the inter-module analysis, we sampled 30 sub-module super-module pairs from P from the 120 possible combinations as described in Section 5. Taking into account the successful classi cation we obtained data from 703 out of 750 possible comparisons. For result stability, we excluded a further 14 pairs that had only a single measurement for either the sub or the super-module, and continued with 689. Figure 3 shows the overall changes in measurement times across pairs by reasoner. Bin membership is determined as follows. Given a pair <M1; M2>2 P we look at the change from either the CT (M1) to CT (M2) or the change from a subsumption test ST M1 to ST M2 . Every pair of measurements has a tendency, a magnitude and a degree of stability. The tendency easier (mean hardness change less than -5%) denotes that a test is easier in the super-module (potentially pathological), harder (mean hardness change more than 5%) the reverse, and neutral means the mean measurement di erence does Fact++[EXP]
HermiT[EXP] not change by more than 5%. High magnitudes are changes above 50%, medium magnitudes are changes between 5% and 50% and low changes are below 5%. An e ect can be of three degrees of stability: clear cut, high or low, see Section 4. Neutral cases have high stability if both sets of measurements have a variation coe cient less than 5%. From the module perspective, the main observation to be made here is that there are 39 cases in the set where the sub-module is harder than the super-module and 173 where there is no signi cant change in hardness (less than 5% change). Test time stability varies a lot across reasoners. While FaCT++ measurements are mostly stable, Pellet and JFact measurements vary a lot across almost all potential categories. The pathological cases as described in Section 4, EHC and EHH, occur rarely. Out of the 1,507,654 tests that got easier overall, only 399,644 (26%) are of a high magnitude. Out of those, 376,078 are clear cut, and 8,850 of high stability. From the clear cut cases, 59,656 are potentially una ected by non-determinism, out of which 204 are harder than 100 ms. Out of the highly stable cases, only 302 are potentially una ected by non-determinism, out of which only 10 are harder than 100ms. None of the tests in both groups are harder than a second. 7
We quantify the impact of subsumption test hardness (RQ1) on classi cation time in two ways: (1) Contribution of test times measured to OCT and (2) ratio of number of ontologies with tests to those without. Only few of the 136 ontologies with tests were dominated by test hardness: Only 1 ontology had more than a 50% contribution of total SST for Hermit, 7 for Pellet, 19 for FaCT++ and 23 for JFact. However, there are cases where the contribution is very high. The ratio of ontologies entirely without tests is very high: FaCT++: 52%-71%, HermiT 55%-80%, JFact in 56%-76% and Pellet 64%-84%. We have established only the lower bound. The upper bound covers the very unlikely possibility that the failed classi cations might be all without tests. Additionally, 36 of the
Fact++[EXP]
RQ2 is quanti ed by ratio of positive to negative tests. Positive tests account to between 0.12% (Pellet) and 2.61% (FaCT++) of the overall number of tests (JFact 2.49%, HermiT 2.12%). This low ratio is not surprising, given that the worst case N 2 is dominated by far by non-subsumptions. As a side observation, current traversal algorithms appear highly e cient. Only 3 ontology-reasoner pairs (two distinct ontologies, small TBoxes) trigger more than 10% of the worst case N 2 number of subsumption tests, and 50 pairs (30 unique ontologies) trigger more than 1% of the worst case. This result however is only indicative of the e ciency, as we do not guarantee to measure all tests.
The distribution of test hardness as shown in Figures 1 tends towards easy tests (RQ3). Figure 1 show that the number of really hard tests are in the minority: only 346 out of 2,671,896 tests measured overall are harder than a second. This result may emphasise the importance of test avoidance over further optimising individual subsumption tests. However, as there are individual tests that can make up to 25% of the overall reasoning time, it cannot be disregarded.
The variation of the measurements, both for individual tests and overall times, is, at least in its magnitude, surprising (RQ4). While the variation of test times could be so high merely due to the low number of measurements that are very vulnerable to experimental error (for example an unaccounted for system background kicking in, stochasticity in the garbage collection, room temperature), we cannot claim the same for the variation in the numbers of triggered tests. That 68% of the modules in the sample vary in the number of tests is a very strong indicator for the stochasticity of the classi cation process (at least in this particular sample), be it due to random e ects in the programming language or deliberate randomness induced by the implementation. This poses a serious threat for single-run benchmarking, as it is still general practice in the DL community. A small indication of the potential impact of a particular programming environment is the very low average variation in test times collected for FaCT++, which is the only reasoner in the set implemented in C++. In the inter-module comparison we learned that our pathological cases rarely happen and if so, the e ect they might have on overall classi cation time is negligible, due to the potential degree of the e ect and the rarity in which they occur. Furthermore, the strong evidence of stochasticity of the classi cation process makes it unclear whether the e ect might not simply be due to non-determinism. Despite having detected some cases that are clearly counter-intuitive (in the sense of getting easier when irrelevant stu is added in), we cannot be sure whether modularity is the cause, due of the small e ect size (RQ6). On top of that, easier and harder tests almost balance each other out. Given our sample bias, our results are not conclusive. 8
In this paper we have presented a procedure for reliable and reproducible isolation of counter-intuitive reasoning behaviour on subsumption tests during classi cation and presented some such isolated cases. Future work includes completing the full characterisation of the corpus with respect to the pathological cases and then investigating the causal basis of those cases. The most likely explanation is that the additional axioms trigger a cheaper choice in the complex non-determinism algorithms. The big challenge is whether any progress can be made in a fairly reasoner independent way. One idea is to extract the justi cations for a given entailment and see whether they are disproportionally di cult individually. This would suggest that the additional information is directing the algorithm toward \easier" reasoners.