The state-of-the-art complete algorithms to solve ABox abduction in DL include the original Reiter's algorithm for minimal hitting sets alongside its more recent updates: Wotawa's HST and Pill and Quaritch's RC-Tree. On the other hand, incomplete methods that quickly find some but not all solutions include Junker's QuickXplain and MergeXplain by Shchekotykhin et al. We present CATS, a new modular ABox abduction solver. It implements all the said algorithms together with the hybrid MHS-MXP, recently introduced by Homola et al., and two new analogous variants: HST-MXP and RCT-MXP, based on HST and RC-Tree, respectively. The user can choose any of the eight algorithms. The solver uses the JFact reasoner as a black box and thus allows any DL expressivity up to ℛℐ. The modular implementation served as a test bed for an evaluation and comparison of the implemented algorithms, which we conducted over the LUBM ontology. Out of the complete algorithms, the hybrid ones were proven to find explanations faster, and they were also more memory-eficient.
Abduction [
There are various types of algorithms that can be utilized to solve an abduction problem. Our research focuses mainly on those that ofer the following advantageous properties [ 26]: (1) Applicability to knowledge bases of any expressivity, or even to any logic (with entailment and model-theoretic semantics); (2) Completeness, meaning they guarantee finding all possible explanations; (3) Black-box reasoning, allowing supporting reasoning tasks required for computing explanations to be delegated to an external reasoner; (4) Requiring no additional information about the problem.
One such algorithm is the well-explored Reiter’s minimal hitting set algorithm (MHS) [27], along
with its hybrid version, MHS-MXP [28], which combines Reiter’s algorithm with the eficient but
incomplete divide-and-conquer MergeXplain (MXP) method [29]. Both were implemented in the
MHSMXP abduction solver [28], currently one of the few publicly available abduction solvers [
However, the MHS-MXP solver has notable shortcomings. It sufers from memory management issues, with one of its evaluations resulting in out-of-memory errors in 57% of cases [31]. Additionally, it adopts a modified version of Reiter’s MHS algorithm that preserves completeness at the cost of sacrificing some of the original optimizations, which, when combined, may lead to the omission of explanations [32].
To address this limitation, we explore alternatives to Reiter’s algorithm that aim to resolve the incompleteness of MHS in a more eficient manner, namely, Wotawa’s Hitting Set Tree (HST) algorithm [33] and RC-Tree (RCT) algorithm [34]. We apply them to solve the abduction problem, and propose new hybrid algorithms by combining them with the MergeXplain method. We then present an improved version of the solver that supports MHS, HST and RC-Tree, together with their hybrid versions MHSMXP, HST-MXP and RCT-MXP, and the two incomplete algorithms MergeXplain and QuickXplain [35]. This new version, rebranded as CATS (Comenius Abduction Team Solver), is freely available1.
Finally, we provide an empirical evaluation of the algorithms on a dataset derived from the LUBM ontology [36], focusing on the cumulative amount of computed explanations over time. The results show a significant advantage of the hybrid algorithms, particularly MHS-MXP and RCT-MXP. We also show that the hybrid algorithms are more eficient in memory usage.
The vocabulary of ℒ [37, 38] consists of three countable, mutually disjoint sets of non-logical symbols: individuals (denoted ), atomic concepts (denoted ) and roles (denoted ). ℒ concepts are recursively built using the following grammar: , ::= | ¬ | ⊓ | ⊔ | ∀. | ∃. , where ∈ and ∈ . The logical symbols used in the grammar, called constructors, are as follows: ¬ (complement), ⊓ (concept intersection), ⊔ (concept union), ∃ (existential restriction), ∀ (value restriction). The semantics is defined using an interpretation ℐ = (∆ ℐ , · ℐ ), which consists of a non-empty domain ∆ ℐ and an interpretation function · ℐ such that: ℐ ∈ ∆ ℐ for every ∈ ; ℐ ⊂ ∆ ℐ for every concept ; ℐ ⊆ ∆ ℐ × ∆ ℐ for every ∈ . A DL knowledge base (KB) = ( , ) consists of a TBox (intensional knowledge) and an ABox (extensional knowledge), whilst contains general concept inclusion (GCI) axioms in form ⊑ for any concepts , , and contains concept assertions : , and role assertions , : for , ∈ , ∈ , and any concept .
An interpretation ℐ satisfies an axiom (ℐ |= ) if and only if: if = ⊑ then ℐ ⊆ ℐ ; if = () then ℐ ∈ ℐ ; if = (, ) then (ℐ , ℐ ) ∈ ℐ . ℐ is a model of a KB (ℐ |= ) if and only if it satisfies all axioms in . is consistent if and only if it has a model. entails ( |= ) if and only if is satisfied by every model of .
In an ABox abduction problem [
Definition 1 (ABox abduction problem). Let abducibles be a finite set of ABox axioms, background knowledge a DL knowledge base, and observation O an ABox axiom. An explanation of an ABox abduction problem = (, O′) is a finite set of ABox axioms ℰ ⊆ such that ∪ ℰ |= O.
The space of possible explanations is limited to axioms from the set of abducibles . They are also typically limited to so-called desired explanations, i.e., (in this work) they must be consistent (ℰ ∪ is consistent); relevant (O ̸|= ℰ ); explanatory ( ̸|= O); and minimal (there is no other explanation ℰ ′ s.t. ℰ ′ ⊆ ℰ ).
The ABox abduction problem can be reduced to a consistency-checking problem [39]: ∪ ℰ |= O if
and only if ′ = ∪ ℰ ∪ {¬O} , i.e., ′ has no models. It has been established that
1https://github.com/Comenius-Abduction-Team/CATS-Abduction-Solver
ifnding all minimal explanations of some = (, O) corresponds w.r.t. to finding all minimal
hitting sets of , where is the collection of negated models of ∪ {¬O} w.r.t. [
Definition 3 (Negated model w.r.t. ). Given a model ℐ, its negation w.r.t. is a finite set of ABox axioms defined as {¬ ∈ | ℐ |= }, where is an atomic (concept/role) assertion.
A classical algorithm for computing all minimal hitting sets, introduced by Reiter [27], was adapted for
ABox abduction [
The algorithm uses three pruning conditions: the first two close nodes whose paths () are redundant w.r.t. other existing paths; the last one removes whole subtrees that are found to be unnecessary, because all hitting sets that could be found in them can also be found in another part of the tree. However, applying all the conditions can lead to loss of explanations [32]. One way to retain completeness is to omit the third condition at the cost of losing the optimization. With this applied, all explanations of size are guaranteed to be found in the th level of the tree. The algorithm though cannot detect when all explanations are found and it continues building the tree as long as new branches can be generated.
Several alternatives to Reiter’s algorithm aim to address its incompleteness. One such method is the RC-Tree (RCT) algorithm [34].2
Instead of closing nodes with duplicate paths, RCT never creates such paths in the first place. Every node is assigned an exclusion set () , containing axioms that cannot use to generate child edges. This includes axioms already used by ’s ancestors and siblings, assuring that every path under will be unique. Using this strategy, RCT tries to create a tree that is as small as possible, but still suficient to ifnd all explanations.
However, this means that removing a subtree with the third pruning condition would prevent some subsets of abducibles from ever being generated, even possible explanations. To prevent this, every pruning updates the s in the tree – axioms that disappeared from the tree are removed from s and they are used to generate new edges, no longer redundant. This way, unlike Reiter’s algorithm, RCT can create branches in any level of the tree, not only the last one. This approach requires more memory (storing s) and repeated tree traversal.
Wotawa’s Hitting Set Tree (HST) algorithm [33], another variant of Reiter’s method, also ensures that duplicate paths cannot be created. Instead of navigating through the search space based on the negated models, the algorithm systematically enumerates every possible combination of abducible axioms. However, at any given point, this only includes abducibles that have appeared in at least one negated model so far, since unused axioms cannot be part of any minimal hitting set (per Definition 2). To track this, every time a new axiom is encountered in a negated model, HST assigns it a unique integer index (the approach to generating all combinations uses integer intervals) . Unlike Reiter’s and RC-Tree, HST 2Though these hitting set algorithms are not adapted for DL abduction, we use abduction-related terminology for simplicity. uses negated models only for this purpose. Once all abducibles are numbered, the models are no longer needed to be stored nor obtained anew.
Reiter’s algorithm also inspired MHS-MXP [28], the only approach here specifically designed for ABox abduction. It leverages the MergeXplain (MXP) algorithm [29], which finds minimal inconsistent axiom sets using repeated calls to QuickXplain (QXP) [35]. QXP is much faster than Reiter’s method but can find only one explanation. MXP improves this by finding multiple explanations but still cannot guarantee completeness.
MHS-MXP builds a HS-tree, but instead of consistency checks, it calls MXP using the current node’s path. This allows MHS-MXP to: (1) find multiple explanations per node; (2) discover explanations of size before reaching tree depth ; (3) and skip generating branches that cannot lead to valid explanations. Thanks to the third property, the algorithm can determine that all possible explanations have already been found and terminate even before the whole search space has been explored.
CATS (Comenius Abduction Team Solver) is a new version of the MHS-MXP solver, the original Java implementation of MHS-MXP [28] that also supported Reiter’s MHS algorithm. It introduces significant changes to the code-base and functionality, most notably, a wider collection of abduction algorithms.
We implemented RC-Tree and HST, adapting them to the context of ABox abduction for the first time. Analogously to MHS-MXP being based on MHS, we also "hybridized" RCT and HST, introducing two brand new algorithms: RCT-MXP and HST-MXP. Additionally, we implemented the two fast, but incomplete methods, QuickXplain and MergeXplain, which were already present in the code as components of MHS-MXP. This brings the total number of available algorithms to 8.
The solver uses the OWL API to delegate consistency checks to an external reasoner. In the case of a successful consistency check, the algorithms require a representation of a model found by the reasoner. This functionality is currently implemented only by JFact [28]. 3.1. Usage An abduction problem and run parameters (such as the algorithm to be used, the abducibles, etc.) can be passed to the solver using either of the following: (1) a structured input file and a command-line application; (2) a graphical application; (3) a programmatical Java API [40]. The explanations found are saved into log files. Unlike the previous version, CATS log files track detailed statistics about the solver’s run, such as memory used, counts of created nodes, branches, prunings, consistency checks, etc.
Abducibles can be set either directly or by specifying allowed individuals and concepts. If none are provided, all combinations of () and ¬() from the background knowledge are used; negations can be disabled to reduce their number. Solver performance depends heavily on abducible size, which increases computational load. Additionally, MHS-MXP has been shown to perform poorly with negations, as MXP identifies any set containing both () and ¬() as a possible explanation [28].
The MHS-MXP solver implementation kept the code of the two original algorithms in the same class, diferentiating between them with if-else blocks. This, however, made it hard to reasonably extend the code. We reworked this basic approach using the composition-over-inheritance [41] principle, creating a modular architecture where the solver’s behaviour is composed of multiple objects realizing abstract interfaces.
The main interfaces are ITreeBuilder, which determines how the HS-tree is built, and INodeProcessor, which handles what should occur in each node – i.e., a consistency check, an MXP or QXP call. Consequently, any algorithm can be trivially hybridized by combining its tree builder with the MXP node processor. Simultaneously, the RootOnlyTreeBuilder class, used in the MXP and QXP implementation, can be used to run an operation just once. This provides the flexibility to abstract away from the HS-tree and implement any abduction algorithm with inputs and outputs matching the interfaces.
Apart from refactoring the code-base, we also identified multiple bugs. Our main focus was on the memory errors encountered in a past evaluation [31]. We discovered the culprit in the process of storing negated models, which created large numbers of redundant objects. A new approach is used in CATS, ifxing the error and making the solver suitable for experiments on bigger ontologies than before.
The implementation includes various optimizations. Most notably, MHS and HST, alongside their hybrid versions, don’t have to remember the whole HS-tree – they only store unprocessed nodes (those awaiting expansion and checks). In the case of MHS, this was already the case in the MHS-MXP solver and was made possible thanks to the omission of Reiter’s third pruning condition. We implemented multiple other optimizations to prevent redundant objects and actions.
Some other changes in the new version include: more accurate time measuring; more reliable time-out mechanism; and automated tests, previously fully absent, to verify the algorithms’ correctness and detect mistakes during development.
We used the dataset of ABox abduction problems3 from the previous evaluation [28]. The abduction problems for the evaluation were grouped as S1–S5, where each Si contains problems with explanations of size . All problems share the same background knowledge (the LUBM ontology [36]) and have the same two sets of abducibles: {(), ¬() | ∈ , ∈ } (with negations) and {() | ∈ , ∈ } (without negations), using the vocabulary from the background knowledge and the given observation. The former set of abducibles is considered “favourable” for the hybrids and the latter “unfavourable” (see Section 3.1). Later groups are not inherently harder, but larger explanations mean more of the search space must be explored and thus a deeper HS-tree must be built. Each problem has the same set of (desired) explanations, regardless of whether negations are allowed or not.
For each group, 5 problems were selected. Each algorithm ran twice with and twice without negations. The time limit was reduced from 4 to 2 hours, as in the previous evaluation, not much of interesting data was obtained from the runs after 2 hours.
The solver4 was run on a server with the Ubuntu 24.04.1 operating system, using Java version 1.8.0_412. The server had 24 2.2 GHz processors and 64GB of RAM. Each run of the solver had 4GB of memory allocated to the JVM.
3Evaluation inputs: https://github.com/Comenius-Abduction-Team/CATS-Abduction-Solver/tree/main/in/dl2025 4CATS version 2.0.0: https://github.com/Comenius-Abduction-Team/CATS-Abduction-Solver/releases/tag/v2.0.0 cutof does not imply early termination – only that no further explanations were found. However, each curve ends at the maximal runtime encountered for that algorithm: if it is present for the whole 2 hours, the algorithm hit the time-out at least once (see Section 4.2.2 for more details). If it breaks earlier, no run of that algorithm lasted longer than the curve’s endpoint.
Without Negations. In S1, MXP and all hybrid algorithms found all explanations around the same time, slightly ahead of base algorithms (MHS, HST, RC-Tree), confirming MXP’s efectiveness at identifying all size-1 explanations in the root.
From S2 on, base algorithms begin to lag. HST-MXP is also significantly slower by S 3 and barely progressing in S5 (39.8 explanations by 5106.5s). MHS-MXP and RCT-MXP overall perform similarly to each other: RCT-MXP is faster in S4 and leads early in S5, but plateaus around 3000–4000s, allowing MHS-MXP to pull ahead. This suggests RCT-MXP may scale less eficiently on deeper HS-trees due to its need to store and traverse the entire structure.
Among base algorithms, RC-Tree performed the best in S2 and S3, while HST was the slowest and least efective. None of the base algorithms found any explanations in S 4 or S5. This highlights a limitation of previous evaluations: while they showed MHS could not guarantee all size-4 explanations before timeout, they did not reveal whether any size-4 explanations were found.
MHS
MHS-MXP With Negations. With negations allowed, base algorithms were generally faster than hybrids and MXP in S1 and S2, echoing previous results – except for HST, which lagged behind all complete algorithms in S2. In S3, it needed nearly two hours to match incomplete MXP’s output. This reinforces HST as likely the least efective complete algorithm. Upon further inspection, we found that HST usually assigned number indices to all of the abducibles right at the beginning of its runs. As it generates combinations of numbered abducibles, this essentially turns HST into a brute-force method, generating all possible combinations of abducibles without using any strategy or heuristics.
Earlier evaluations portrayed MHS-MXP as consistently worse than MHS in cases with negations. This setting is indeed disadvantageous for hybrids, leading to low explanation counts and slow initial growth compared to cases without negations. However, from S3 onward, hybrids proved faster and more productive than base algorithms, which found no explanations of size 4 or 5. Though neither guaranteed completeness, hybrids clearly performed better.
Notably, HST-MXP – generally the weakest hybrid – led among hybrids during a 1000–2000s window, and was the fastest in S2 and S4. While RCT-MXP found slightly more total explanations, HST-MXP may be more efective when prioritizing early results in a limited time. QXP failed to find any explanations, illustrating its low efectiveness with non-trivial abducibles.
MHS
MHS-MXP
In practice, it matters not only how many explanations an algorithm finds, but also whether it can terminate naturally instead of running unnecessarily long after all explanations are found.
QXP and MXP always terminated early, while all base algorithm runs and all hybrid runs with negations hit the time-out. Only hybrids without negations occasionally finished early (see Table1). Since HST-MXP usually timed out, we focused on MHS-MXP and RCT-MXP. Their average run times were similar, with RCT-MXP slightly faster in S2 and S5, and notably faster in S3. As it also finished early in two more cases, it appears marginally more efective in this respect. Note that MXP can always find all explanations of size 1. This means that in S 1 cases, the hybrids are able to find all explanations in their root and ideally should terminate almost immediately. However, negations in abducibles are in conflict with the hybrids’ ability to terminate early, causing them to always hit time-out in S1 with negations enabled. As it stands, MXP is the only algorithm that could ifnd all explanations and then terminate in S 1 with negations.
To plot memory usage over time, we recorded the average memory per HS-tree level. We applied linear interpolation between checkpoints for each run, then averaged the results across all runs – separately for cases with and without negations. Input groups were not distinguished, as their diferences were minimal.
MHS MHS-MXP
HST HST-MXP
RCT
RCT-MXP negations
QXP
MXP no negations
The methodology is reflected in the graphs: cases with negations show smooth curves due to longer times needed to complete tree levels, resulting in fewer records. Most records appear early or at timeout, with the rest interpolated. This is especially true for the curves that are mostly straight (MHS, HST and HST-MXP with negations; all base algorithms without negations) – these algorithms had almost no records between 1000 seconds and the timeout.
Without negations, faster level completions yield more real data, producing more uneven curves. RC-Tree and RCT-MXP, which revisit levels frequently, have the jaggedest curves.
Without negations, algorithms fall into three groups: RCT(-MXP) uses the most memory and MHS(MXP) slightly more than HST(-MXP). Interestingly, hybrids generally start less memory demanding than their base versions, but the gap narrows over time. With negations, RC-Tree and RCT-MXP are still the most memory-intensive, though the diferences are smaller. Once again, base algorithms use more memory than hybrids.
RCT(-MXP)’s high memory use is expected due to storing the full HS-tree and more data per node. HST(-MXP)’s lower usage than MHS(-MXP) is surprising, possibly tied to pruning behaviour (never duplicates a path) or model storage, though causes are unclear without analysing the deeper metrics.
Although we mostly focus on the complete algorithms, it is practical to explore properties of MXP in the S1 cases, where it can always find all explanations. Table 2 shows average memory usage of complete algorithms in S1. As MXP does not need to construct a tree, it is obviously less memory-heavy than the others. The exception is the hybrids without negations. In those cases, hybrids can terminate right after the root and essentially are the same as MXP.
We have described CATS Solver, a new ABox abduction solver for DL implementing eight algorithms. CATS is based on the JFact reasoner as a black box, and it supports any DL expressivity up to ℛℐ/OWL 2. The modular implementation of the solver enables the user to freely choose an algorithm best suited for a given application. For instance, if just one of a few explanations needs to be found, the incomplete but fast methods QuickXplain and MergeXplain may be used. If one wishes to ifnd as many explanations as possible, one of the five complete algorithms may be used. The solver ofers a command-line and graphical user interface, together with an API Java library.
The modular implementation of the algorithms also enables us to compare them. To this end, we have conducted an empirical evaluation of all eight algorithms on a dataset derived from the LUBM ontology. The results showed that out of the classic algorithms, including Reiter’s MHS, Wotawa’s HST and Pill and Quaritch’s RC-Tree performed the best most of the time, followed by MHS, with HST performing constantly worse than the two. As a more interesting result, all three hybrid algorithms perform significantly better than any of the three classic versions. The diference in performance of the hybrids is much more fine-grained with HST-MXP being the slowest most of the time (but also the fastest in a small number of cases), while MHS-MXP and RCT-MXP are much harder to distinguish between.
Importantly, contrary to the previous evaluation [28], the new evaluation methodology focusing on the progress of explanations being found in time (and possibly a number of optimizations that were implemented) helped us to clearly demonstrate that the hybrid algorithms are always performing better, even on less favourable use cases.
In the future, we plan [42] to conduct a more detailed evaluation on real-world ontologies. The performance of the solver may also possibly be improved by integration with other reasoners than JFact.
The authors would like to express their gratitude to Ján Kľuka for his valuable insights and helpful discussions. This research was funded by the EU NextGenerationEU through the Recovery and Resilience Plan for Slovakia under the project No. 09I05-03-V02-00064.
During the preparation of this work, the authors used Grammarly and gpt-4o in order to: Grammar and spelling check, Improve writing style. After using these tools, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. Description Logics (DL 2025), Opole, Poland, September 3–6, 2025, 2025. To appear.