00

UniGen

Tool ☆ WATCH ⎘ SHARE

First seen 7/17/2026

Last seen 7/26/2026

Evidence 22 chunks

01

NEIGHBORHOOD

12 nodes · 18 edges

graph · UniGen · depth=1

02

RELATIONSHIPS

28 connections

Independent Support uses → 100% 5e evidence

UniGen uses an independent support as sampling variables to reduce XOR clause size and improve scalability.

UniWit compares with → 100% 5e evidence

UniGen is explicitly compared against UniWit in terms of theoretical guarantees and runtime performance.

Approximate Model Counting uses → 100% 4e evidence

UniGen invokes an approximate model counter to estimate |RF| for choosing the hash parameter m.

r-wise Independent Hash Functions uses → 100% 4e evidence

UniGen uses 3-wise independent hash functions from the XOR family to randomly partition witnesses.

constrained random verification ← uses 95% 2e evidence

UniGen is intended to be used in constrained-random verification for generating test vectors.

Uniform Generation of SAT Witnesses implements → 100% 2e evidence

UniGen is specifically designed for uniform generation of SAT witnesses.

uniform SAT witness generation implements → 99% 2e evidence

UniGen is designed as an algorithm for uniform generation of SAT witnesses with strong guarantees.

Almost-Uniform Generator implements → 100% 2e evidence

UniGen provides strong two-sided guarantees of almost-uniformity.

XOR-based Hash Partitioning uses → 100% 2e evidence

UniGen uses XOR-based hash partitioning via the family Hxor to partition the solution space.

Boolean CNF Formula uses → 100% 2e evidence

UniGen takes a Boolean CNF formula as its primary input.

Uniform Generation of SAT Witnesses evaluates → 90% 2e evidence

The paper evaluates UniGen's performance in generating SAT witnesses uniformly.

almost-uniform generation implements → 99% 2e evidence

UniGen is described as the first algorithm to provide strong two-sided guarantees of almost-uniformity.

XOR clauses uses → 97% 2e evidence

UniGen constructs XOR clauses over the independent support to partition the witness space.

CryptoMiniSAT uses → 100% 2e evidence

UniGen's BSAT procedure is implemented using CryptoMiniSAT, a SAT solver with XOR clause handling.

ApproxMC uses → 100% 2e evidence

UniGen's ApproxModelCounter is implemented using ApproxMC.

PAWS ← compares with 97% 2e evidence

UniGen provides stronger theoretical guarantees than PAWS and scales further.

ISCAS89 circuits evaluates → 92% 1e evidence

UniGen was evaluated on constraints from ISCAS89 circuits.

Hashing-Based Sampling implements → 100% 1e evidence

UniGen is described as falling in the category of hashing-based almost-uniform generators.

blocking clauses uses → 95% 1e evidence

UniGen's BSAT implementation uses blocking clauses restricted to the independent support variables.

UniGen Paper (DAC 2014) ← introduces 100% 1e evidence

The paper proposes and introduces the UniGen algorithm for almost-uniform generation of SAT witnesses.

sharpSAT uses → 88% 1e evidence

sharpSAT is used as an exact model counter in a uniform sampler US that is compared against UniGen.

sampling variables uses → 96% 1e evidence

UniGen accepts sampling variables as input to restrict hash function scope.

Kuldeep S. Meel authored by → 100% 1e evidence

Kuldeep S. Meel is an author of UniGen.

Moshe Y. Vardi authored by → 100% 1e evidence

Moshe Y. Vardi is an author of UniGen.

Supratik Chakraborty authored by → 100% 1e evidence

Supratik Chakraborty is an author of UniGen.

bounded model checking evaluates → 90% 1e evidence

UniGen was experimentally evaluated on benchmarks from bounded model checking.

SMTLib benchmarks evaluates → 92% 1e evidence

UniGen was tested on bit-blasted SMTLib benchmarks.

hashing-based sampling implements → 99% 1e evidence

UniGen is a hashing-based almost-uniform generator.