*SAT, KSATC, DLP and TA: a comparative analysis.
Enrico Giunchiglia, Fausto Giunchiglia, Armando Tacchella · 1999
*sat is our new platform for building decision procedures for modal and description logics. Currently, *sat can test the satisability of a formula in the modal logic K or in the description logic ALC. We comparatively test *sat with some among the fastest solvers for K: KsatC, Dlp and TA. The experimental analysis shows that *sat performs better than or as well as the other systems on the tests we consider. 1 Introduction *sat is our new platform for building decision procedures for modal and description logics. Currently, *sat can test the satisability of a formula in the modal logic K or in the description logic ALC. It is out of the goals of this paper to describe *sat structure, optimizations and congurable options. For a more detailed presentation, see [ 1 ] and the manual distributed with *sat. We only remark that: *sat is built on top of the SAT decider sato [ 2 ] . sato is one of the fastest among the currently available SAT-solvers, and has many congurable op...