On Parallel Scalable Uniform SAT Witness Generation
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit Seshia, Moshe Y. Vardi

Citation
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit Seshia, Moshe Y. Vardi. "On Parallel Scalable Uniform SAT Witness Generation". 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, Christel Baier, Cesare Tinelli (eds.), TACAS, 302-319, April, 2015.

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 20x 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.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel,
  Sanjit Seshia, Moshe Y. Vardi. <a
  href="http://www.terraswarm.org/pubs/483.html"
  >On Parallel Scalable Uniform SAT Witness
  Generation</a>, 21st International Conference, TACAS
  2015, Held as Part of the European Joint Conferences on
  Theory and Practice of Software, ETAPS 2015, London, UK,
  April 11-18, 2015, Proceedings, Christel Baier, Cesare
  Tinelli (eds.), TACAS, 302-319, April, 2015.

• Plain text

  Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel,
  Sanjit Seshia, Moshe Y. Vardi. "On Parallel Scalable
  Uniform SAT Witness Generation". 21st International
  Conference, TACAS 2015, Held as Part of the European Joint
  Conferences on Theory and Practice of Software, ETAPS 2015,
  London, UK, April 11-18, 2015, Proceedings, Christel Baier,
  Cesare Tinelli (eds.), TACAS, 302-319, April, 2015.

• BibTeX

  @inproceedings{ChakrabortyFremontMeelSeshiaVardi15_OnParallelScalableUniformSATWitnessGeneration,
      author = {Supratik Chakraborty and Daniel J. Fremont and
                Kuldeep S. Meel and Sanjit Seshia and Moshe Y.
                Vardi},
      title = {On Parallel Scalable Uniform SAT Witness Generation},
      booktitle = {21st International Conference, TACAS 2015, Held as
                Part of the European Joint Conferences on Theory
                and Practice of Software, ETAPS 2015, London, UK,
                April 11-18, 2015, Proceedings},
      editor = {Christel Baier, Cesare Tinelli},
      organization = {TACAS},
      pages = {302-319},
      month = {April},
      year = {2015},
      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
                20x 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.},
      URL = {http://terraswarm.org/pubs/483.html}
  }
  

Posted by Daniel J. Fremont on 2 Feb 2015.
Groups: tools