State of the art in the *SAT project

From the paper A. Tacchella Evaluating *SAT on TANCS2000 benchmarks a collection of tables showing the performance of *SAT with subset-matching and size-bounded caching:

• Tables and samples in the easy/medium category.
• Tables and samples in the (modalized) easy/medium category.
• Tables and samples in the medium category.
• Tables and samples in the (modalized) easy/medium category.

From the paper E. Giunchiglia, A. Tacchella A Subset-matching Size-bounded Cache for Satisfiability in Modal Logics :

• Tableaux 2000 formulae, logic K a comparison among *SAT, *SAT with subset matching bounded caching, and *SAT with hash-based caching.
• Tableaux 2000 formulae, logic K a comparison among *SAT versions featuring subset matching bounded caching with different cache bounds.

• Random formulae, logic K a comparison among *SAT, KsatC, DLP and TA using randomly generated benchmarks for the modal logic K;
• Tableaux '98 formulae, logic K a comparison among *SAT, DLP and TA using the Tableaux '98 benchmarks for the modal logic K;
• Random formulae, logic E a comparison among *SAT featuring a decision procedure for the modal logic E and *SAT+GH, DLP+GH and TA+GH, i.e. *SAT, DLP and TA exploiting a translation from the modal logic E to the modal logic K(2) (K with two agents);