An SAT-based Decision Procedure for ALC

Description Logic Papers from the Fifth International Conference on Principles of Knowledge Representation and Reasoning

The goal of this paper is to describe and thoroughly test a decision procedure, called KSAT, checking satisfiability in the terminological logic ACC. KSAT is said to be SATbased as it is defined in terms of a decision procedure for propositional satisfiability (SAT). The tests are performed comparing KSAT with, among other procedures, KRIS, a state-of-the-art tableau-based implementation of a decision procedure for ALe. KSAT outperforms KRIS of orders of magnitude. Furthermore, the empirical results highlight an intrinsic weakeness that tableau-based decision procedures have with respect to SATbased decision procedures.