# A Scalable and Nearly Uniform Generator of SAT Witnesses

arXiv: https://arxiv.org/abs/1304.1584 · HTML: https://mlsanity.com/paper/1304.1584/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Apr 2013.

## Built on by (most cited first, 10 of 10)

- [Efficient Exploration of the Rashomon Set of Rule Set Models](https://mlsanity.com/paper/2406.03059/) (2024)
- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [Lifted Algorithms for Symmetric Weighted First-Order Model Sampling](https://mlsanity.com/paper/2308.08828/) (2023)
- [On Exact Sampling in the Two-Variable Fragment of First-Order Logic](https://mlsanity.com/paper/2302.02730/) (2023)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)
- [CCDD: A Tractable Representation for Model Counting and Uniform Sampling](https://mlsanity.com/paper/2202.10025/) (2022)
- [Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees](https://mlsanity.com/paper/2309.08883/) (2023)
- [Learning Markov Random Fields for Combinatorial Structures via Sampling through Lov'asz Local Lemma](https://mlsanity.com/paper/2212.00296/) (2022)
- [Fast Rerandomization for Balancing Covariates in Randomized Experiments: A Metropolis-Hastings Framework](https://mlsanity.com/paper/2602.07613/) (2026)
- [Enhancing Query Efficiency for d-DNNF Representations Through Preprocessing](https://mlsanity.com/paper/2607.11492/) (2026)

## Abstract (arXiv)

Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the functional verification landscape. A dominant paradigm in simulation-based verification is directed random testing, where a model of the system is simulated with a set of random test stimuli that are uniformly or near-uniformly distributed over the space of all stimuli satisfying a given set of constraints. Uniform or near-uniform generation of solutions for large constraint sets is therefore a problem of theoretical and practical interest. For Boolean constraints, prior work offered heuristic approaches with no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. We offer here a new approach with theoretical performance guarantees and demonstrate its practical utility on large constraint sets.