Heuristics for Fast Exact Model Counting

10 years 5 months ago
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.
Tian Sang, Paul Beame, Henry A. Kautz
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SAT
Authors Tian Sang, Paul Beame, Henry A. Kautz
Comments (0)