A SAT-based decision procedure for ALC
Fausto Giunchiglia, Roberto Sebastiani · 1996
The goal of this paper is to describe and thoroughly test a decision procedure, called Ksat, checking satisfiability in the terminological logic ALC. Ksat is said to be SAT-based 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 ALC. Ksat outperforms Kris of orders of magnitude. Furthermore, the empirical results highlight an intrinsic weakeness that tableau-based decision procedures have with respect to SAT-based decision procedures. Franz Baader, Marco Cadoli, Enrico Franconi, Enrico Giunchiglia, Fabio Massacci and Bernhard Nebel have given very useful feedback. Fabio Massacci has suggested testing the Halpern & Moses formulas. Marco Roveri has given technical assistance in the testing phase. All the members of the Mechanized Reasoning Group in Genoa have put up with many weeks of CPU-time back...