A Subset-Matching Size-Bounded Cache for Testing Satisfiability in Modal Logics

The implementation of efficient decision procedures for modal logics is a major research problem in automated deduction. Caching the result of intermediate consistency checks has experimentally proved to be a very important technique for attaining efficiency. Current state-of-the-art systems implement 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, and (iii) if bounded, they can easily implement different policies to resolve which results have to be kept. We have implemented caching mechanisms based 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 experiment with the benchmarks proposed for the modal logic K at the “TABLEAUX Non Classical Systems Comparison (TANCS) 2000”. On the basis of the results, we conclude that *SAT performances are improved by (i) caching the results of intermediate consistency checks, (ii) using bit matrices instead of hash tables, and (iii) storing a small number of results in the bit matrices.