Leveraging belief propagation, backtrack search, and statistics for model counting

Lukas Kroc (), Ashish Sabharwal () and Bart Selman ()

Annals of Operations Research, 2011, vol. 184, issue 1, 209-231

Abstract: 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 the Belief Propagation (BP) algorithm. 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 based on these two ideas, BPCount and MiniCount, can provide very good bounds in time significantly less than alternative approaches. Copyright Springer Science+Business Media, LLC 2011

Keywords: Boolean satisfiability; SAT; Number of solutions; Model counting; BPCount; MiniCount; Lower bounds; Upper bounds (search for similar items in EconPapers)
Date: 2011
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://hdl.handle.net/10.1007/s10479-009-0680-7 (text/html)
Access to full text is restricted to subscribers.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:annopr:v:184:y:2011:i:1:p:209-231:10.1007/s10479-009-0680-7

Ordering information: This journal article can be ordered from
http://www.springer.com/journal/10479

DOI: 10.1007/s10479-009-0680-7

Access Statistics for this article

Annals of Operations Research is currently edited by Endre Boros

More articles in Annals of Operations Research from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().