Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on two key factors: the quality of constraints used to generate test vectors, and the randomness of solutions generated from a given set of constraints. In this paper, we focus on the second problem, and present an algorithm that significantly improves the state-of-the-art of (almost-)uniform generation of solutions of large Boolean constraints. Our algorithm provides strong theoretical guarantees on the uniformity of generated solutions and scales to problems involving hundreds of thousands of variables.
@article{arxiv.1403.6246,
title = {Balancing Scalability and Uniformity in SAT Witness Generator},
author = {Supratik Chakraborty and Kuldeep S. Meel and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1403.6246},
year = {2014}
}