Almost-Uniform Sampling

Concept

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.

First seen 9/7/2026

Last seen 9/7/2026

Evidence 4 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

2 nodes · 1 edges

graph · Almost-Uniform Sampling · depth=1

RELATIONSHIPS

1 connections

UniGen2 ← uses 95% 2e

UniGen2 provides guarantees similar to an almost-uniform generator.

LINKED ENTITIES

1 links

UniGen2 USES Extracted graph relationship

CITATIONS

7 sources

7 citations — click to expand

[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