We introduce a new technique for counting models of Boolean satisfiability problems. Our approach incorporates information obtained from sampling the solution space. Unlike previous approaches, our method does not require uniform or near-uniform samples. It instead converts local search sampling without any guarantees into very good bounds on the model count with guarantees. We give a formal analysis and provide experimental results showing the effectiveness of our approach.

Authors

• Carla P. Gomes Department of Computer Science, Cornell University, USA
• Joerg Hoffmann
• Ashish Sabharwal
• Bart Selman

Keywords

No keywords are indexed for this paper.