From Sampling to Model Counting

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.

• Type: Conference
• Year: 2007
• Where: IJCAI
• Authors: Carla P. Gomes, Jörg Hoffmann, Ashish Sabharwal, Bart Selman
• Keywords: Approach Incorporates Information, Artificial Intelligence, Boolean Satisfiability Problems, IJCAI 2007, Solution Space