Skip to content
STIMSMITH

Almost-Uniform Sampling

Concept WIKI v1 · 9/7/2026

Almost-uniform sampling is a relaxation of uniform sampling in which the probability of generating any particular element is guaranteed only to lie within a multiplicative factor (1+ε) of the uniform probability, rather than being exactly uniform. In the context of SAT witness generation, almost-uniform generators are central to Constrained Random Verification (CRV) because they preserve near-optimal bug-discovery rates while enabling scalable, hashing-based implementations such as UniGen and UniGen2.

Almost-Uniform Sampling

Definition

Given a Boolean formula $F$ in CNF and a sampling set $S$, a probabilistic witness generator $G_{au}(\cdot,\cdot,\cdot)$ is called an almost-uniform generator if, for tolerance parameter $\varepsilon > 0$ and every $y \in R_{F|S}$, it satisfies the bounds

$$\frac{1}{(1+\varepsilon),|R_{F|S}|} \le \Pr[G_{au}(F, S, \varepsilon) = y] \le \frac{(1+\varepsilon)}{|R_{F|S}|}$$

That is, the per-element sampling probability lies within a multiplicative factor $(1+\varepsilon)$ of the uniform probability $1/|R_{F|S}|$. A generator may also "fail" by returning no witness even when $R_{F|S}$ is non-empty; such failure probability must be bounded by a constant strictly less than 1.

Theoretical Context

The notion of almost-uniform sampling was introduced in the foundational work of Jerrum, Valiant, and Vazirani, who showed that almost-uniform generation of SAT witnesses can be performed in probabilistic polynomial time given access to a $\Sigma_2^P$ oracle, and that almost-uniform generation is polynomially inter-reducible with approximate model counting. Bellare, Goldreich, and Petrank subsequently improved this to a $BPP^{NP}$ algorithm. These algorithms, however, do not scale beyond a few tens of variables in practice.

A close cousin of the almost-uniform distribution is the notion of $(l,u)$-almost-independent almost-identically distributed (a.a.d.) events used in the analysis of parallel samplers: a family of events ${E_1,\dots,E_n}$ is $(l,u)$-a.a.d. if for every $i$, $l \le \Pr[E_i] \le u$ and $l \le \Pr[E_i \mid {E_1,\dots,E_n}\setminus E_i] \le u$. This is a relaxation of the i.i.d. condition that captures the weakened independence guarantees produced by samplers that pick multiple elements from a single hash-defined cell.

Role in Constrained Random Verification (CRV)

Almost-uniform sampling is the central theoretical guarantee in Constrained Random Verification. Given a bug set $B \subseteq R_{F|S}$ with fraction $f = |B|/|R_{F|S}| < 0.8$, the probability that $N$ i.i.d. uniform stimuli miss $B$ is $(1-f)^N$, which decreases exponentially in $N$ with decay rate $f$. For an almost-uniform generator with tolerance $\varepsilon$, the achievable decay rate is

$$\frac{1-\tilde{f}}{1+\varepsilon f}, \quad \text{where } \tilde{f} = \tfrac{1}{2}(1+\varepsilon)f$$

so that the relative number of samples needed (compared to a uniform generator) is $\frac{1}{(1+\tilde{f})(1+\varepsilon)}$. The constant factor in sample count is acceptable in practice because it is outweighed by a dramatic reduction in SAT-solver calls.

Hashing-Based Realizations

Modern scalable almost-uniform samplers follow the hashing paradigm pioneered by Sipser and later used by Jerrum–Valiant–Vazirani and Bellare–Goldreich–Petrank:

  1. Partition the witness space $R_{F|S}$ into small "cells" of roughly equal size using an $r$-wise independent hash family $H(n, m, r)$.
  2. Pick a random hash $h$ and a random cell index $\alpha$; enumerate a witness in $R_{F|S,h,\alpha} = R_{F|S} \cap h^{-1}(\alpha)$.

Bellare, Goldreich, and Petrank showed that with $r = n$ (full independence), uniform generation is achievable, but the algorithm does not scale. Chakraborty, Meel, and Vardi then showed that $r = 3$ suffices to obtain a scalable near-uniform generator, UniWit. Building on this, Chakraborty et al. designed UniGen, which exploits the connection between approximate counting and almost-uniform sampling and scales to hundreds of thousands of variables, at the cost of being 2–3 orders of magnitude slower than ideal in runtime.

Almost-Uniform Guarantees of UniGen2

UniGen2 produces multiple samples per hash cell, weakening strict independence but preserving near-uniform coverage:

  • Theorem 2 (single call to GenerateSamples). For a given $F$, $S$, and $\varepsilon$, let $L$ be the set of samples from a single invocation of GenerateSamples. Then for every $y \in R_{F|S}$,

