Vibhav Giridhar Gogate, Rina Dechter
We introduce novel algorithms for generating random solutions from a uniform distribution over the solutions of a boolean satisfiability problem. Our algorithms operate in two phases. In the first phase, we use a recently introduced SampleSearch scheme to generate biased samples while in the second phase we correct the bias by using either Sampling Importance Resampling or the Metropolis-Hastings method. Unlike state of the art algorithms, our algorithms guarantee convergence in the limit. Our empirical results demonstrate the superior performance of our new algorithms over several competing schemes.
Subjects: 15. Problem Solving; 15.2 Constraint Satisfaction
Submitted: Apr 15, 2008