Finding Justifications by Approximating Core for Large-scale Ontologies

1 Introduction and Background

Recent years, automated reasoning techniques in description logics have been developed for computing not only concept subsumption, but also to find justifications causing each subsumption. In the early research stages, Schlobach et al. first proposed the glass-box approach based on the tableau extension strategy to find Minimal unsatisfiability-preserving subTBoxes(MUPS), which is actually a special justification, in any expressive description logic languages. The main idea of the glass-box is to use the rules of the tableau to expand. In the process of expansion, once a conflict occurs, the elements on the path that caused the conflict are the causes(may not be the minimal) of the inconsistency of the ontology. Certainly, there may be more than one such path. After that, Kalyanpur et al. extended the interpretation of the unsatisfiable concept to the interpretation of general axioms and named it as justification. They introduced a black-box method which could be easily and robustly implemented to debugging ontologies. The black-box algorithm uses the reasoner solely as a subroutine and the internals of the reasoner do not need to be modified.

∗Contact Author

With the advent of a series of the light-weight ontology(such as the EL family, etc.), it began to consider novel strategies to find justifications for such ontologies. Since the language complexity of the ontology is reduced, the size of the ontology becomes larger, relatively. Considering the characteristics of the light-weight ontology, it is feasible to encode the classification of the ontology such as the EL family into the form of the Horn proposition formula, thus transforming finding justifications into computing all MUSes of the propositional formula. Baader used SAT based to find justifications for SNOMED-CT ontology in [Baader and Suntisrivaraporn, 2007]. The method built an exponential-size monotone propositional formula from a classification of terminology. [Sebastiani and Vescovi, 2009] used the boolean constraint propagation and conflict analysis of the SAT solver to compute the concept subsumptions and perform finding justifications. It's based on a polynomial-size Horn propositional formula. [Arif et al., 2015] exploited an important relationship between minimal axiom sets and minimal unsatisfiable subformulas in the propositional domain. The encoding of this method also adopts a polynomial-size Horn propositional formula. In addition, [Ignatiev et al., 2017] describes different improvements that have been considered since the translation was firstly proposed. Clauses of the encoded unsatisfiable formula are partitioned into groups. The recent work [Kazakov and Skocovsk´y, 2018] is based on the extension of the resolution method with so-called answer literals. According to the experiment of the paper, it was able to compute all justifications for all direct subsumptions of SNOMED-CT in about 1.5 hour.

2 RelatedWork

Recent years, some of approximation methods to reduce the set of clauses that must be tested for exclusion from the MUS have been proposed. The following methods were compared in [Gr´egoire et al., 2007]. AMUSE proposed the algorithm adapting the "learning process" of a modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. The unsatisfiable cores obtained by this way could be helpful in diagnosing the causes of infeasibility in large systems. Zcore served to find a fixed point in the unsatisfiable sub-formulas computed by proof-producing SAT solvers, that is, it aimed to remove irrelevant clauses that can be included by SAT solvers while generating an unsatisfiable sub-formula. AOMUS associating a score with each clause was based on LS exploited the fact that clauses in MUSes are likely to be unsatisfied often during LS. Experimental results illustrated that AOMUS proved more competitive with respect to both the required run-times and the quality of the delivered approximations of MUSes, in the sense that smallersizes approximations were obtained most often. In this paper, we adopt LS technique to optimize finding justifications based on SAT encoding. It aims to pre-select a subset of axioms corresponding to an accurate justification as small as possible from a large-scale ontology.

3 ResearchGoals and Expected Contributions

SAT solver is used to determine the satisfiability of formulas during finding justifications. It's complete but expensive. However, the computational cost based on incomplete LS technology is much lower. We use it instead of SAT solver to detect an approximating core in advance. The approximating core is identified by taking critical clause into account. Intuitively, a critical clause is a falsified clause that becomes true thanks to a local search flip only when some other clauses become false at the same time. It must be complete in the sense that it always delivers a MUS for any unsatisfiable SAT instance. By introducing this incomplete LS before the complete SAT solving, the scope of the axioms for finding justifications will be reduced to the single-digit scale. A justification will be computed by iterating process for an amount of time up-to-linear in the size of the first approximating core was found.

4 Preliminary Results

The experiment mainly compares the time and the size of clauses calculated with Zcore and LS. We modified the ontologies in the same way as [Sebastiani and Vescovi, 2009] in order to be compliant with the input grammar of EL+2SAT. It removed the comments and annotations of the ontologies and also rewrote the axioms with purely syntactic transformations. Table 1 records the detailed experimental results. We experimented with NOT-GALEN, the Gene Ontology(GO), NCI and FULL-GALEN. In the query file for the four ontologies, 20 queries were randomly selected for the experiment. #var represents the number of literals in the formula obtained by encoding, and #cla corresponds to the number of the clauses. It also records the computing time and the size of the approximating core for each query using LS and Zcore, respectively. Calculating in the approximating way can quickly locate the ontology used for finding justifications from the original scale in 4th power of 10 to the single digit level. LS always delivers an approximating core within a reasonable time less than Zcore, and delivered clauses are often similar to the clauses obtained by Zcore.

5 Conclusion and FutureWork

Our approach is based on encoding the ontology classification procedure into Horn clauses. It introduces the process of computing the approximating core by LS before calculating a MUS. Experiments show that the approach proposed in this paper deserves further study. From the experimental data, the method can greatly reduce the scale of the axioms used for finding justifications. It is also proved that the larger the scale of the ontology, the more obvious the effect of LS. The work of calculating the approximating core by using LS has been completed. In the following, we will use the Insertion method to calculate the MUS, and then use the method proposed in [Ignatiev et al., 2017] to calculate the MUSes. At last, MUSes are decoded into all justifications for given queries. We expect that the results of the experiment will be very substantial and of practical value.