• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Designing Samplers is Easy: The Boon of Testers.
Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel.
In Proceedings of Formal Methods in Computer-Aided Design (FMCAD), October 2021.
Given a formula F, the problem of uniform sampling seeks to sample solutions of F uniformly at random. Uniform sampling is a fundamental problem with a wide variety of applications. The computational intractability of uniform sampling has led to the development of several samplers that are heuristics and are not accompanied by theoretical analysis of their distribution. Recently, Chakraborty and Meel (2019) designed the first scalable sampling tester, Barbarik, based on a grey-box sampling technique for testing if the distribution, according to which the given sampler is sampling, is close to the uniform or far from uniform. While the theoretical analysis of Barbarik provides only unconditional soundness guarantees, the empirical evaluation of Barbarik did show its success in determining that some of the off-the-shelf samplers were far from a uniform sampler. The availability of Barbarik has the potential to spur the development of samplers and testing techniques such that developers can design sampling methods that can be accepted by Barbarik even though these samplers may not be amenable to a detailed mathematical analysis. In this paper, we present the realization of this aforementioned promise. Based on the flexibility offered by CryptoMiniSat, we design a sampler CMSGen that promises the achievement of the sweet spot of the quality of distributions and runtime performance. In particular, CMSGen achieves significant runtime performance improvement over the existing samplers. We conduct two case studies, and demonstrate that the usage of CMSGen leads to significant runtime improvements in the context of combinatorial testing and functional synthesis. A salient strength of our work is the simplicity of CMSGen, which stands in contrast to complicated algorithmic schemes developed in the past that fail to attain the desired quality of distributions with practical runtime performance.
@inproceedings{GSCM21,
title={Designing Samplers is Easy: The Boon of Testers},
author={
Golia, Priyanka and Soos, Mate and Chakraborty, Sourav and Meel, Kuldeep S.
},
booktitle=FMCAD,
year={2021},
month=oct,
bib2html_rescat={Sampling,Distribution Testing},
bib2html_dl_pdf={../Papers/fmcad21.pdf},
bib2html_pubtype={Refereed Conference},
abstract={
Given a formula F, the problem of uniform sampling seeks to sample solutions
of F uniformly at random. Uniform sampling is a fundamental problem with a
wide variety of applications. The computational intractability of uniform
sampling has led to the development of several samplers that are heuristics
and are not accompanied by theoretical analysis of their distribution.
Recently, Chakraborty and Meel (2019) designed the first scalable sampling
tester, Barbarik, based on a grey-box sampling technique for testing if the
distribution, according to which the given sampler is sampling, is close to
the uniform or far from uniform. While the theoretical analysis of Barbarik
provides only unconditional soundness guarantees, the empirical evaluation
of Barbarik did show its success in determining that some of the
off-the-shelf samplers were far from a uniform sampler.
The availability of Barbarik has the potential to spur the development of
samplers and testing techniques such that developers can design sampling
methods that can be accepted by Barbarik even though these samplers may not
be amenable to a detailed mathematical analysis. In this paper, we present
the realization of this aforementioned promise. Based on the flexibility
offered by CryptoMiniSat, we design a sampler CMSGen that promises the
achievement of the sweet spot of the quality of distributions and runtime
performance. In particular, CMSGen achieves significant runtime performance
improvement over the existing samplers. We conduct two case studies, and
demonstrate that the usage of CMSGen leads to significant runtime
improvements in the context of combinatorial testing and functional
synthesis.
A salient strength of our work is the simplicity of CMSGen, which stands in
contrast to complicated algorithmic schemes developed in the past that fail
to attain the desired quality of distributions with practical runtime
performance.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21