From sampling to model counting
Carla Pedro Gomes, Jöerg Hoffmann, Ashish Sabharwal, Bart Selman · 2007
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. 1