SAT encoding of unification in ℰℒ

Abstract

Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in ℰℒ is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problems in ℰℒ, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state-of-the-art SAT solvers when implementing an ℰℒ-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that ℰℒ-unification is in NP that is much simpler than the one given in our previous paper on ℰℒ-unification. © 2010 Springer-Verlag.