UniGen
ToolFirst seen 7/17/2026
Last seen 7/17/2026
Evidence 10 chunks
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
17 connectionsUniGen is directly compared with UniWit in experiments showing superior performance.
UniGen exploits the concept of independent support to reduce the size of XOR clauses and scale to larger problems.
UniGen uses XOR-based hash partitioning via the family Hxor to partition the solution space.
The paper evaluates UniGen's performance in generating SAT witnesses uniformly.
UniGen provides strong two-sided guarantees of almost-uniformity.
UniGen invokes an approximate model counter to estimate |RF| and determine the partitioning parameter m.
UniGen uses 3-wise independent linear hash functions from the family Hxor for partitioning.
UniGen takes a Boolean CNF formula as its primary input.
UniGen is intended to be used in constrained-random verification for generating test vectors.
UniGen is specifically designed for uniform generation of SAT witnesses.
UniGen is described as falling in the category of hashing-based almost-uniform generators.
The paper proposes and introduces the UniGen algorithm for almost-uniform generation of SAT witnesses.
UniGen's ApproxModelCounter subroutine is implemented using ApproxMC.
UniGen's BSAT subroutine is implemented using CryptoMiniSAT.
Supratik Chakraborty is an author of UniGen.
Kuldeep S. Meel is an author of UniGen.
Moshe Y. Vardi is an author of UniGen.