Vibhav Giridhar Gogate, Rina Dechter
We present a new estimator for counting the number of solutions of a Boolean satisfiability problem as a part of an importance sampling framework. The estimator uses the recently introduced SampleSearch scheme that is designed to overcome the rejection problem associated with distributions having a substantial amount of determinism. We show here that the sampling distribution of SampleSearch can be characterized as the backtrack free distribution and propose several schemes for its computation. This allows integrating SampleSearch into the importance sampling framework for approximating the number of solutions and also allows using SampleSearch for computing a lower bound measure on the number of solutions. Our empirical evaluation demonstrates the superiority of our new approximate counting schemes against recent competing approaches.
Subjects: 15. Problem Solving; 15.2 Constraint Satisfaction
Submitted: Apr 24, 2007