We present two alternative algorithms for computing (all or some) solutions to the concept abduction problem: one algorithm is based on Reiter's hitting set tree algorithm, whereas the other one relies on a SAT encoding. In contrast to previous work, the algorithms do not rely on a refutation-based calculus and, hence, can be used also with eficient reasoners for tractable DLs such as ℰℒ and its extensions. An adaptation to other forms of (logic-based) abduction, e.g., to ABox abduction, is also possible.
but directly derive (logical) consequences, which prevents the use of existing approaches to abduction. We aim at closing this gap and, inspired by the work of Kazakov and Glimm [10] for computing justification (i.e., minimal subsets of axioms from a knowledge base that are needed for a given entailment), we propose an alternative approach to eficiently compute some or all (minimal) explanations. The approach is based on Reiter’s minimal hitting set algorithm [11] without relying on a refutation-based calculus to guide the algorithm. An encoding of the problem into SAT allows for better managing the combinatorial problem of selecting what constitutes an explanation. As our goal is the development of an approach for DLs such as ℰ ℒ, where the main reasoning task involves determining concept subsumptions, we focus on concept abduction [12] as introduced next. The accompanying technical report gives further details, examples, and complete proofs [13].
We use the standard syntax and semantics of DLs (see, e.g., [14]). Note that the DL ℰ ℒ only allows for using the top concept, conjunctions, and existential restrictions as concepts. We now introduce the basic ideas of (concept) abduction (see also [12, 15]).
Definition 1. A concept abduction problem is a tuple ⟨, ℋ, ⟩ with a knowledge base, ℋ, the hypotheses, a set of atomic concepts, and , the observation, a single atomic concept.1 A set = {1, . . . , } ⊆ ℋ is an explanation for if |= 1 ⊓ . . . ⊓ ⊑ . Such an is explanatory if 1 ⊓ . . . ⊓ ⊑ ̸∈ , is satisfiable if 1 ⊓ . . . ⊓ is satisfiable w.r.t. , is relevant if ∅ ̸|= 1 ⊓ . . . ⊓ ⊑ , and (syntactically) minimal if there is no other explanation ′ for such that ′ ⊊ .
Note that the given set of hypothesis allows for restricting the set of concepts that can be used in explanations, but may also contain all concepts used in the knowledge base.
In the remainder, we are interested in finding explanations that are explanatory, satisfiable, relevant, and (syntactically) minimal. Abusing notation, for a set of concepts = {1, . . . , }, we also write |= ⊑ instead of |= 1 ⊓ . . . ⊓ ⊑ .
Example 1. Consider the knowledge base containing the axioms
⊑ ∃.
∃. ⊑
(
Algorithm 1: Finding one explanation
Minimize(, ℋ, ): compute a minimal explanation for the concept abduction problem
⟨, ℋ, ⟩
input : a knowledge base , a set of hypotheses ℋ, and an observation such that
|= ℋ ⊑
output : a minimal explanation ⊆ ℋ such that |= ⊑ (cf. Definition 1)
1 ← ℋ ;
2 for ∈ ℋ do
3 if |= ( ∖ {}) ⊑ then
4 ← ∖ {};
5 return ;
Among these only 1 is explanatory, relevant, satisfiable, and minimal. We have that 2 is not
explanatory since ⊓ ′ ⊑ ∈ , and 3 is not satisfiable (due to Axiom (
Before proposing our approach, we point out that the number of (minimal) explanations for a given observation may be exponential in the size of the knowledge base. We start by showing how to compute one explanation before generalizing the approach to compute all explanations, ifrst, using hitting set trees and, then, via a SAT encoding.
Given a concept abduction problem = ⟨, ℋ, ⟩, a naive algorithm for computing one explanation such that |= ⊑ is relatively easy. If ̸|= ℋ ⊑ , there is no satisfiable explanation and we can stop. Otherwise, we start from = ℋ and repeatedly remove concepts from as long as this does not break the entailment |= ⊑ . At a certain point, no concept can be removed without breaking the entailment, which implies that is a minimal explanation w.r.t. . Algorithm 1 summarizes this idea. Note that Algorithm 1 makes calls to a reasoning service for concept subsumption checking without relying on a particular kind of procedure (e.g., tableau-based as well as consequence-based procedures may be used). It remains to check whether the returned is explanatory, satisfiable, and relevant, which requires at most two further subsumption checks and a check for set containment.
The correctness of Algorithm 1 relies on the fact that a conjunction with additional conjuncts is more specific: Lemma 1. Let be a DL knowledge base, and ′ two sets of atomic concepts such that ′ ⊆ , and an atomic concept. Then |= ′ ⊑ implies |= ⊑ .
Proof Sketch. Intuitively, the interpretation of a conjunction is more restricted the more conjuncts are contained in the conjunction.
Note that Lemma 1 only relies on the semantics of conjunctions and subsumption, which is shared among all DLs. We show that Algorithm 1 is correct under the assumed semantics. Theorem 1. Let be the output of Algorithm 1 for the input , ℋ, and such that |= ⊑ . Then is a minimal explanation for the abduction problem ⟨, ℋ, ⟩.
Proof Sketch. Since |= ℋ ⊑ by assumption, is initialized such that |= ⊑ (in Line 1). Since we only remove a concept from , if the subsumption still holds in Line 4, |= ⊑ is preserved. We can further show that is minimal explanation as unneeded conjuncts are step by step removed.
Finally, observe that a run of Algorithm 1 requires exactly subsumption tests, where = ||ℋ||, which is bounded by the number of concepts in (two further subsumption tests and a set containment test are needed for checking whether is relevant, satisfiable, and explanatory). Hence, the complexity of computing one minimal explanation is bounded by a linear function over the complexity of subsumption checking. In particular, for tractable languages such as ℰ ℒ and its tractable extensions [16], one (minimal) explanation for the concept abduction problem can be computed in polynomial time, which is worst-case optimal [12].2 For DLs where subsumption checking is ExpTime-complete such as ℒ [17, 18], the algorithm requires worst-case exponential time.
An explanation for a concept abduction problem ⟨, ℋ, ⟩ consists of concepts that are subsumed by the observation. As we have seen in Example 1, there can be several diferent explanations. To find all explanations, it is, therefore, necessary to change a concept in every explanation of ⟨, ℋ, ⟩ and the question of how to compute all (minimal) explanations arises.
Note first, that the output of Algorithm 1 depends on the order in which the axioms in are enumerated in the for-loop (Line 2). Diferent orders of the concepts can result in diferent removals and, consequently, diferent explanations.
Lemma 2. For each (minimal) explanation of a concept abduction problem ⟨, ℋ, ⟩, there exists some order of concepts in ℋ for which Algorithm 1 with the input , ℋ, and returns . Proof Sketch. Assume, to the contrary of what is to be shown, that a minimal explanation is not returned. We can show that processing first concepts in ℋ ∖ and then concepts from leads to a contradiction as desired. 2Note that although subsumption checking for ℰℒ++ is tractable, the complexity of checking whether an explanation exists is found to be NP-complete by Bienvenu [12]. This apparent contradiction is because unsatisfiable explanations (which can only occur in logics that can express unsatisfiable concepts/ ⊥, as ℰℒ++) are excluded in the definition of Bienvenu as explanations. Our algorithm, however, might terminate with an unsatisfiable explanation. If that has to be avoided, some form of backtracking for such cases would be needed, which indeed then leads to a higher complexity of the problem. ′ ⊥
⊥ ′ ⊥
′
The property stated in Lemma 2 means that for computing all explanations for = ⟨, ℋ, ⟩, it is suficient to run Algorithm 1 for all possible orders of concepts in ℋ. As the number of explanations can be exponential in , the exponential behavior of an algorithm for computing all explanations cannot be avoided in general. Unfortunately, the described algorithm is not very practical since it performs exponentially many subsumption tests for all inputs, even if, e.g., has just one explanation. This is because this algorithm is not goal-directed: the computation of each next explanation does not depend on the explanations computed before.
Hence, the question arises, how we can we find a more goal-directed algorithm. Suppose that we have computed an explanation 1 using Algorithm 1. The next explanation 2 must be diferent from 1, so 2 should miss at least one axiom from 1. Hence the next explanation 2 can be found by finding 1 ∈ 1 such that |= (ℋ ∖ {1}) ⊑ and calling Algorithm 1 for the input , ℋ ∖ {1}, and . The next explanation 3, similarly, should miss something from 1 and something from 2, so it can be found by finding some 1 ∈ 1 and 2 ∈ 2 such that |= (ℋ ∖ {1, 2}) ⊑ and calling Algorithm 1 for the input , (ℋ ∖ {1, 2}), and . In general, when explanations (1 ≤ ≤ ) are computed, the next explanation can be found by calling Algorithm 1 for the input , (ℋ ∖ { | 1 ≤ ≤ }), and such that ∈ (1 ≤ ≤ ) and |= (ℋ ∖ { | 1 ≤ ≤ }) ⊑ . Enumeration of subsets ℋ ∖ { | 1 ≤ ≤ } can be organized using a data structure called a hitting set tree. Definition 2. Let = ⟨, ℋ, ⟩ be a concept abduction problem. A hitting set tree (short: HS-tree) for is a labeled tree = (, , ) with ̸= ∅ such that: 1. each non-leaf node ∈ is labeled with an explanation () = for and, for each ∈ , has an outgoing edge ⟨, ⟩ ∈ with label (, ) = , and 2. each leaf node ∈ is labeled by a special symbol () = ⊥.
For each ∈ , let () be the set of edge labels appearing on the path from to the root node of . Then the following properties should additionally hold: 3. for each non-leaf node ∈ , we have () ∩ () = ∅, and 4. for each leaf node ∈ , we have ̸|= (ℋ ∖ ()) ⊑ . Example 2. Consider the concept abduction problem = ⟨, ℋ, ⟩ with = {′ ⊑ , ′ ⊓ ⊑ ⊥, ⊓ ⊑ }, ℋ = {, ′, , }, and = , which has the (minimal) explanations 1 = {′, } (not satisfiable), 2 = {, } (not explanatory), and 3 = {′, } (satisfiable, explanatory, and relevant). Figure 2 shows an HS-trees for , where the explanation 2 = {, } labels two diferent nodes of the tree.
We next prove that every HS-tree must contain every explanation at least once. Lemma 3. Let = (, , ) be an HS-tree for the concept abduction problem = ⟨, ℋ, ⟩. Then, for each explanation for , there exists a node ∈ such that () = . Proof Sketch. Using Lemma 1 and Conditions 1, 3 and 4 of Definition 2, we can show that a node ∈ for which () is maximal (w.r.t. set inclusion) and () ∩ = ∅ is such that () = .
We next show that each HS-tree = (, , ) for a concept abduction problem = ⟨, ℋ, ⟩ has at most exponentially many nodes in the number of concepts in ℋ. Lemma 4. Every HS-tree for a concept abduction problem = ⟨, ℋ, ⟩ has at most ∑︀0≤ ≤ nodes, where is the number of concepts in ℋ.
Proof Sketch. By analyzing Conditions 1 and 3 of Definition 2, we can show that both the depth and the branching factor of is bounded by ||ℋ||, which gives the desired bound.
For constructing an HS-tree = (, , ) for a concept abduction problem = ⟨, ℋ, ⟩, we can use Reiter’s Hitting Set Tree algorithm (or short: HST-algorithm) [11, 19]: We start by creating the root node 0 ∈ . Then we repeatedly assign labels of nodes and edges as follows. For each ∈ , if () was not yet assigned, we calculate (). If ̸|= (ℋ ∖ ()) ⊑ , we label () = ⊥ according to Condition 4 of Definition 2. Otherwise, we compute an explanation for |= (ℋ ∖ ()) ⊑ using Algorithm 1 and set () = . Note that satisfies Condition 3 of Definition 2 since ⊆ (ℋ ∖ ()). Next, for each ∈ , we create a successor node of and label (, ) = . This ensures that Condition 1 of Definition 2 is satisfied for . Since, by Lemma 4, has a bounded number of nodes, this process eventually terminates.
Algorithm 2: Computing all explanations by the Hitting Set Tree algorithm ComputeExplanationsHST(, ℋ, ): compute all explanations for ⟨, ℋ, ⟩ input : a knowledge base , a set of hypotheses ℋ, and an observation such that |= ℋ ⊑ output : the set of all (minimal) subsets ⊆ ℋ such that |= ⊑ 1 ← ∅ ; 2 ← {∅} ; 3 while ̸= ∅ do 4 ← choose ∈ ; 5 ← ∖ {}; 6 if |= ℋ ∖ ⊑ then 7 ← Minimize(, ℋ ∖ , ); 8 ← ∪ {}; 9 for ∈ do 10 ← ∪ { ∪ {}}; 11 return ; Note that unlike the algorithm sketched in Lemma 2, the input for each call of Algorithm 1 now depends on the results returned by the previous calls.
The main idea of the HST-algorithm is to systematically compute two kinds of sets: (
Definition 3. Let be a set of sets of some elements. A set is a hitting set for if ∩ ̸= ∅ for each ∈ . A hitting set for is minimal if every ′ ⊊ is not a hitting set for .
Intuitively, a hitting set for is a set that contains at least one element from every set ∈ . An HS-tree is then a tree = (, , ) such that for each ∈ , () is a hitting set of the set of explanations on the path from to the root of . The leaf nodes of are labeled by hitting sets () such ̸|= (ℋ ∖ ()) ⊑ . Intuitively, the set () represents a set such that the removal of () from ℋ breaks the subsumption.
We get following bound on the number of subsumption tests performed by the HST-algorithm: Lemma 5. An HS-tree for a concept abduction problem = ⟨, ℋ, ⟩ can be constructed using at most ∑︀1≤ ≤ +1 subsumption tests, where is the number of concepts in ℋ. Proof. We call Algorithm 1 exactly once per node. Combined with Lemma 4, we get the desired bound on the number of subsumption tests performed by the HST-algorithm.
The HST-algorithm can further be optimized in several ways. First, it is not necessary to store the complete HS-tree in memory. For computing an explanation at each node , it is suficient to know just the set (). For each successor of associated with some ∈ (), the set () can be computed as () = () ∪ {}. Hence, it is possible to compute all explanations by recursively processing and creating the sets () as shown in Algorithm 2. The algorithm saves all explanations in a set , which is initially empty (Line 1). The explanations are computed by processing the sets (); the sets that are not yet processed are stored in the queue , which initially contains (0) = ∅ for the root node 0 (Line 2). The elements of are then repeatedly processed in a loop (Lines 3–10) until becomes empty. First, we choose any ∈ (Line 4) and remove it from (Line 5). Then, we test whether |= (ℋ ∖ ) ⊑ (Line 6). If the subsumption holds, this means that the corresponding node of the HS-tree with () = is not a leaf node. We then compute an explanation using Algorithm 1 and add it to (Lines 7–8). Further, for each ∈ , we create the set () = () ∪ {} for the corresponding successor node of and add () to for later processing (Lines 9–10). If the subsumption |= (ℋ ∖ ) ⊑ does not hold, we have reached a leaf of the HS-tree and no further children of this node should be created.
Lemma 6. Given , ℋ, and as input, Algorithm 2 returns all explanations for the concept abduction problem = ⟨, ℋ, ⟩.
Proof Sketch. We can prove the claim by showing that the following invariant always holds in the main loop (Lines 3–10): If is an explanation for , then either ∈ or there exists ∈ such that ⊆ ℋ ∖ .
Note that, as before, checking whether a returned subsumption is explanatory, satisfiable, and relevant requires at most two subsumption and a set membership check.
The main idea of the HST-algorithm is to systematically compute two kinds of sets: (
Suppose that we have already computed some set of explanations and some set of hitting
sets for the concept abduction problem = ⟨, ℋ, ⟩. How can we find a new explanation?
As mentioned, each new explanation must be a hitting set for , i.e., it should contain one
concept from every set in . Furthermore, it should be diferent from any of the previously
computed explanations, i.e., it should miss one axiom from every ∈ . Suppose we have
found a subset ⊆ ℋ satisfying these two requirements:
∀ ∈ : ∩ ̸= ∅,
(
Maximize(, ℋ, , ): compute a maximal subset ⊆ ℋ such that ⊆ and
̸|= ⊑
input : a knowledge base , a set of hypotheses ℋ, a subset ⊆ ℋ , and an
observation such that ̸|= ⊑
output : such that ⊆ ⊆ ℋ such that ̸|= ⊑ but |= ′ ⊑ for every
′ with ⊊ ′ ⊆ ℋ
1 ← ;
2 for ∈ ℋ ∖ do
3 if ̸|= ( ∪ {}) ⊑ then
4 ← ∪ {};
5 return ;
can find a maximal superset of ( ⊆ ⊆ ℋ ) such that ̸|= ⊑ : see Algorithm 3.
Note that (
The question arises, how we can find a set satisfying Conditions (
To formulate the propositional encoding, we assign to each concept ∈ ℋ a fresh
propositional variable . Then, every interpretation ℐ determines a set = (ℐ) = { ∈ ℋ | ℐ =
1} of concepts whose corresponding propositional variable is true. We construct a propositional
formula such that ℐ = 1 if and only if (ℐ) satisfies (
∈ ∈
∈ ∈
(
= (, ) = (¬ ∨ ¬′ ) ∧ (¬ ∨ ¬′ ) ∧ ( ∨ ). has a model ℐ with ℐ = 1 and ℐ = ℐ = ℐ′ = 0, which gives (ℐ) = {}.
Once the set determined by a model ℐ of is found, we can extract either a new explanation
or a new minimal hitting set from by minimizing the subsumee using Algorithm 1
or maximizing non-subsumption using Algorithm 3. After that, we can update according
to (
Algorithm 4: Computing all explanations using a SAT solver
ComputeExplanationsSAT(, ℋ, ): compute all explanations for the concept abduction problem = ⟨, ℋ, ⟩ input : a knowledge base , a set of hypotheses ℋ, and an observation such that |= ℋ ⊑ output : the set of all minimal subsets ⊆ ℋ such that |= ⊑
Maximize(ℋ, ℋ, , ); ∧ ⋁︀{ | ∈ ℋ ∖ }; ← ← 13 return ;
Algorithm 4 summarizes the described procedure for computing all explanations for a concept
abduction problem = ⟨, ℋ, ⟩ using a SAT solver. We start by creating an empty set of
explanations (Line 1) and a formula that is always true (Line 2). Then, in a loop (Lines 3–12), as
long as is satisfiable (which is checked using a SAT solver), we take any model ℐ of (Line 4),
extract the corresponding set = (ℐ) that it defines (Line 5), and check the subsumption
|= ⊑ . If the entailment holds, using Algorithm 1 we compute an explanation for
|= ⊑ (Line 7), which, by Lemma 1, is an explanation for . This explanation is then
added to (Line 8) and is extended with a new conjunct for this explanation according to (
Example 4. Consider the concept abduction problem = ⟨, ℋ, ⟩ from Example 1 and propositional encoding of concepts in ℋ from Example 3. The following table shows a run of Algorithm 4 for the inputs , ℋ, and . Every row in this table corresponds to one iteration of the while-loop (Lines 3–12). The first column gives the value of the interpretation ℐ for computed in this iteration. The second column shows the value of computed for this interpretation and whether the entailment |= ⊑ holds. The third column shows the result of minimizing the subsumee or maximizing the non-subsumption using Algorithms 1 and 3. The last column shows the conjunct that is added to for the corresponding explanation or minimal hitting set. |= min( ) ⊑ / ̸|= max( ) ⊑ ̸|= {, } ⊑ ̸|= {, } ⊑ |= {, } ⊑ |= {, ′} ⊑ |= {, ′} ⊑ ̸|= {, ′} ⊑
∨ ′ ∨ ′ ¬ ∨ ¬ ¬ ∨ ¬′ ¬ ∨ ¬′ ∨
We briefly discuss similarities and diferences between Algorithm 2 and Algorithm 4: Both algorithms systematically explore subsets of ℋ and minimize the subsumee from such subset to compute explanations. Algorithm 2 constructs such subsets (ℋ ∖ ) manually by removing one axiom appearing in the previously computed explanation (if there is any) in all possible ways. Algorithm 4 enumerates such subsets with the help of a SAT solver. The main diference is that Algorithm 2 may encounter the same subsets many times (on diferent branches), whereas the propositional encoding in Algorithm 4 ensures that such subsets never repeat. Of course, an iteration of Algorithm 2 cannot be directly compared to an iteration of Algorithm 4. Both iterations use at most one call to Algorithm 1, but Algorithm 4 may also require a call to Algorithm 3, as well as checking satisfiability of . The latter requires solving an NP-complete problem, for which no polynomial algorithm is known so far. In order to check satisfiability of , a SAT solver usually tries several (in worst-case exponentially many) propositional interpretations until a model of is found. As each such interpretation ℐ corresponds to a subset (ℐ) ⊆ ℋ , this process can be compared to the enumeration of subsets in Algorithm 2. However, a SAT solver usually implements a number of sophisticated optimizations, which make the search for models very eficient in practice, whereas the subset enumeration strategy used by Algorithm 2 is rather simplistic. Hence Algorithm 4 is likely to win in speed. On the other hand, Algorithm 4 requires saving all explanations (and minimal hitting sets) in the propositional formula , which might result in a formula of exponential size, if the number of such explanations or hitting sets is exponential. In this regard, Algorithm 2 could be more memory eficient since saving (all) explanations is optional (see the discussion at the end of Section 3.2). Hence both algorithms have their own advantages and disadvantages.
We have presented two alternative algorithms for computing (all or some) solutions to the concept abduction problem: one algorithm is based on Reiter’s hitting set tree algorithm, whereas the other one relies on a SAT encoding. It remains to be analyzed how these algorithms behave in practice and how these algorithms difer on diferent real-world ontologies, where an important aspect is also finding eficient incremental SAT solvers.
In contrast to previous work, the algorithms do not rely on a refutation-based calculus and, hence, can be used also with eficient reasoners for tractable DLs such as ℰ ℒ and its extensions. Another direction for future work is extending the approach to other forms of (logic-based) abduction, e.g., to ABox abduction and a comparison with other existing approaches, which are mostly focusing on ABox abduction.