@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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.},
}