On Parallel Scalable Uniform SAT Witness Generation

Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. On Parallel Scalable Uniform SAT Witness Generation. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 304–319, April 2015.

Download

[pdf] 

Abstract

Constrained-random verification (CRV) is widely used in industry for validating hardware designs. The effectiveness of CRV depends on the uniformity of test stimuli generated from a given set of constraints. Most existing techniques sacrifice either uniformity or scalability when generating stimuli. While recent work based on random hash functions has shown that it is possible to generate almost uniform stimuli from constraints with 100,000+ variables, the performance still falls short of today's industrial requirements. In this paper, we focus on pushing the performance frontier of uniform stimulus generation further. We present a random hashing-based, easily parallelizable algorithm, UniGen2, for sampling solutions of propositional constraints. UniGen2 provides strong and relevant theoretical guarantees in the context of CRV, while also offering significantly improved performance compared to existing almost-uniform generators. Experiments on a diverse set of benchmarks show that UniGen2 achieves an average speedup of about $20\times$ over a state-of-the-art sampling algorithm, even when running on a single core. Moreover, experiments with multiple cores show that UniGen2 achieves a near-linear speedup in the number of cores, thereby boosting performance even further.

BibTeX

@inproceedings{chakraborty-tacas15,
  author    = {Supratik Chakraborty and Daniel J. Fremont and Kuldeep S. Meel and Sanjit A. Seshia and Moshe Y. Vardi},
  title     = {On Parallel Scalable Uniform SAT Witness Generation},
 booktitle = {Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
 month = "April",
 year = {2015},
 pages = {304--319},
 abstract = {Constrained-random verification (CRV) is widely used in industry 
for validating hardware designs.  The effectiveness of CRV depends on 
the uniformity of test stimuli generated from a given set of 
constraints.  Most existing techniques sacrifice either uniformity or 
scalability when generating stimuli.  While recent work based on 
random hash functions has shown that it is possible to generate almost 
uniform stimuli from constraints with 100,000+ variables, the 
performance still falls short of today's industrial requirements.  In 
this paper, we focus on pushing the performance frontier of uniform 
stimulus generation further.  We present a random hashing-based, easily 
parallelizable algorithm, UniGen2, for sampling solutions of 
propositional constraints.  UniGen2 provides strong and relevant 
theoretical guarantees in the context of CRV, while also offering 
significantly improved performance compared to existing almost-uniform 
generators. Experiments on a diverse set of benchmarks show that 
UniGen2 achieves an average speedup of about $20\times$ over a 
state-of-the-art sampling algorithm, even when running on a single 
core.  Moreover, experiments with multiple cores show that UniGen2 achieves a 
near-linear speedup in the number of cores, thereby boosting 
performance even further.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Sun Jun 21, 2015 12:56:34