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 [16], and it was studied also in the context of description logics (DL) [5,12,10,9,4,13,6,2,17,18,14,3]. We focus on ABox abduction [5] wherein both observations and explanations are extensional (i.e., they come in the form of ABox assertions).
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 [10,9] and later extended by Pukancová and Homola [17,18] and Mrózek et al. [14] who have developed a black box approach and its proof-of-concept implementation.
The main advantage of Reiter's algorithm is its completeness. Also, thanks to properties of breath-first search it finds smaller explanations first [18], but to search through the complete space of explanations may simply take too long.
However, completeness is not necessarily required. In some applications it may be sufficient to find just one explanation. For such scenarios Junker [11] proposed Quick-Xplain (QXP), which uses divide and conquer to find one explanation more effectively. This method was further extended by Shchekotykhin et al. [20] into MergeXplain (MXP), capable of finding multiple explanations in one run.
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
al. [14]. This allowed us to repeat all our experiments with Pellet [22], HermiT [21], and JFact [15]. 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.
For simplicity we will introduce [1]. However any other DL may be used due to our black box approach. A vocabulary consists of countably infinite mutually disjoint sets of individuals I = { , , …}, roles R = { , , …}, and atomic concepts C = { , , …}. Concepts are recursively built using constructors ¬, ⊓, ∃, as shown in Table 1. A KB = ∪ consists of a a finite set of GCI and RIA axioms (in TBox ), and a finite set of assertions (in ABox ) as given in Table 1.
An interpretation is a pair = (Δ , ⋅ ), where Δ ≠ ∅ is a domain, and the interpretation function
such a way that the interpretation of any complex concept is as given on the right-hand side of Table 1.
Finally, we define
In ABox abduction [5], we are given a KB and an observation consisting of an ABox assertion. The task is to find an explanation , again, consisting of ABox assertions, such that ∪ ⊧ . However, the set of all ABox expressions may be too broad to draw the explanations from (after all, it is infinite), hence we typically consider some set of abducibles Abd. In this work we will limit the explanations to atomic and negated atomic concept assertions; so we set Abd ∶= { ( ), ¬ ( ) | ∈ C , ∈ I }. Note that we do not limit the observations in any way, apart from allowing only one (possibly complex) ABox assertion.
ABox abduction problem is a pair = (, ) such that is a knowledge base in DL and is an ABox assertion. A solution of (also called explanation) is any finite set ⊆ Abd of ABox assertions such that ∪ ⊧ .
While Definition 1 establishes the basic reasoning mechanism of abduction, some of the explanations it permits may be unintuitive. According to Elsenbroich et al. [5] given = (, ) and its solution :
Indeed an explanation should be consistent, as anything follows from inconsistency; and so, an explanation that makes inconsistent does not really explain the observation. It should be relevant -it should not imply the observation directly without requiring the KB 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.
Assume an ABox abduction problem = (, ). Given two solutions and ′ of , we say that is (syntactically) smaller than ′ if ⊆ ′ . 1We further say that a solution of is syntactically minimal if there is no other solution ′ of that is smaller than .
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.
This approach is based on the fact that is an explanation of = (, ) if and only if ∪ ⊧ , i.e., if and only if ∪ ∪ {¬ } is inconsistent. Assume ∪ {¬ } is consistent and the set of all its models is . To find some explanation, we may simply collect in assertions that invalidate each model ∈ . 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( ) | ∈ } where Abd( ) = { ∈ Abd | ̸ ⊧ } is a set of expressions that invalidate 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( ) | ∈ }, modulo negation. The algorithm works by constructing a HS-tree = ( , , ), a labelled tree in which each node is labelled by Abd( ) for some model of ∪ {¬ } and whose edges are labelled by elements of the parent node's label. The HS-tree has the property that the node label ( ) and the union of the edge-labels ( ) on the path from root to each node are disjoint. If cannot be extended by any successor satisfying this property then ( ) 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 already corresponds to a hitting set ( ) and there is another node ′ with ( ) ⊆ ( ′ ). Any such ′ 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 [17].
The resulting algorithm is given in Algorithm 1. This algorithm is sound and complete [19,17,18]. Theorem 1. The MHS algorithm is sound and complete (i.e., it returns the set of all minimal desired explanations of and .)
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 [18].
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 = ∪ , where is the consistent background theory and 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 = (, ) one needs to call MXP( ∪ {¬ }, Abd). This observation allows us to adopt the following result from Shchekotykhin et al. [20]: Theorem 2. Assume an ABox abduction problem = (, ) and a set of abducibles Abd. If there is at least one explanation ⊆ Abd of then calling MXP(∪{¬ }, Abd) returns a nonempty set Γ of explanations of .
Require: knowledge base , observation Ensure: set of all explanations of = (, ) of the class Abd 1:
return "nothing to explain" for each ∈ ( ) create a successor of and label the resp. edge by 18: end while 19: return 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. FINDCONFLICTS needs to decide how to split = Abd into 1 and 2 . Let us assume the split was 1 = { ( )} and 2 = { ( ), ( )}. Since both 1 and 2 are now conflictfree w.r.t. ∪{¬ }, the two consecutive recursive calls return ⟨ ′ 1 , ∅⟩ and ⟨ ′ 2 , ∅⟩ where ′ 1 = { ( )} and ′ 2 = { ( ), ( )}. In the while loop, GETCONFLICT( ∪ {¬ } ∪ { ( ), ( )}, { ( ), ( )}, { ( )}) returns = { ( )} while GETCONFLICT( ∪ {¬ } ∪ { ( )}, { ( )}, { ( ), ( )}) returns ( ), and hence the first confclit = { ( ), ( )} is found and added into Γ.
However, consecutively ( ) is removed from ′ 1 leaving it empty, and thus the other conflict is not found and Γ = {{ ( ), ( )}} is returned.
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: : Background theory, : the set of possibly faulty constraints Output: Γ, a set of minimal conflicts 1: if ¬ () then 2:
return "no solution" The combined algorithm MHS-MXP, presented in Algorithm 3, amends the function FINDCONFLICTS with additional third parameter ⊆ that guarantees that if is a conflict for (i.e., if ∪ is inconsistent) then ∈ Γ, where Γ is the set of conflicts returned by FINDCONFLICTS(, , ). This is assured by the modifications in lines 27 and 30. These changes are satisfactory to guarantee that if is a conflict for , it is not lost from the output. The GETCONFLICT function did not require any modifications.
Require: knowledge base , observation Ensure: set of all explanations of = (, ) of the class Abd
return "nothing to explain" MHS-MXP starts by checking if ⊧ (i.e., if ∪ {¬ } 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 we call FINDCONFLICTS( ∪ {¬ }, Abd, ( )) where by passing ( ) 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.
The soundness follows from the soundness of MXP. The completeness follows from the observation that for every ⊆ Abd that is an explanation of = (, ), the HS-tree contains a path respective to some leaf node s.t. ( ) = 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.
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. 2The 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.
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 [8], is a standard benchmark. Beer ontology 4 was chosen. Both LUBM and Beer were chosen because of their larger size compared to the Family ontology, but on the other hand as in the case of many real world ontologies their axiomatic structure is less complex which implies that most if not all explanations are of size one. 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.
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 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.
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. 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.
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á [7]. It was supported by the Slovak national project VEGA 1/0778/18.