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. 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 promise the achievement of sweet-spot of the quality of distributions and runtime performance. In particular, CMSGen achieves significant runtime performance improvement over the existing samplers. The existence of CMSGen leads us to observe the need for a tester to return quantitative answers to determine the quality of underlying samplers instead of a merely quantitative answer of Accept or Reject. To this end, we design a computational hardness-based tester ScalBarbarik that provides a more nuanced analysis of the quality of a sampler.