@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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.},
}