The AECN Description Logic Concept Satisfiability as a SAT Problem

摘要

In this paper we propose a procedure for encoding the AECN Description Logic concept satisfiability into SAT problem. In particular, a concept description is translated into the set of propositions, which is satisfiable iff the description is satisfiable, as well. The satisfiability of the resulting propositions is tested by SAT solving tools based on the DPLL procedure and widely known for their efficiency. We describe and analyse the results of preliminary experiments aimed at evaluating the performance of the presented approach.