$$\frac{\text{loThresh}}{(1+\varepsilon),|R_{F|S}|} \le \Pr[y \in L] \le \frac{1.02,\text{loThresh}}{(1+\varepsilon),|R_{F|S}|}$$

  • Theorem 3 (multiple parallel/sequential calls). If GenerateSamples is called $N$ times (in any parallel or sequential interleaving), the events $E_{y,i}$ that $y$ appears in the $i$-th call are $(l, u)$-a.a.d. with $l = \text{loThresh}/((1+\varepsilon),|R_{F|S}|)$ and $u = 1.02 \cdot \text{loThresh} \cdot (1+\varepsilon)/|R_{F|S}|$.

  • Theorem 4 (CRV effectiveness). UniGen2 achieves the same asymptotic failure decay rate as an almost-uniform generator — namely $(1-\tilde{f}_b)/(1+\varepsilon f)$ with $\tilde{f}_b = 1.02 \cdot \text{loThresh} \cdot \tilde{f} < 1$ — while requiring fewer expected SAT calls than UniGen. In particular, for $8.07 \le \varepsilon \le 243$ and $f \le 1/1000$, UniGen2 uses strictly fewer SAT calls than UniGen on average.

A worked numerical example from the source makes the trade-off concrete: when 1 in $10^4$ inputs triggers a bug and the target bug-discovery probability is $\tfrac{1}{2}$, an ideal uniform generator needs about $6.93 \cdot 10^3$ samples; UniGen needs about $1.17 \cdot 10^5$; UniGen2 needs about $1.20 \cdot 10^5$ at tolerance $\varepsilon = 16$. Yet UniGen2 requires only $\sim 3.38 \cdot 10^6$ expected SAT calls versus $4.35 \cdot 10^7$ for UniGen — roughly an order of magnitude fewer.

Practical Implementations and Parallelism

UniGen2 has been implemented and shown by extensive experiments to:

  • Produce sample distributions indistinguishable from those of an ideal uniform sampler,
  • Significantly outperform prior state-of-the-art algorithms on diverse benchmarks,
  • Be inherently parallelizable, with a parallel variant achieving near-linear speedup with the number of cores.

These properties make almost-uniform sampling, as realized by UniGen2, the practical workhorse for CRV in industrial hardware design flows.

Related Concepts

  • UniGen2 — A parallelizable hashing-based almost-uniform SAT witness generator that uses the almost-uniform sampling framework and is the primary modern realization of it.
  • UniGen — The predecessor of UniGen2; provides almost-uniform guarantees but with higher SAT-call cost and weaker parallelizability.
  • Uniform sampling — The stricter ideal in which every witness is generated with probability exactly $1/|R_{F|S}|$; almost-uniform sampling is the relaxation that makes scalable algorithms possible.
  • Approximate model counting — Shown by Jerrum–Valiant–Vazirani to be polynomially inter-reducible with almost-uniform generation.
  • Constrained Random Verification (CRV) — The principal industrial application domain where almost-uniform sampling is used to maximize bug-discovery probability.

LINKED ENTITIES

1 links
UniGen2 USES

CITATIONS

7 sources
7 citations
[1] An almost-uniform generator G_au guarantees 1/((1+ε)|R_{F|S}|) ≤ Pr[G_au(F,S,ε)=y] ≤ (1+ε)/|R_{F|S}| for every y in R_{F|S}, and may fail with probability bounded by a constant strictly less than 1. On Parallel Scalable Uniform SAT Witness Generation
[2] Jerrum, Valiant, and Vazirani showed that almost-uniform generation of SAT witnesses is solvable in probabilistic polynomial time with a Σ_2^P oracle and is polynomially inter-reducible with approximate model counting; Bellare, Goldreich, and Petrank gave a BPP^NP algorithm but it fails to scale beyond a few tens of variables. On Parallel Scalable Uniform SAT Witness Generation
[3] UniGen2's single GenerateSamples call yields per-element bounds loThresh/((1+ε)|R_{F|S}|) ≤ Pr[y∈L] ≤ 1.02·loThresh/((1+ε)|R_{F|S}|) (Theorem 2). On Parallel Scalable Uniform SAT Witness Generation
[4] Across N parallel/sequential GenerateSamples invocations, the per-call events are (l,u)-a.a.d. with l = loThresh/((1+ε)|R_{F|S}|) and u = 1.02·loThresh·(1+ε)/|R_{F|S}| (Theorem 3). On Parallel Scalable Uniform SAT Witness Generation
[5] In the CRV setting, almost-uniform generators achieve failure decay rate (1−f̃)/(1+εf) and require (1+ε)(1+f̃) relative samples compared to a uniform generator, while drastically reducing SAT-solver calls (Theorem 4). On Parallel Scalable Uniform SAT Witness Generation
[6] UniGen2 is inherently parallelizable, scales near-linearly with cores, and produces sample distributions indistinguishable from those of an ideal uniform sampler while outperforming prior state-of-the-art algorithms. On Parallel Scalable Uniform SAT Witness Generation
[7] Hashing-based samplers partition the witness space into roughly equal cells using r-wise independent hash families; r=n suffices for uniform generation (Bellare et al.) and r=3 underlies the scalable UniWit/UniGen line. On Parallel Scalable Uniform SAT Witness Generation