We propose a novel approach to axiom pinpointing based on a reduction to the SAT task of minimal unsatis able subformula enumeration, allowing highly optimized algorithms and data structures developed for SAT solving in the last two decades to be used in this problem. Exploiting the speci c properties of axiom pinpointing, we apply further optimizations resulting in considerable runtime improvements of several orders of magnitude. Our ideas are implemented in SATPin, a system capable of performing axiom pinpointing in large biomedical ontologies faster than other existing tools. While our paper focuses on a slight extension of EL, the presented approach directly generalizes to all ontology languages for which consequence-based reasoning methods are available.
Axiom pinpointing is the task of identifying the axioms in an ontology that are
responsible for a consequence to follow. This task has been successfully used to correct
modeling errors and understand unexpected consequences from very large ontologies.
For example, the 2007 version of the very large bio-medical ontology Snomed CT3
incorrectly implied that every amputation of nger was also amputation of arm; i.e.,
whenever a patient had a nger amputated, the ontology would imply that they had
also lost their arm. Using automated axiom pinpointing tools it was possible to identify
the 6 axioms (from over 300,000) that caused this error [
For EL+ ontologies [
We implemented these optimizations in the new SATPin system. We compared the e ciency of SATPin against other axiom-pinpointing tools over real-life bio-medical ontologies that have been used as benchmarks before. Our experiments show that SATPin is an e cient tool for axiom pinpointing that can be used in practice over large inputs. Interestingly, our approach depends only on the structure of the propositional formula, and can be directly generalized to any other ontology language allowing consequence-based reasoning beyond EL+. 2
We assume that the reader is familiar with the DL EL+, and brie y describe the
completion algorithm for deciding subsumption in this logic [
In the completion phase, the normalized ontology NF(T ) is saturated through an exhaustive application of completion rules of the form A ) , where A [ f g is a nite set of axioms in normal form. This rule is applicable to the ontology T if A T ; its application adds to T . Completion rules generate the logical closure of the axioms in normal form w.r.t. a limited signature. For example, the EL+ completion rule fX v Y; Y v Zg ) X v Z expresses that if the two subsumption relations X v Y , Y v Z hold, then X is also subsumed by Z. In general, the rule A ) states that if all the axioms in A hold, must hold too. To ensure termination, the rule A ) is only applicable if 2= T 0. R denotes the set of all completion rules. Let c(T ) be the ontology obtained from T after normalization and completion. For every two concept names A; B appearing in T , T j= A v B i A v B 2 c(T ); i.e., the completion algorithm makes all the implicit subsumptions between concept names that can be derived from T explicit.
Example 1. Consider the ontology Texa := fA v 9r:A u Y; Y v B; 9r:Y v Bg: The last two axioms are already in normal form, but the axiom A v 9r:A u Y is not. It can be transformed to normal form by separating the conjunction on the right-hand side of the axiom, as described before. Hence,
NF(Texa) = fA v 9r:A; A v Y; Y v B; 9r:Y v Bg: Applying the completion rules to this normalized ontology yields c(Texa):=fA v 9r:A; A v Y; Y v B; 9r:Y v Bg[fA v 9r:Y; A v 9r:B; A v Bg: We conclude Texa j= A v B, as this subsumption relation appears in c(Texa). In axiom pinpointing we are interested in nding the axiomatic causes for a subsumption to hold, in order to understand this consequence. Thus, we want all the minimal sub-ontologies that entail this subsumption.
De nition 2 (MinA). A MinA for A v B w.r.t. the ontology T is a subset M T s.t. (i) M j= A v B and (ii) for all S M, S 6j= A v B. Axiom-pinpointing is the task of nding all MinAs for a subsumption w.r.t. an ontology. For instance, there are two MinAs for A v B w.r.t. the ontology Texa of Example 1: M1 := fA v 9r:A u Y; Y v Bg; and M2 := fA v 9r:A u Y; 9r:Y v Bg.
One approach for solving this problem is to create a Horn formula whose satisfying interpretations can be mapped to sub-ontologies entailing the subsumption relation. Before describing this reduction in detail, we recall some basic notions of SAT. Consider a xed in nite set V of Boolean variables. A literal is a variable v (positive literal ) or a negated variable v (negative literal ). The variable of a literal x is denoted as var(x). The complement x of a positive (negative) literal x is the negative (resp., positive) literal with the same variable as x. The complement of a set of literals S is S := fx j x 2 Sg. A clause C is a nite set of literals, representing the disjunction of its elements. A clause containing single literal is called a unit clause. Formulas are nite multisets of clauses, which intuitively represent the conjunction of its elements; i.e., we consider only formulas in conjunctive normal form. For two clauses C1; C2 with x 2 C1, and x 2 C2, the resolvent of C1 and C2 upon x is the clause C1 x C2 := (C1 n fxg) [ (C2 n fxg).
A sequence of literals M is consistent, if x 2 M implies x 2= M . For simplicity, we view consistent sequences M as sets throughout this paper. An interpretation is a consistent set of literals I. The reduct F jI of a formula F with respect to the interpretation I is the multiset F jI := fC n I j C 2 F; C \ I = ;g. I satis es a formula F if F jI = ;. F is satis able if there is an interpretation that satis es it. The standard reasoning problem in SAT is to decide satis ability of a formula.
A major operation in modern SAT solvers is unit propagation, based on the fact that a unit clause C = fxg is only satis ed by interpretations using the literal x. Given a formula F and a consistent sequence M of literals, unit propagation returns the set of all literals (including M ) that must occur in an interpretation to satisfy F jM . The interpretation J is initialized with M . If there are unit clauses in the current reduct, J is extended with the corresponding literal. Additionally, the clause C is stored as the reason for this extension. If no further unit clauses can be found, the algorithm returns the nal interpretation J .
Most modern SAT solvers follow essentially the same approach, known as
CDCL [
One approach for axiom pinpointing originally proposed in [22] builds a propositional formula that simulates the process of the completion algorithm. The computation of the MinAs for an atomic subsumption is thus reduced to an enumeration problem over this formula. We brie y describe this translation next, but refer the reader to [22] for all the details. For every axiom 2 T [ c(T ) we introduce a unique Boolean variable x , which represents the axiom throughout the completion process. Then, we build the formula FT := Fn [ Fc, where
Fn := ffx ; x g j 2 T ;
2 NF( )g; Fc := ffx g [ fx j
2 Ag j A ) These formulas describe all the possible causes for an axiom to appear in c(S) for some subontology S of T . The clauses in Fn (equivalent to implications x ! x ) state that, for every axiom occurring in S, all the axioms in normal form generated by must be in c(S). The formula thus simulates the normalization step. Similarly, the completion rule A ) expresses that if all axioms in A are contained in c(S), then so must be ; this logical dependency is expressed in the clauses of the formula Fc which can equivalently be written as V 2A x ! x . 2 R; A [ f g c(T )g: Example 3. Consider again the ontology Texa from Example 1. For brevity, we use the following shorthand for the axioms in Texa [ c(Texa): 1 : A v 9r:A u Y , 2 : Y v B, 3 : 9r:Y v B, 1 : A v 9r:A, 2 : A v Y , 3 : A v 9r:Y , 4 : A v 9r:B, 5 : A v B. Then, Fn = ffx 1 ; x 1 g; fx 1 ; x 2 gg since the axioms 1 and 2 are generated by the normalization of the axiom 1, and all other axioms in Texa are already in normal form. The formula Fc is composed by the clauses
fx 1 ; x 2 ; x 3 g; fx 3 ; x 2 ; x 4 g; fx 2 ; x 2 ; x 5 g; fx 3 ; x 3 ; x 5 g; fx 1 ; x 5 ; x 4 g: There are two clauses in Fc that entail 5. Although the completion algorithm uses only one of them, the translation to SAT must preserve both to know all the possible ways in which axioms can be derived from the knowledge in Texa. Given S T , let XS := ffx g j 2 Sg; i.e., the conjunction of all the variables from the axioms in S. A model I of XS ^ FT satis es S[c(S) f jx 2Ig. On the other hand, the set fx j 2 S [ c(S)g is a model of XS ^ FT . It follows that S j= A v B i xAvB 2 I for all interpretations I satisfying XS ^ FT . This means that, in order to nd all MinAs for A v B w.r.t. T , it su ces to compute all minimal subsets M of XT such that M ^ FT ^ fxAvBg is unsatis able. Notice that XT ^ FT is always satis able. On the other hand, since T j= A v B, the formula XT ^ FT ^ fxAvBg is unsatis able. Hence, this problem is well-de ned. 3
We have constructed, from an ontology T , the formula FT that encodes the derivation steps made by the completion algorithm, and the set of choice variables XT . By construction, XT ^ FT is satis able. Given a consequence , we want to enumerate all the minimal subsets M XT such that M ^ FT ^ x is unsatis able (M ^ FT ^ x ?). Our approach does not depend on the precise shape of the formula FT , but rather on these properties. Hence, we consider an arbitrary satis able formula F , a set X of propositional variables such that X ^ F is satis able, and a propositional variable q such that X ^ F ^ q ?.
Enumerating all minimal subsets M of X such that a formula is unsatis able
is closely related to nding all minimal unsatis able subformulas (MUS) of a
propositional formula [
In essence, we make several calls to a SAT solver to nd all MinAs. For the rst MinA, we try to prove satis ability of X ^ F ^ q choosing, at search decisions, a variable from X to be satis ed. This process eventually leads to a con ict. Con ict analysis yields an M X that led to the con ict (a MinA). Learning the negation of this MinA guarantees that the con ict cannot be found again. The same approach leads to the next MinA, repeating this process until no more con icts exist. To handle large ontologies, many optimizations are needed.
Incremental SAT Solving. To nd one MinA, we use incremental SAT [
Minimizing the Candidate Set. Algorithm 1 nds a (possibly not minimal) set M s.t.
(M ^ F ) ! q. To reduce M to a MinA, we use con ict analysis [
X and (F ^ R) ! q ENU1 S := ; ENU2 R := implies(F; q; X; reason) // Is there a MinA? ENU3 if R = ? then return ; // there are no MinA ENU4 setup enumerator(X) // setup enumeration ENU5 while > // check all candidates ENU6 if R 6= ? // if there was a MinA ENU7 R := minimize(F; R; q) // minimize candidate ENU8 S := S [ fRg // add R to set of MinAs ENU9 if enumerator.avoid(R) = ? // disallow this MinA ENU10 break // no more MinAs ENU11 if enumerator.hasNext() = ? // Do other MinAs exist? ENU12 break // no more MinAs ENU13 M := enumerator.next() // next MinA candidate ENU14 R := implies(F; q; M; reason) // Is there a MinA? ENU15 return S // return set of MinAs x 1 ; x 2 , and x 3 . At this point, a new choice is needed. If we activate x 2 , then unit propagation enforces x 5 to be true, nding a contradiction; i.e., f 1; 2g is a MinA. We learn the clause fx 1 ; x 2 g and restart the incremental SAT solver, nding the second MinA f 1; 3g. After disallowing this MinA, the only remaining candidate set is fx 2 ; x 3 g, which does not entail the wanted implication.
Candidate Enumeration. Candidate enumeration is initialized with the set of literals
X. While there are candidates left, a new M X is chosen. A nave approach is to
enumerate all subsets of X as candidates. This is unfeasible as it would need to verify
2jXj candidates, with jXj very large. We partition X into the set of relevant literals
V = lits(S) and the remaining literals T . The relevant literals refer to axioms that
belong to some MinA. At the beginning, we do not know which literals are relevant
and which not. Hence, T is initialized to be X. Whenever a MinA R is found, V and
T are updated accordingly: V := V [ R, and T := T n R; all the variables in this
MinA are now known to be relevant. The new candidates are sets of the form V 0 [ T
for V 0 V . In this way, the number of candidates is bounded by 2jlits(S)j. As jlits(S)j
is typically much smaller than jXj the search space is reduced considerably. Since the
sets T and V change during the execution of the algorithm, it is important to verify
that candidates are never tested twice. We also apply the Hitting Set Tree (HST)
approach developed originally for axiom pinpointing in expressive DLs [
HvB; AvD; DvE; AvG; AvC; CvE; EvB; AvF; F vB | {Tz } | {Vz } We continue searching for new MinAs in all sets T [ V 0 for all proper subsets V 0 of V which do not contain a known MinA. We can pick, e.g., V 0 = fAvC; CvE; AvF g. Then T [ V 0 does not imply the subsumption AvB. Any future MinA must contain at least one of the axioms from V n V 0 = fEvB; F vBg. We continue by trying a new subset of V , e.g. V 0 = fAvC; EvB; AvF g and obtain fAvD; DvE; EvBg as MinA. This again requires to update T and V :
HvB; AvG; AvC; CvE; EvB; AvF; F vB; AvD; DvE | {Tz } | {Vz } The algorithm will then tell us that no other MinAs exist. Recall that typically, the set T will be much bigger than V and using our strategy, we will never have to go through subsets of it.
We realized the enumerator object as a SAT solver. Model enumeration is based on CDCL: once a model I is found, I is added to the formula, and the next model is generated. We add only the decision literals of I: all other literals of I are implied. To avoid repeating MinAs, the literals of every MinA R are added to the formula as clause R, too. For the enumeration, we incrementally add the variables of the last MinA R to the solver. Previous clauses remain valid: previous candidates are not enumerated twice and known MinAs cannot be repeated. For the HST enumeration, we modify the decision heuristic of the solver. A stack of found solutions is kept and the decision heuristic follows the hitting set scheme to enumerate candidates. Finally, inverse enumeration is realized adding the necessary clause X n M to include one of the missing literals. The algorithm spends most time on the imply check, as all literals x 2 X have to be applied. Depending on the ontology, X can be very large: the encoding of Snomed contains 378579 literals. As discussed, the set of relevant literals V = lits(S) might be much smaller. In our experiments, the largest set V found for Snomed contains 88 literals. For each imply check, 378491 (378579 88) literals could be kept in line IMP1. Instead of initializing M = ;, we can initialize M = T to the set of (currently) irrelevant literals. The initialization is sound, since (F ^ T ) 6! q. In the implementation we do not undo and recreate the set M , but keep the last state and only perform the needed updates. Theoretically, this optimization improves the algorithm by two orders of magnitude over Snomed: 99:98 % of the work is saved in the implies routine; i.e., maintaining relevant variables may be the di erence between solvability and unfeasibility. 4
We implemented a new tool called SATPin, based on Minisat 2.2.4 To test our
ideas, we ran SATPin on four well-known EL+ biomedical ontologies, which have
been widely used as benchmarks for DL reasoners, specially in the context of
axiom-pinpointing: the Gene Ontology, NCI, the EL+ version of FullGalen, and the
2010 version of Snomed. All computations ran with a 5h timeout (18000s) on an Intel
Xeon CPU at 2.6GHz and a memory limit of 6.5GB. We compare the performance of
SATPin with the state-of-the-art MUS enumeration tool Marco [
Each ontology was transformed into a propositional formula by el2sat all [22].
Table 1 summarizes the properties of these ontologies and their translations; the
number of axioms in the original ontology is also the number of selection variables
used by SATPin. Snomed is an order of magnitude larger than the other three test
ontologies; in fact, one of the main problems when dealing with Snomed is to handle
the memory consumption issues. For each of the three smaller ontologies, we computed
all the MinAs for 100 di erent consequences: 50 randomly chosen, and 50 selected as
those where the variable xAvB appears the most often in FT , indicating that they
have the most MinAs, as originally designed in [23], and later used also in [
SATPin clearly outperforms the other two tools in GO. In FullGalen, Marco behaves much worse than the other two tools. At rst sight, it seems that SATPin has the worst behavior in NCI by far. However, EL2MUS was faster than SATPin in only 23 of the samples tested for this ontology, and was much slower (up to an order of magnitude) in all others. The median and 90th percentile for SATPin on these tests is lower than those for Marco and EL2MUS. The average performance of SATPin is 4 http://minisat.se/ 5 All experimental data is available at: http://goo.gl/kJ0sE4.
GO
Marco EL2MUS SATPin a ected by three instances that took over 3000s, which explains the huge standard deviation. If only these three instances are removed, the average time taken by SATPin decreases drastically to only 40.55s. A similar, although less extreme situation was observed for FullGalen.
In theory, SATPin is a ected by the branching factor produced by the HST
method, and the number of relevant variables used. This is con rmed in Figure 1,
which shows the proportional speedup of SATPin w.r.t. EL2MUS against the number
of MinAs in each experiment. The improvement shown by SATPin grows inversely to
the number of MinAs. The size and shade of each dot is proportional to the average
MinA size in that instance. Clearly, the relative performance of SATPin decreases as
this average increases: all instances containing large MinAs appear below the dashed
line, which signals where both SATPin and EL2MUS perform equally. Notice that
real-world ontologies are typically well-structured, and their consequences have only a
few MinAs of small size [
We did another experiment to understand the in uence of (i) the order of the selection variables, and (ii) the variable separation optimization. We ran the 20 instances of GO where SATPin behaved the worst again with (i) the order of the selection variables reversed, and (ii) the variable separation optimization deactivated. In the latter, the average CPU time increased from 13 to 279s; increasing in the worst instance from 47 to 1239s; i.e., the optimization is really e ective. The theoretical speedup is 681: at most 30 out of 20466 axioms appear in MinAs; however, this speedup is not reached in practice. When the order of the selection variables was reversed, the CPU time variated to up to 2x in both directions. The relative performance of SATPin against EL2MUS and Marco was not a ected by the ordering.
We compared the performance of SATPin and EL2MUS on the 34 very hard instances from Snomed CT. These instances are so hard that their full set of MinAs was previously unknown. Only 9 of these instances were solved by both tools, and EL2MUS solved three additional ones. The solved cases had in average 16.4 MinAs (maximum 33) with an average size of 14 axioms each. In the other cases, before timing-out SATPin found in average 32 MinAs containing 16 axioms each. In an extreme case, SATPin found 96 MinAs, with up to 30 axioms. EL2MUS succeeded in this case, proving that there existed no more MinAs: SATPin computed the full answer to this instance, but could not verify it within the time limit. Recall that these 34 test cases were specially selected for their hardness; most Snomed CT consequences have less than ten MinAs [26].
Discussion. Other axiom-pinpointing systems for EL+ are Cel [25], Just [
We exploited highly optimized tools and data structures from the SAT community to
produce an e cient tool for axiom pinpointing in EL+. The core of our approach is
based on the construction of a propositional formula encoding the derivation steps of
the completion-based procedure for deciding atomic subsumption. While we focused on
the standard completion algorithm for EL+ [