MHS-MXP is a hybrid algorithm which adopts the divide-and-conquer strategy of fast but incomplete MergeXplain (MXP) and combines it with Minimal Hitting Set (MHS) to regain completeness. We describe a class of inputs on which MHS-MXP has an advantage. We provide an experimental implementation which enables us to perform first preliminary empirical evaluation on this class of inputs. CEUR Workshop Proceedings
In the context of DL, ABox abduction [
together with ℰ entails . The MHS algorithm [
MHS is complete. It searches through the space of all possible explanations, from the smallest
(in terms of cardinality) towards the largest. This approach is useful, particularly in cases
where there are smaller explanations. However in cases where there is (even a small number
of) explanations of larger size this search strategy may be ineficient. Notably, the worst-case
complexity of the underlying problems is also hard. The MHS problem is NP-complete [
Alternative strategies were explored. QuickXplain (QXP) [
However, when MXP is run repeatedly, with slightly modified inputs, it divides the search
space diferently and it may return a diferent set of explanations than in the previous runs.
Based on this key observation, we have proposed a combined algorithm, dubbed MHS-MXP [
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). that iterates runs of MXP and it uses MHS to steer the search space exploration in such a way that completeness is retained.
In the current report we study relevant properties of MHS-MXP that help not only to establish its correctness, but also hint the class of inputs on which it may have an advantage over MHS. We conjecture, that one such class of favourable inputs are those with a smaller number of shorter explanations. We provide a preliminary implementation and show first empirical results that supports the above conjecture.
The main advantage of our work compared to some other promising approaches in DL
abduction [
We assume familiarity with the basics of DL [
In ABox abduction [
Definition 1 (ABox Abduction Problem). Let Abd be a finite set of ABox assertions. An ABox abduction problem is a pair = ( , ) such that is a knowledge base in DL and is an ABox assertion. An explanation of (on Abd) is any finite set of ABox assertions ℰ ⊆ Abd such that ∪ ℰ ⊧ .
We limit the explanations to atomic and negated atomic concept and role assertions; hence Abd ⊆ {(), ¬() ∣ ∈ C, ∈ I} ∪ {(, ), ¬(, ) ∣ ∈ R, , ∈ I}. Note that we do not limit the observations, apart from allowing only one (possibly complex) ABox assertion.
According to Elsenbroich et al. [
Definition 2 (Minimality). Assume an ABox abduction problem = ( , ) . Given explanations ℰ and ℰ ′ of , ℰ is (syntactically) smaller than ℰ ′ if ℰ ⊆ ℰ ′.An explanation ℰ of is (syntactically) minimal if there is no other explanation ℰ ′ of that is smaller than ℰ.
Input: Knowledge base , observation , abducibles Abd Output: ℰ all explanations of = ( , ) w.r.t. Abd 1: ← a model of ∪ {¬} 2: if = null then 3: return ”nothing to explain” 4: end if 5: ← ( = {}, = ∅, = { ↦ Abd()}) 6: for each ∈ () create new -successor of 7: ℰ ← {} 8: while exists next node in w.r.t. BFS do 9: if can be pruned then 3. Computing Explanations 10: prune 11: else if exists model of ∪ {¬} ∪ () 12: label by () ← Abd() 13: else if () is desired then 14: ℰ ← ℰ ∪ { ()} 15: end if 16: for each ∈ () 17: end while 18: return ℰ create new -successor of then We now review first the complete MHS algorithm and then the faster but approximative MXP algorithm. The hybrid approach that tries to combine “the best of both worlds” is then introduced in Section 4.
Adopting the well-known result of Reiter [
for some ⊧ ∪ {¬} , then ( , ) has no explanations on
The MHS algorithm (Algorithm 1) works by constructing an HS-tree = ( , , ) in which each node is labelled by Abd( ) for some model of ∪ {¬} and whose edges are labelled by elements of the parent’s label. If a node 1 ∈ has a successor 2 ∈ such that (⟨ 1, 2⟩) = then 2 is a -successor of 1.
The HS-tree has the property that the node-label () and the union () of the edge-labels on the path from the root to each node are disjoint. Each label () can be found as Abd( ) of any model of ∪ {¬} ∪ () , by one call to an external DL reasoner. If no such model exists then () corresponds to a hitting set. Note that if exists but Abd( ) = ∅ , then in accord with Observation 2 () cannot be extended to a hitting set.
Subset pruning eliminates non-minimal hitting sets: given a hitting set () , nodes ′ with
() ⊆ ( ′) are pruned. Equal-paths pruning prunes also nodes ′ with () = ( ′), even
if () is not a hitting set. Once completed, a pruned HS-tree contains all minimal hitting sets
[
Input: background theory ℬ, set of possibly faulty constraints Output: a set of minimal conflicts Γ 1: if ¬isConsistent(ℬ) then 2: return ”no explanation” 3: else if isConsistent(ℬ ∪ ) then 4: return ∅ 5: end if 6: ⟨ , Γ⟩ ← FindConflicts(ℬ, ) 7: return Γ 8: function FindConflicts(ℬ, ) 9: if isConsistent(ℬ ∪ ) then 10: return ⟨ , ∅⟩ 11: else if | | = 1 then 12: return ⟨∅, { }⟩ 13: end if 14: Split into disjoint, non-empty sets 1 and 2 15: ⟨ 1′, Γ1⟩ ← FindConflicts(ℬ, 1) 16: ⟨ 2′, Γ2⟩ ← FindConflicts(ℬ, 2) 17: Γ ← Γ1 ∪ Γ2 18: while ¬isConsistent( 1′ ∪ 2′ ∪ ℬ) do 19: ← GetConflict(ℬ ∪ 2′, 2′, 1′) 20: ← ∪ GetConflict(ℬ ∪ , , 2′) 21: 1′ ← 1′\{ } where ∈ 22: Γ ← Γ ∪ { } 23: end while 24: return ⟨ 1′ ∪ 2′, Γ⟩ 25: end function 26: function GetConflict(ℬ, , ) 27: if ≠ ∅ ∧ ¬ isConsistent(ℬ) then 28: return ∅ 29: else if | | = 1 then 30: return 31: end if 32: Split into disjoint, non-empty sets 1 and 2 33: 2 ← GetConflict(ℬ ∪ 1, 1, 2) 34: 1 ← GetConflict(ℬ ∪ 2, 2, 1) 35: return 1 ∪ 2 36: end function Theorem 1. The MHS algorithm is sound and complete (i.e., it returns the set ℰ of all minimal desired explanations of and on Abd).
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 [12].
Both QXP [
The essence of QXP is captured in the GetConflict function, which cleverly decomposes by splitting it into smaller and smaller subsets such that it is always able to reconstruct one minimal conflict, if it only exists. The auxiliary function isConsistent( ) encapsulates calls to an external reasoner; it returns true if is consistent and false otherwise.
Thus, if we just wanted to find one minimal explanation of an ABox abduction problem,
adopting a result of Junker [
MXP, captured in the FindConflicts function, finds as many conflicts as it is possible to reconstruct from one way in which can be split. MXP relies on GetConflict to recover some of the conflicts that would be lost due to splitting. This ensures that it keeps the important property of QXP that at least one minimal is found in each run, if it exists.
This approach can be immediately adopted for ABox abduction: in order to find explanations
for an abduction problem = ( , ) on Abd one needs to call MXP( ∪ {¬}, Abd). This
observation allows us to adopt the following result from Shchekotykhin et al. [
In fact, MXP is thorough in its decomposition of , which is broken to smaller and smaller subsets until they are consistent with ℬ or until only sets of size 1 remain. This directly implies that all conflicts of size 1 will always be found and returned by a single run of MXP. This observation will prove to be useful for our hybrid algorithm.
Observation 3. Given an ABox abduction problem = ( , ) any ⊆ Abd s.t. | | = 1 , if ∪ ⊧ then ∈ MXP( ∪ {¬}, , a set of abducibles Abd, and Abd).
Thus MXP is sound and it always finds at least one minimal explanation (Theorem 3), and it ifnds all explanations of size one (Observation 3). Still, MXP is not complete. Some explanations may be lost, especially in cases with multiple partially overlapping explanations. Example 1. Let = { ⊓ ⊑ , ⊓ ⊑ } and let = () . Let us ignore negated ABox expressions and start with Abd = {(), (), ()} . There are two minimal explanations of = ( , ) : {(), ()} , and {(), ()} . Calling MXP( ∪ {¬}, Abd), it passes the initial tests and calls FindConflicts( ∪ {¬}, Abd).
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 conflict-free 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 conflict = {(), ()} 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.
Finally, not only is MXP able to find all explanations of size 1, but it also has the property that if no longer explanations are returned in a given run then in fact this is because there are none. So in such a case we are sure that we have found all explanations whatsoever in a single run and we do not have to search any further.
Theorem 4. Given an ABox abduction problem = ( , ) , a set of abducibles Abd, let Γ = MXP( ∪ {¬}, Abd). If there is no ∈ Γ s.t. | | > 1 , then for all minimal ⊆ Abd s.t. ∪ ⊧ we have that ∈ Γ .
▷ Set of conflicts ▷ Set of cached models ▷
Init. HS-Tree ▷ Otherwise is pruned ▷ HS-tree is extended under The idea to use MXP to find all explanations is based on the observation that running it multiple times in a row may result in a consecutive extension of the overall set of conflicts found so far. A naïve, and possibly to a large extent successful idea, would be to randomize the set splits MXP does in each recursive call. We would likely find diferent conflicts each time, however it would not be clear when to stop.
We will instead explore a hybrid approach, and we will show that by modifying MXP’s inputs in its consecutive iterations, the search space exploration can be guided by the construction of an HS-tree from the obtained outputs, and thus completeness will be achieved.
The combined MHS-MXP algorithm, listed as Algorithm 3, therefore constructs the HS-tree as usual, but in each node , instead of simply retrieving one model of ∪ {¬} ∪ () , it launches MXP by calling FindConflicts.
It starts by checking the consistency of ∪ {¬} . We use a modified isConsistent function which stores all models in the model cache Mod. The stored models are later used to construct the HS-tree and label its nodes. For this reason we also assume that FindConflicts uses this modified isConsistent function.
Then the main loop is initiated. For the root node , FindConflicts is simply called passing ∪ {¬} as the background theory and Abd as the set of conflicts (as () = ∅ at this point). The obtained conflicts Γ are stored in Con. We then verify if all conflicts were already found or if the search needs to go on (line 13). From Theorem 3 we know that if no conflicts were returned in Γ, it means there are no conflicts whatsoever. Also from Observation 3 we know that all conflicts of size 1 are always found and returned in Γ. Finally, by Theorem 4 we have that if any larger conflicts remain, at least one is also present in Γ. Hence, if there is no ∈ Γ with | | > 1 there are no other explanations to be found and the search can be terminated.
If however at least one such was returned in Γ then the HS-tree is extended under using the model that was previously found and stored in Mod.
When consecutively any other node ≠ is visited by the main loop, we first check if it can be pruned: it is pruned if () contains any of the conflicts already stored in Con. If not, we now want to use MXP with the goal to explore as much as possible of that part of the space of explanations that extends () . Therefore we call FindConflicts passing ∪ {¬} ∪ () as the background theory and Abd ⧵ () as the set of conflicts.
If we are lucky, we might cut of this branch completely in line 13, that is, if no extension of () of size greater than 1 is found (by Theorem 4). Otherwise we extend the HS-tree below .
To be able to do that, we need a model of ∪ {¬} ∪ () . However, we do not need to run another consistency check here, as by design of our algorithm at this point such a model is already cached in Mod.
Observation 4. For each node of the HS-tree visited by the main loop of MHS-MXP( , , either () ∈ Con or ∪ {¬} ∪ () is consistent and at least for one ∈ Mod, ⊧ ∪ {¬} ∪ () .
Abd)
For the root this trivially holds as it was only visited (as the first node in the main loop) if the consistency check in line 3 was positive, i.e. a suitable model was found and cached.
For any other node , this holds due to FindConflicts was previously called in the parent node ′ of , and from Observation 3 we know that during that call all possible inconsistent extensions of ( ′) of size 1 were added to Con. So, if was not pruned in line 10, () = ( ′) ∪ { } must be consistent with ∪ {¬} . Moreover, since FindConflicts did not prove { } being a conflict for ∪ {¬} ∪ ( ′), at some point it must have checked the consistency of ∪ {¬} ∪ ( ′) together with { } or some superset thereof with a positive result, and at that point the respective model was added to Mod.
Finally, by the time a complete HS-tree is constructed, all explanations are accumulated in Con. However, due to calls to FindConflicts where (nonempty) () was passed together with as the consistent background theory, some of these conflicts in Con may be non-minimal and they have to be filtered out. At this point we also filter out any other undesired explanations. Then the remaining minimal and desired explanations are returned as ℰ.
Theorem 5. The MHS-MXP algorithm is sound and complete (i.e., it returns the set ℰ of all minimal desired explanations of and on Abd).
First of all, it is immediately apparent from the properties of MXP alone, that our approach absolutely crushes MHS in cases when all explanations are of size one. By Observation 3 and Theorem 4 the search may immediately stop after one call to MXP in the root node of the HS-tree. Without this “look ahead” capability provided to the hybrid algorithm by MXP, pure MHS has no way of knowing it could stop and has to generate the HS-tree completely.
Let us now consider some cases when bigger explanations come into play.
Example 2. Let = { ⊓ ⊑ , ⊓ (), ()} , let = () and let Abd = {(), (), (), ()} . There is exactly one explanation of ( , ) , ℰ1 = {(), ()} .
If we run MHS-MXP, it first checks ∪ {¬ ()} for consistency and it obtains a model thereof, say one with Abd( ) = {(), ()} .
The call to FindConflicts in the root does not allow to terminate the search, since ℰ1 was returned and |ℰ1| > 1. Therefore 1 and 2 are added to the HS-tree with ( 1) = {()} and ( 2) = {()} .
When FindConflicts is called in 1, it returns one conflict {()} which together with ( 1) makes up for the explanation ℰ1. What is more, this branch is consecutively cut of, as no greater conflicts were found. Notably, further exploration of branches extending ( 1) with () and () is avoided (in comparison with MHS).
Then FindConflicts is called in 2 returning one conflict {(), ()} , corresponding to the non-minimal explanation {(), (), ()} . However, since there was a conflict extending ( 1) by a size greater than one, we may not terminate yet and must explore this branch in the HS-tree further, until only extensions of size one are returned by MXP in each path.
The case presented in Example 2 and similar cases with a small overall number of explanations can still be handled rather eficiently, compared to MHS. It can be observed that a significant part of the search space is cut of. However consider the following modification of the inputs. Example 3. Given the and as in Example 2, let Abd = {(), (), (), (), (), ¬()} . The abduction problem ( , ) now has two explanations ℰ1 and ℰ2 = {(), ¬()} , where the second one is undesired (inconsistent). When FindConflicts is called in the root node it returns {{(), ()}, {(), ¬()}} . W.l.o.g. we may assume that the same model was used to label and that ⊧ ̸() . This time Abd( ) = {(), (), ()} and in addition to 1 and 2 as above also 3 is generated with ( 3) = {()} .
Now the search cannot be immediately cut of after MXP is called in any of the three nodes 1, 2, or 3. E.g., in 1 FindConflicts returns {{()}, {(), ¬()}} . Only branches where all but one element from each explanation is already present can be cut of safely.
The exercise we make in Example 3 shows that the larger the overall amount of explanations (including also various undesired explanations as ℰ2) and also the greater their size, the less advantage MHS-MXP is likely to retain. It should also be noted that while adding complementary assertions (inducing inconsistent explanations) to abducibles does not make a diference for MHS, it does make a diference (towards the worse) for MHS-MXP. This is also true of assertions that are mutually inconsistent due to the background ontology (and therefore inducing another type of undesired explanations, called irrelevant).
The problem of finding all explanations of a given abduction problem is hard. MHS itself is
NP-complete [
An implementation1 of MHS-MXP was developed in Java using Maven for dependency
management. Compared to the previous version of the implementation [
An external DL reasoner is called in each node to query about the model. The model data is extracted through OWL API [13], using the g e t T y p e s method. This approach is preliminary and it has known issues2, we are currently working on an alternate approach (cf. Conclusions).
Using the implementation, we ran3 tests in order to understand if MHS-MXP may have a certain advantage at least on cases of inputs that we identified as favourable. We have used the LUBM ontology [14]. It does not contain disjunction, so we are able to test on it even given the limited model extraction method that we currently use.
LUBM does not feature atomic concepts that would allow explanations of size greater than 1. Hence in each input we have set the observation to () where is an individual and is a new auxiliary concept name. Then we have randomly generated a set of LUBM concept names 1, … , , and added an equivalence ≡ 1 ⊓ ⋯ ⊓ into the input ontology. If 1, … , are independent concepts with no subconcepts there is exactly one explanation { 1(), … , ()} . If 1, … , are not independent the explanation will be shorter. If some of 1, … , have (independent) subconcepts there will be multiple partially overlapping explanations. We targeted explanations of size up to 5, hence we generated inputs for ∈ [1..5] – 50 inputs altogether. We have aggregated the inputs into five groups S1–S5 based on the size of the largest explanation. The inputs were generated randomly (however LUBM concepts with subconcepts were drawn twice as often to ensure higher number of explanations). The number of generated samples was consecutively reduced in order to obtain balanced groups S1–S5, each with 10 inputs.
To verify the second part of our conjecture, i.e. that MHS-MXP may perform better on inputs with smaller number of explanations, we also aggregated the same 50 inputs diferently, into 1The implementation is available at https://github.com/IvetBx/MHS-MXP-algorithm. 2We would need to extract all atomic concept assertions that are true in a model (i.e. in a complete completion tree constructed during a consistency check). OWL API is not well equipped for this task. The getTypes method instead returns all concept assertions that are entailed for a given individual. In cases e.g. when the ontology contain disjunction and ⊧ ⊔ () this would yield incorrect results. However for simple ontologies without disjunction there is always one model in which exactly those atomic concept assertions are true for a given individual which are also entailed (which is the model that we will extract). Therefore we may employ this preliminary model extraction method in our limited evaluation as described in the following. 3The experiments were executed on a virtual machine with 8 cores (16 threads) of the processor Intel Xeon CPU E5-2695 v4, 32GB RAM, 2.10GHz, running Ubuntu 20.04 and Oracle Java SE Runtime Environment v1.8.0_201. To measure the execution times in Java, ThreadMXBean from the package java.lang.management was used. The user time measured the actual time without system overhead. The maximum Java heap size to 4GB. groups C1–C5 accordingly. Basic characteristics of groups S1–S5 and C1–C5 are given in Table 1.
Our implementation supports atomic and negated atomic concept assertions as abducibles, where the latter may be suppressed by a switch. We have used this to obtain an unfavourable case for MHS-MXP (both atomic and negated atomic concepts allowed) and a favourable case (negated atomic concepts suppressed). However, all generated inputs only have explanations involving atomic concept assertions, hence each input has exactly the same number of explanations in either case (favourable and unfavourable) – only the search space in the unfavourable case (and the inherent dificulty for MHS-MXP to handle it) is larger.
Testing the inputs on the unfavourable case did not show significant diference between MHS and MHS-MXP. For the lack of space we omit details. The results on the favourable case are plotted in Figure 1. MHS runs are plotted on the left, and MHS-MXP runs are plotted on the right; results from groups S1–S5 are at the top, while groups C1–C5 are at the bottom.
To observe the eficiency of search space exploration we measured for each level of the HS-tree ( -axis) the time by which it is fully completed ( -axis). Group averages are plotted. Recall that when MHS completes level it has already found all explanations of size up to . In contrast MHS-MXP, after completing level , has already found all explanations of size up to +1 (cf. Observation 3).
MHS runs show similar times for S1–S5 up to level 2. S4–S5 reached time out in level 3, S2–S3 in level 4. Few S1 runs managed to finish levels 4 and 5. (Note that the results for levels 4 and 5 are “polluted” by the fact that only a small number of runs which finished before the time out are averaged here. However, levels 0–3 show the general trend.) In contrast, MHS-MXP was able to finish all runs within the same time out, even if sometimes required a few more levels than the maximal size of explanation for the given input. We can see a clear correlation between the maximal length of explanations and the required running time, in this respect each consecutive group between S1 and S5 proved to be harder.
The results on groups C1–C5 shows very similar trends, proving that MHS-MXP has greater advantage on inputs with smaller number of explanations.
We have reported on an ABox abduction algorithm based on hybrid combination of MHS and MXP. The aim of this approach is to obtain a complete algorithm, that is more eficient than 104 103 102 101 100 104 103 102 101 100 all S5 S4 S3 S2 S1 all C5 C4 C3 C2 C1 0 1 2 3 MHS 4 5 6 7 0 1 2 3 4 5 6
7
MHS-MXP 104 103 102 101 100 104 103 102 101 100 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 MHS, at least on a class of favourable inputs that we have described. We have implemented the algorithm and our first preliminary evaluation on the LUBM ontology confirms this conjecture.
Both MHS and MHS-MXP rely on an external DL reasoner (as a black box) to compute models of the KB. However DL reasoners do not return models as a standard reasoning service. They do not even necessarily compute them, however, tableau-based reasoners compute a finite representation of a model which contains suficient information for our approach. We currently employ a simplified workaround for model extraction which does not work in general. It allowed us to make experiments on LUBM, however we want to extend these to other (real world) ontologies. We are currently looking into the possibility to use OWLKnowledgeExplorerReasoner extension in OWL API for true model extension. The advantage of using an API would be that diferent (tableau-based) DL reasoners could then be plugged in. Another option would be to use a tight source-code integration of a DL reasoner such as in the case the MHS solver AAA [15] which tightly integrates Pellet [16].
We would like to express our thanks to anonymous reviewers for their valuable feedback on this and also on the previous version of this report. This work was supported by the Slovak Research and Development Agency under the Contract no. APVV-19-0220 (ORBIS) and by the EU H2020 programme under Contract no. 952215 (TAILOR). Martin Homola is also supported by projects VEGA 1/0621/22 and APVV-20-0353. Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, AAAI, 2006, pp. 57–67. [12] J. Pukancová, M. Homola, ABox abduction for description logics: The case of multiple observations, in: Proceedings of the 31st International Workshop on Description Logics, Tempe, Arizona, US, volume 2211 of CEUR-WS, 2018. [13] M. Horridge, S. Bechhofer, The OWL API: A java API for OWL ontologies, Semantic Web 2 (2011) 11–21. [14] Y. Guo, Z. Pan, J. Heflin, LUBM: A benchmark for OWL knowledge base systems, Journal of Web Semantics 3 (2005) 158–182. [15] J. Pukancová, M. Homola, The AAA abox abduction solver, Künstliche Intell. 34 (2020) 517–522. [16] E. Sirin, B. Parsia, B. Cuenca Grau, A. Kalyanpur, Y. Katz, Pellet: A practical OWL-DL reasoner, Journal of Web Semantics 5 (2007) 51–53.