From Sampling to Model Counting

Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart Selman

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.

URL: http://www.cs.cornell.edu/~sabhar/publications/sampleCountIJCAI07.pdf