# Balancing Scalability and Uniformity in SAT Witness Generator

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Mar 2014.

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

- [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)
- [Denoising Diffusion for Sampling SAT Solutions](https://mlsanity.com/paper/2212.00121/) (2022)
- [Generating from Discrete Distributions Using Diffusions: Insights from Random Constraint Satisfaction Problems](https://mlsanity.com/paper/2603.20589/) (2026)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)

## Abstract (arXiv)

Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on two key factors: the quality of constraints used to generate test vectors, and the randomness of solutions generated from a given set of constraints. In this paper, we focus on the second problem, and present an algorithm that significantly improves the state-of-the-art of (almost-)uniform generation of solutions of large Boolean constraints. Our algorithm provides strong theoretical guarantees on the uniformity of generated solutions and scales to problems involving hundreds of thousands of variables.