Sciweavers

Share
CPAIOR
2008
Springer

Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting

9 years 8 months ago
Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting
We consider the problem of estimating the model count (number of solutions) of Boolean formulas, and present two techniques that compute estimates of these counts, as well as either lower or upper bounds with different trade-offs between efficiency, bound quality, and correctness guarantee. For lower bounds, we use a recent framework for probabilistic correctness guarantees, and exploit message passing techniques for marginal probability estimation, namely, variations of Belief Propagation (BP). Our results suggest that BP provides useful information even on structured loopy formulas. For upper bounds, we perform multiple runs of the MiniSat SAT solver with a minor modification, and obtain statistical bounds on the model count based on the observation that the distribution of a certain quantity of interest is often very close to the normal distribution. Our experiments demonstrate that our model counters, BPCount and MiniCount, based on these two ideas can provide very good bounds in ...
Lukas Kroc, Ashish Sabharwal, Bart Selman
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2008
Where CPAIOR
Authors Lukas Kroc, Ashish Sabharwal, Bart Selman
Comments (0)
books