A subset-matching size-bounded cache for testing satisfiability in modal logics

The implementation of efficient decision procedures for modal logics is a m ajor research problem in automated deduction. Caching the result of interme diate consistency checks has experimentally proved to be a very important t echnique for attaining efficiency. Current state-of-the-art systems impleme nt caching mechanisms based on hash tables. In this paper we present a data type - that we call "bit matrix" - for caching the (in)consistency of sets of formulas. Bit matrices have three distinguishing features: (i) they can be queried for subsets and supersets, (ii) they can be bounded in size, an d (iii) if bounded, they can easily implement different policies to resolve which results have to be kept. We have implemented caching mechanisms base d on bit matrices and hash tables in *SAT. In *SAT, the bit matrix cache is bounded, and keeps the latest obtained (in)consistency results. We experim ent with the benchmarks proposed for the modal logic K at the "TABLEAUX Non Classical Systems Comparison (TANCS) 2000". On the basis of the results, w e conclude that *SAT performances are improved by (i) caching the results o f intermediate consistency checks, (ii) using bit matrices instead of hash tables, and (iii) storing a small number of results in the bit matrices.