Heuristics for Fast Exact Model Counting

An important extension of satisfiability testing is model-counting, a task that corresponds to problems such as probabilistic reasoning and computing the permanent of a Boolean matrix. We recently introduced Cachet, an exact model-counting algorithm that combines formula caching, clause learning, and component analysis. This paper reports on experiments with various techniques for improving the performance of Cachet, including component-selection strategies, variable-selection branching heuristics, randomization, backtracking schemes, and cross-component implications. The result of this work is a highlytuned version of Cachet, the first (and currently, only) system able to exactly determine the marginal probabilities of variables in random 3-SAT formulas with 150+ variables. We use this to discover an interesting property of random formulas that does not seem to have been previously observed.

• Type: Conference
• Year: 2005
• Where: SAT
• Authors: Tian Sang, Paul Beame, Henry A. Kautz
• Keywords: Exact Model-counting Algorithm, Random 3-SAT Formulas, SAT 2005, Variable-selection Branching Heuristics