Abstract
Given a formula φ, the problem of uniform sampling seeks to sample solutions of φ uniformly at random. The computational intractability of uniform sampling has led to the development of several samplers that heavily rely on 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 is close to uniform. The availability of Barbarik has the potential to spur development of sampler 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. Based on the flexibility offered by CryptoMiniSat, we design the sampler CMSGen that achieves a sweet spot of quality of distributions and runtime performance.