We investigate an application of the MergeXplain algorithm on ABox abduction. This approach was recently proposed to address computational limitations of more traditional approaches, such as Reiter's Minimal Hitting Set algorithm. MergeXplain uses divide and conquer to search through the space of possible explanations more quickly, however this comes at a cost, as it is not complete. In this paper, we report on our preliminary experimental evaluation of both approaches in the context of finding explanations of ABox abduction problems in description logics. Finally, we also investigate how to combine both approaches in order to leverage on the improved effectivity of MergeXplain and still retain completeness.
Abduction explains why some observation does not follow from a knowledge base (KB).
This problem was originally introduced by Peirce [
Multiple existing works adopted Reiter’s Minimal Hitting Set algorithm [19]
exploiting a DL reasoner for satisfiability checking. This was proposed by Halland and Britz
[
The main advantage of Reiter’s algorithm is its completeness. Also, thanks to
properties of breath-first search it finds smaller explanations first [
However, completeness is not necessarily required. In some applications it may be
sufficient to find just one explanation. For such scenarios Junker [
In this work we report on our experiments with MXP-based abduction. We have implemented both methods (MHS and MXP) into an ABox abduction solver. Our implementation calls DL reasoners as a black box using OWL API similarly to Mrózek et Concept
Syntax
Semantics Atomic concept A complement C intersection C à D existential restriction ÇR:C nominal ^a`
AI
I ä CI CI ã DI ^x Ý Çy .x; y/ Ë RI á y Ë CI ` ^aI ` Axiom concept incl. (GCI) role incl. (RIA) concept assertion role assertion neg. role assertion
Syntax C Þ D R Þ S
Semantics CI Ó DI
RI Ó SI
C.a/ aI Ë CI
R.a; b/ .aI ; bI / Ë RI
R.a; b/ .aI ; bI / Ì RI
al. [
We have conducted a preliminary experimental evaluation with two use cases. In the first, simpler use case we focused on explanations of size one. While MXP is incomplete in general, it is guaranteed to find all explanations of size one in a single run, hence such a comparison is interesting. In the second use case we did not limit the size of explanations. We simply set a timeout (of 12 hours) and compared the number of explanations found by each approach.
Our evaluation shows that in cases when one is only interested in explanations of size one MHS is more effective. In cases when larger explanations cannot be ruled out of consideration MXP was able to find over 80 % of explanations found by MHS before the timeout expired.
Finally, we have also investigated a combined approach, in which MXP is run repeatedly and MHS is used to steer this process in order to achieve completeness. We present the resulting algorithm. Empirical evaluation of this approach is subject to our ongoing work. 2
For simplicity we will introduce ALCHO [
An interpretation is a pair I = . I ; I /, where I ç is a domain, and the interpretation function I maps each individual a Ë NI to aI Ë I , each atomic concept A Ë NC to AI Ó I , each role R Ë NR to RI Ó I I in such a way that the interpretation of any complex concept is as given on the right-hand side of Table 1.
An interpretation I satisfies an axiom ' (denoted I ô ') if the respective constraint in Table 1 is satisfied. It is a model of a KB K (denoted I ô K) if I ô ' for all ' Ë K. A KB K is consistent, if there is at least one interpretation I such that I ô K. K entails an axiom ' (denoted K ô ') if I ô ' for each I ô K.
Finally, we define ' := C.a/ if ' = C.a/; ' := C.a/ if ' = C.a/; ' := R.a; b/ if ' = R.a; b/; ' := R.a; b/ if ' = R.a; b/.
In ABox abduction [
ABox abduction problem is a pair P = .K; O/ such that K is a knowledge base in DL and O is an ABox assertion. A solution of P (also called explanation) is any finite set E Ó Abd of ABox assertions such that K ä E ô O.
While Definition 1 establishes the basic reasoning mechanism of abduction, some of
the explanations it permits may be unintuitive. According to Elsenbroich et al. [
Indeed an explanation should be consistent, as anything follows from inconsistency; and so, an explanation that makes K inconsistent does not really explain the observation. It should be relevant – it should not imply the observation directly without requiring the KB K at all. And it should be explanatory, that is, we should not be able to explain the observation without it.
Only explanations which satisfy all three of the above conditions will be called desired. In addition, in order to avoid excess hypothesizing, minimality is required. Definition 2 (Minimality). Assume an ABox abduction problem P = .K; O/. Given two solutions E and E ¨ of P , we say that E is (syntactically) smaller than E ¨ if E Ó E ¨.1 We further say that a solution E of P is syntactically minimal if there is no other solution E ¨ of P that is smaller than E . 3
We first describe the MHS algorithm and then the MergeXplain algorithm. Both were implemented and evaluated as reported in Section 4. Finally we also describe how both algorithms may be combined to obtain a more effective yet still complete approach. 1 Note that before we compare two solutions E and E¨ of P syntactically, we typically normalize the assertions w.r.t. (outermost) concept conjunction: as C à D.a/ is equivalent to the pair of assertions C.a/ and D.a/, we replace the former form by the latter while possible. 3.1
This approach is based on the fact that E is an explanation of P = .K; O/ if and only if K ä E ô O, i.e., if and only if K ä E ä ^O` is inconsistent. Assume K ä ^O` is consistent and the set of all its models is M. To find some explanation, we may simply collect in E assertions that invalidate each model M Ë M. However we want to draw these assertions from the set of abducibles Abd. Hence it suffices to find a hitting set (MHS) of the set ^Abd.M / Ý M Ë M` where Abd.M / = ^ Ë Abd Ý M ¡ô ` is a set of expressions that invalidate M and are part of Abd.
In fact, as proved by Reiter [19], the set of all minimal explanations corresponds to the set of all minimal hitting sets of ^Abd.M / Ý M Ë M`, modulo negation.
The algorithm works by constructing a HS-tree T = .V ; E; L/, a labelled tree in which each node is labelled by Abd.M / for some model M of K ä ^O` and whose edges are labelled by elements of the parent node’s label. The HS-tree has the property that the node label L.n/ and the union of the edge-labels H .n/ on the path from root r to each node n are disjoint. If n cannot be extended by any successor satisfying this property then H .n/ corresponds to a hitting set.
In addition, pruning is applied during the HS-tree construction in order to eliminate
non-minimal hitting sets. The most obvious case is when a node n already corresponds
to a hitting set H .n/ and there is another node n¨ with H .n/ Ó H .n¨/. Any such n¨ can
be pruned. A pruned HS-tree (i.e., one on which all pruning conditions were applied),
once completed, contains all minimal hitting sets [19]. In addition we also prune nodes
which correspond to undesired explanations [
The resulting algorithm is given in Algorithm 1. This algorithm is sound and
complete [
Theorem 1. The MHS algorithm is sound and complete (i.e., it returns the set SE of all minimal desired explanations of K and O.)
The fact that MHS explores the search space using breadth-first search (BFS) allows
to limit the search for explanations by maximum size. The algorithm is still complete
w.r.t. any given target size [
MXP is listed in Algorithm 2. Both QXP and MXP were originally designed to find minimal inconsistent subsets (dubbed conflicts) of an overconstrained knowledge base K = B ä C, where K is the consistent background theory and C is the “suspicious” part from which the conflicts are drawn. This can be immediately adopted for ABox abduction: in order to find explanations for an abduction problem P = .K; O/ one needs to call MXP.K ä ^O`; Abd/. This observation allows us to adopt the following result from Shchekotykhin et al. [20]: Theorem 2. Assume an ABox abduction problem P = .K; O/ and a set of abducibles Abd. If there is at least one explanation Ó Abd of P then calling MXP.Kä^O`; Abd/ returns a nonempty set of explanations of P .
Ë L.n/ create a successor n of n and label the resp. edge by
Thus MXP is sound, and it always finds at least one explanation if at least one exists. However it is not complete, especially in cases of abduction problems which have multiple partially overlapping explanations.
Example 1. Let K = ^A à B Þ D; A à C Þ D` and let O = D.a/. Let us ignore negated ABox expressions and start with Abd = ^A.a/; B.a/; C.a/`. There are two minimal explanations of P = .K; O/: ^A.a/; B.a/`, and ^A.a/; C.a/`. Calling MXP(Kä ^O`; Abd), it passes the initial tests and calls FINDCONFLICTS(K ä ^O`; Abd).
FINDCONFLICTS needs to decide how to split C = Abd into C1 and C2. Let us assume the split was C1 = ^A.a/` and C2 = ^B.a/; C.a/`. Since both C1 and C2 are now conflictfree w.r.t. K ä ^O`, the two consecutive recursive calls return êC1¨ ; çë and êC2¨ ; çë where C1¨ = ^A.a/` and C2¨ = ^B.a/; C.a/`.
In the while loop, GETCONFLICT(K ä ^O` ä ^B.a/; C.a/`; ^B.a/; C.a/`; ^A.a/`) returns X = ^A.a/` while GETCONFLICT(K ä ^O` ä ^A.a/`; ^A.a/`; ^B.a/; C.a/`) returns B.a/, and hence the first confclit = ^A.b/; B.a/` is found and added into .
However, consecutively A.a/ is removed from C1¨ leaving it empty, and thus the other conflict is not found and = ^^A.b/; B.a/`` is returned. 3.3
As showed by the example, MergeXplain is not always complete. However, both approaches can be combined in order to regain completeness. The idea is to call MXP repeatedly and use the construction of the HS-tree to steer this process and to guarantee completeness.
Input: B: Background theory, C: the set of possibly faulty constraints Output: , a set of minimal conflicts 1: if isConsistent.B/ then 2: return "no solution" 3: else if isConsistent.B ä C/ then 4: return ç 5: end if 6: ê ; ë } FINDCONFLICTS(B; C) 7: return 8: function FINDCONFLICTS(B; C) returns a tuple êC¨; ë 9: if isConsistent.B ä C/ then 10: return êC; çë 11: else if ðCð = 1 then 12: return êç; ^C`ë 13: end if 14: Split C into disjoint, non-empty sets C1 and C2 16: êêCC21¨¨ ;; 21ëë }} FFIINNDDCCOONNFFLLIICCTTSS((BB;; CC12)) 15: 17: } 1 ä 2 18: while isConsistent.C1¨ ä C2¨ ä B/ do 19: X } GETCONFLICT(B ä C2¨ ; C2¨ ; C1¨ ) 20: } X ä GETCONFLICT(B ä X; X; C2¨ ) 21: C1¨ } C1¨ \^a` where a Ë X 22: } ä ^ ` 23: end while 24: return êC1¨ ä C2¨ ; ë 25: end function 26: function GETCONFLICT(B; D; C) 27: if D ç á isConsistent.B/ then 28: return ç 29: else if ðCð = 1 then 30: return C 31: end if 32: Split C into disjoint, non-empty sets C1 and C2 33: D2 } GETCONFLICT(B ä C1; C1; C2) 34: D1 } GETCONFLICT(B ä D2; D2; C1) 35: return D1 ä D2 36: end function
The combined algorithm MHS-MXP, presented in Algorithm 3, amends the function FINDCONFLICTS with additional third parameter Ó C that guarantees that if is a conflict for B (i.e., if B ä is inconsistent) then Ë , where is the set of conflicts returned by FINDCONFLICTS.B; C; /. This is assured by the modifications in lines 27 and 30. These changes are satisfactory to guarantee that if is a conflict for B, it is not lost from the output. The GETCONFLICT function did not require any modifications. Algorithm 3 MHS-MXP(K,O) 42: function ADDPATH(n, êa1; § ; anë) 43: if there is no n¨ in T s.t. L.n; n¨/ = a1 then 44: add node n¨, L..n; n¨// } a, L.n¨/ } L.n/ 45: end if 46: if n > 1 then 47: ADDPATH(n¨,êa2; § ; anë) 48: else 49: L.n¨/ } ç 50: end if 51: end function . n is pruned
MHS-MXP starts by checking if K ô O (i.e., if K ä ^O` is inconsistent) in which case there is nothing to explain. It then constructs the HS-tree with the following modifications: (a) Nodes are not labelled by subsets of Abd, instead the successor edges are drawn from the whole set Abd. Only nodes corresponding to found conflicts and to pruned nodes are labelled by ç to cut further search. (b) Nodes are explored by BFS, for each node n we call FINDCONFLICTS(K ä ^O`; Abd; H .n/) where by passing H .n/ as parameter we assure that, if it is a conflict, it is not omitted from the resulting set of conflicts . (c) If FINDCONFLICTS did not find any conflicts (i.e., if = ç) we terminate the search. We can do this because MXP always return some conflict, if one exists [20]. Hence we can be sure that the search is over. (d) The HS-tree is enriched by all paths found in which are now verified minimal conflicts and hence (the corresponding leaf-nodes) are omitted from future exploration. This is assured by labelling the ends of these paths by ç. (e) From now on all paths corresponding to their supersets will immediately be pruned when encountered by the BFS search – they correspond to nonminimal conflicts. (f) Finally we filter out conflicts corresponding to undesired explanations. Theorem 3. The MHS-MXP algorithm is sound and complete (i.e., it returns the set SE of all minimal desired explanations of K and O.)
The soundness follows from the soundness of MXP. The completeness follows from the observation that for every Ó Abd that is an explanation of P = .K; O/, the HS-tree contains a path respective to some leaf node n s.t. H .n/ = as was only subtracted from the node labels once at least one such node was added to the HS-tree.
Note that one additional optimization is possible: after FINDCONFLICTS is called for the first time and returns , it is safe to reduce Abd by removing all Ë such that ð ð = 1. This is because all minimal conflicts involving these abducibles were now found. This reduces the search space, and in the special case when all explanations are of size one the algorithm will terminate after two calls of FINDCONFLICTS. 4
A preliminary experimental evaluation was conducted with implementations of MHS and MXP, both paired with three DL reasoners – Pellet, HermiT, and JFact. Both algorithms are implemented in Java and communicate with the reasoners through OWL API. The source code of both implementations is available online.2
The evaluation is split into two experiments. Experiment 1 is focused on computing explanations of size one. In this case MHS can be made more effective by bounding the HS-tree depth, and on the other hand MXP is complete in this case. Experiment 2 was conducted without any constraints on the size of explanations, but a timeout needed to be set. Both experiments were focused on comparing execution times between the two approaches and the three reasoners. Each time was computed as an average value from ten runs with ten different observations. 2 https://github.com/katuskaa/MasterThesis 4.1
Three ontologies were chosen. The Family ontology3, is our own ontology of family
relations. It is smaller, but it is particularly useful in this use case as it generates a number
of explanations of size higher than one. LUBM ontology [
All experiments were done on a virtual machine with 8 cores (16 threads) of the processor Intel®Xeon®CPU E5-2695 v4, 32 GB RAM, 2.10GHz, running Ubuntu 18.04.1, while the maximum Java heap size was set to 4GB. Execution times were measured in Java using ThreadMXBean from the java.lang.management package. We used user time, that is the actual time without system overhead. 4.2
The first experiment is focused on comparing both methods (MHS and MXP) on a simplified task of finding all explanations of size one. We focus on this class of explanations for two reasons. Firstly, many real-world ontologies feature only weak axiomatization, if any, implying that most explanations, if not all, will be of size one.
Secondly, both MHS and MXP can be used to find all explanations of size one quite effectively. MHS – which is complete but normally quite ineffective – can be depthbound and stopped after it explored the search space up to size one, which takes considerably less time than to explore the rest of the search space. MXP, in turn, is incomplete in general, but it does not lose any explanations of size one.
For each ontology Figure 1 plots the average time of execution over ten observations for each of the three reasoners and for both methods. In case of the smallest Family ontology Figure 1 (a) shows that MHS is always quicker than MXP regardless of the DL reasoner used. Among the reasoners Pellet is the quickest when paired with MHS, however JFact is the quickest when paired with MXP. In all three cases MXP has found one additional explanation (of size 2) than MHS for one of the observations.
The results for medium-sized Beer ontology are plotted in Figure 1 (b). We observe that MHS is quicker than MXP with Pellet and HermiT, but in case of JFact MXP is quicker. Again, Pellet is the quickest when paired with MHS, and JFact is the quickest when paired with MXP, however the performance of HermiT is improved for this 3 http://dai.fmph.uniba.sk/~pukancova/aaa/ont/family2.owl 4 https://www.cs.umd.edu/projects/plus/SHOE/onts/beer1.0.html 0.7 0.6 larger ontology. Both approaches have found the same amount of explanations for each observation.
The LUBM ontology is the largest one in our use case. The plot in Figure 1 (c) shows that the results are essentially similar to the case of the Beer ontology. The only two cases which took significantly greater time were those of MHS/JFact and MXP/Pellet. We can also observe that the comparative performance of HermiT is further improved. Again, both approaches have found the same amount of explanations for each observation. 4.3
The goal of this experiment was to compute as much explanations as possible using MHS and MXP. We compare execution times and the number of explanations found. As runtimes of MHS (especially for larger ontologies) may be too high, a timeout of 12 hours (43200 seconds) was set. MXP terminated way faste in all runs, however, as we know, it does not explore the whole search space. The results are plotted in Figure 2.
The Family ontology (a) is much smaller compared to the other two, hence all runs finished before the timeout. Its richer axiomatization generates a number of explanations of size higher than one. Hence while MXP took shorter time than MHS it found a smaller number of explanations. Still, on average it found 82.35 % of the explanations found by MHS. On this smaller ontology once again Pellet was the quickest when paired with MHS while JFact was the quickest when paired with MXP.
The results for the Beer and LUBM ontologies (Figures 2, b–c) are similar. They show that even in case of medium size ontologies it simply is not feasible for MHS to explore the whole search space as it either reached the timeout (the cases of HermiT and JFact) or it exceeded the memory (the case of Pellet).5 Note that it may be feasible to use MHS in cases when the set of abducibles is further reduced, i.e., if the user knows or is able to guess beforehand in which part of the search space to look for possible explanations. Such cases are out of the scope of this paper. 5 Note that if the time out was reached we recorded 12 hours, but if the memory was exceeded we recorded the time at the end of the last completed depth of the HS-tree – hence the results for Pellet in Figure 2 (b–c) are only seemingly good.
In contrast, MXP only took a fraction of this time. (Note that while exact times of MXP runs are not readable from Figure 2 (b–c) due to scale, they are the same as in Figure 1 (b–c)). Both approaches found exactly all explanations of size one in each run (and none other). Since both ontologies feature only weak axiomatization it is unlikely that there are any larger explanations.
Looking at the MHS results of the three reasoners we observe that HermiT was the most successful in terms of being able to explore the largest part of the search space before the timeout. Interestingly, this is in contrast with the results on the Family ontology which may indicate that it likely features some initial overhead which is outweighed when the reasoning task grows larger. 5
In this work we have focused on comparison of MHS and MXP on the task of ABox abduction. We have implemented both approaches and conducted a preliminary evaluation. Our evaluation shows that in cases when there are only explanations of size one, or one is only interested in this size of explanations MHS is more effective. In cases when larger explanations cannot be ruled out MXP can be used for fast but incomplete query; in our tests we were able to obtain over 80 % of explanations in this way. MHS is complete but it is much slower. Even on medium size ontologies such as Beer and LUBM MHS did not terminate before the 12 hour timeout.
As we paired our solvers with three different DL reasoners in all experiments, we were able to compare the performance of these reasoners as well. Out of them HermiT was the most effective as it was able to search through the largest part of the search space before the 12 hour timeout expired.
We have also described a combined approach which leverages on the effectivity of MXP and uses MHS to steer the search and retain completeness. Empirical evaluation of this approach is an ongoing effort.
Acknowledgements. This work presents the results of the Master’s thesis by Katarína
Fabianová [