Speaker
Dr
Ashish Sabharwal
(Cornell)
Description
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 time significantly
less than alternative approaches.
Joint work with Lukas Kroc and Bart Selman.
Joint work with Lukas Kroc and Bart Selman.
