Enhanced Caching for #SAT Solving
Jean-Marie Lagniez, Pierre Marquis · HAL (Le Centre pour la Communication Scientifique Directe) · 2020
We present and evaluate an improved caching scheme and an improved cache cleaning strategy that can be exploited for model counting of propositional formulae in conjunctive normal form (CNF). The caching scheme consists in storing for each entry (a CNF formula forming a connected component given a current variable assignment, together with its model count) the corresponding set of variables and the corresponding set of clauses, except those clauses of the CNF formula that are satisfied or not shortened when conditioned by the assignment. The cache cleaning strategy is based not only on the ages of the entries, but also on the proportion of entries of the same size that led to positive hits. We also report the results of an empirical evaluation showing the benefits that are provided by these caching scheme and cache cleaning strategy when implemented in a #SAT solver.