Balancing Scalability and Uniformity in SAT Witness Generator ∗

    Supratik Chakraborty Kuldeep S. Meel, Moshe Y. Vardi
Indian Institute of Technology, Bombay Rice University
    supratik@cse.iitb.ac.in kuldeep@rice.edu,vardi@cs.rice.edu

ABSTRACT In recent years, constrained-random simulation (also called Constrained-random simulation is the predominant approach constrained-random verification, or CRV) [21] has emerged used in the industry for functional verification of complex as a practical approach to address the problem of simulat- digital designs. The effectiveness of this approach depends ing designs with “random enough” input patterns. In CRV, on two key factors: the quality of constraints used to gener- the verification engineer declaratively specifies a set of con- ate test vectors, and the randomness of solutions generated straints on the values of circuit inputs. Typically, these con- from a given set of constraints. In this paper, we focus on the straints are obtained from usage requirements, environmen- second problem, and present an algorithm that significantly tal constraints, constraints on operating conditions and the improves the state-of-the-art of (almost-)uniform generation like. A constraint solver is then used to generate random val- of solutions of large Boolean constraints. Our algorithm pro- ues for the circuit inputs satisfying the constraints. Since the vides strong theoretical guarantees on the uniformity of gen- distribution of errors in the design’s behavior space is not erated solutions and scales to problems involving hundreds known a priori, every solution to the set of constraints is as of thousands of variables. likely to discover a bug as any other solution. It is therefore important to sample the space of all solutions uniformly or

1. INTRODUCTION almost-uniformly (defined formally below) at random. Un- fortunately, guaranteeing uniformity poses significant tech-

Functional verification constitutes one of the most chal- nical challenges when scaling to large problem sizes. This has lenging and time-consuming steps in the design of modern been repeatedly noted in the literature (see, for example, [8, digital systems. The primary objective of functional veri- 22, 16]) and also confirmed by industry practitioners¹. The fication is to expose design bugs early in the design cy- difficulties of generating solutions with guarantees of unifor- cle. Among various techniques available for this purpose, mity have even prompted researchers to propose alternative those based on simulation overwhelmingly dominate indus- techniques for generating input patterns [8, 22]. This paper trial practice. In a typical simulation-based functional ver- takes a step towards remedying this situation. Specifically, ification exercise, a gate-level or RTL model of the circuit we describe an algorithm for generating solutions to a set of is simulated for a large number of cycles with specific in- Boolean constraints, with stronger guarantees on uniformity put patterns. The values at observable outputs, as computed and with higher scalability in practice than that achieved by the simulator, are then compared against their expected earlier. values, and any discrepancy is flagged as manifestaton of Since constraints that arise in CRV of digital circuits are a bug. The state of simulation technology today is mature encodable as Boolean formulae, we focus on uniform gener- enough to allow simulation of large designs within reason- ation of solutions of Boolean formulae. Henceforth, we call able time using modest computational resources. Generating such solutions SAT witnesses. Besides its usefulness in CRV input patterns that exercise diverse corners of the design’s and in other applications [2, 23], uniform generation of SAT behavior space, however, remains a challenging problem [4]. witnesses has had strong theoretical interest as well [14]. ∗This work was supported in part by NSF grants CNS 1049862 and Most prior approaches to solving this problem belong to CCF-1139011, by NSF Expeditions in Computing project ”ExCAPE: one of two categories: those that focus on strong guaran- Expeditions in Computer Augmented Program Engineering”, by BSF tees of uniformity but scale poorly in practice (examples be- grant 9800096, by gift from Intel, by a grant from Board of Research ing [27, 3, 14]), and those that provide practical heuristics in Nuclear Sciences, India, and by the Shared University Grid at Rice to scale to large problem instances with weak or no guar- funded by NSF under Grant EIA-0216467, and a partnership between Rice University, Sun Microsystems, and Sigma Solutions, Inc. antees of uniformity (examples being [7, 16, 25])). In [5], Permission to make digital or hard copies of all or part of this work for per- Chakraborty, Meel and Vardi attempted to bridge these ex- sonal or classroom use is granted without fee provided that copies are not tremes through an algorithm called UniWit. More recently, made or distributed for profit or commercial advantage and that copies bear Ermon, Gomes, Sabharwal and Selman [9] proposed an algo- this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstract- rithm called PAWS for sampling witnesses from discrete dis- ing with credit is permitted. To copy otherwise, or republish, to post on tributions over large dimensions. While PAWS is designed servers or to redistribute to lists, requires prior specific permission and/or a to work with any discrete distribution specified through a fee. Request permissions from Permissions@acm.org. graphical model, for purposes of this paper, we focus only DAC ’14, June 01-05 2014, San Francisco, CA, USA Copyright is held by the owner/author(s). Publication rights licensed to on distributions that assign equal weight to every assign- ACM. ACM 978-1-4503-2370-5/14/06$15.00. 1Private communication: R. Kurshan http://dx.doi.org/10.1145/2593069.2593097.

ment. For such distributions, both PAWS and UniWit repre- counter ApproxMC(·, ·, ·) relaxes this requirement to some sent alternative (albeit related) approaches to solve the same extent. Given a CNF formula F , a tolerance ε > 0 and a con- problem – that of uniform generation of SAT witnesses. Un- fidence 1−δ ∈ (0, 1], and approximate model counter ensures fortunately, both algorithms suffer from inherent limitations that Pr[ |RF | ≤ ApproxMC(F, ε, 1 − δ) ≤ (1 + ε)|R |] ≥ 1 − δ. that make it difficult to scale them to Boolean constraints 1+ε F with tens of thousands of variables and beyond. In addition, dentA special class of hash functions, called r-wise indepen- the guarantees provided by these algorithms (in the context and rhash functions, play a crucial role in our work. Let n, m of uniform generation of SAT witnesses) are weaker than ily of be positive integers, and letr H(n, m, r) denote a fam- what one would desire in practice. to {0, 1}-wise independent hash functions mapping {0, 1}ⁿ R m. We use h ← In this paper, we propose an algorithm called UniGen that − H(n, m, r) to denote the prob- addresses some of the deficiencies of UniWit and PAWS. This ability space obtained by choosing a hash function h uni- enables us to improve both the theoretical guarantees and formly at random from H(n, m, r). The property of r-wise independence guarantees that for all α₁, . . . α practical performance vis-a-vis earlier algorithms in the con- and for all distinct] y₁, . . . yᵣ ∈ {0, 1}ⁿ, Pr [∧ʳ r ∈ {0, 1}ᵐ text of uniform generation of SAT witnesses. UniGen is the R i=1 h(yi) = αi − H(n, m, r) = 2−mr. For every α ∈ {0, 1}ᵐ and first algorithm to provide strong two-sided guarantees of : h ← almost-uniformity, while scaling to problems involving hun- h ∈ H(n, m, r), let h−1(α) denote the set {y ∈ {0, 1}ⁿ | dreds of thousands of variables. We also improve upon the h(y) = α}. Given RF ⊆ {0, 1}ⁿ and h ∈ H(n, m, r), we use success probability of the earlier algorithms significantly, RF,h,α to denote the set RF ∩ h−1(α). If we keep h fixed and both in theory and as evidenced by our experiments. let α range over {0, 1}ᵐ, the sets RF,h,α form a partition of RF . For every m ∈ {1, . . . |S| − 1}, the mᵗʰ prefix-slice 2. NOTATION AND PRELIMINARIES of h, denoted h(m), is a map from {0, 1}|S| to {0, 1}ᵐ, such Let F be a Boolean formula in conjunctive normal form thati h(m)(y)[i] = h(y)[i], for all y ∈ {0, 1}|S| and for all (CNF), and let X be the set of variables appearing in F . The α∈ {1, . . . m}. Similarly, the mᵗʰ prefix-slice of α, denoted set X is called the support of F . A satisfying assignment or all(m)i , is an element of {0, 1}ᵐ such that α(m)[i] = α[i] for witness of F is an assignment of truth values to variables in ∈ {1, . . . m}. its support such that F evaluates to true. We denote the set of all witnesses of F as RF . Let D ⊆ X be a subset of the 3. RELATED WORK support such that there are no two satisfying assignments of Marrying scalability with strong guarantees of uniformity F that differ only in the truth values of variables in D. In has been the holy grail of algorithms that sample from solu- other words, in every satisfying assignment of F , the truth tions of constraint systems. The literature bears testimony values of variables in X \ D uniquely determine the truth to the significant tension between these objectives when de- value of every variable in D. The set D is called a dependent signing random generators of SAT witnesses. Earlier work support of F , and X \ D is called an independent support in this area either provide strong theoretical guarantees at of F . Note that there may be more than one independent the cost of scalability, or remedy the scalability problem at supports of F . For example, (a ∨ ¬b) ∧ (¬a ∨ b) has three the cost of guarantees of uniformity. More recently, however, independent supports: {a}, {b} and {a, b}. Clearly, if I is there have been efforts to bridge these two extremes. an independent support of F , so is every superset of I. For Bellare, Goldreich and Petrank [3] showed that a provably notational convenience, whenever the formula F is clear from uniform generator of SAT witnesses can be designed in the- the context, we omit mentioning it. ory to run in probabilistic polynomial time relative to an NP We use Pr [X : P ] to denote the probability of outcome X oracle. Unfortunately, it was shown in [5] that this algorithm when sampling from a probability space P . For notational does not scale beyond formulae with few tens of variables in clarity, we omit P when it is clear from the context. The practice. Weighted binary decision diagrams (BDD) have expected value of the outcome X is denoted E [X]. Given a been used in [27] to sample uniformly from SAT witnesses. Boolean formula F , a probabilistic generator of witnesses of However, BDD-based techniques are known to suffer from F is a probabilistic algorithm that generates a random wit- scalability problems [16]. Adapted BDD-based techniques ness in RF . A uniform generator G u(·) is a probabilistic gen- with improved performance were proposed in [18]; however, erator that guaranteesy Pr [G u(F ) = y] = 1/|RF |, for every the scalability was achieved at the cost of guarantees of uni- ∈ RF . An almost-uniform generator G au(·, ·) ensures that formity. Random seeding of DPLL SAT solvers [20] has been for every y ∈ RF , we have (1+ε)|R¹ F | ≤ Pr [G au(F, ε) = y] ≤ shown to offer performance, although the generated distri- 1+ε , where ε > 0 is the specified tolerance. A near-uniform |RF | butions of witnesses can be highly skewed [16]. generator G nu(·) further relaxes the guarantee of unifor- Markov Chain Monte Carlo methods (also called MCMC mity, and ensures that Pr [G nu(F ) = y] ≥ c/|RF | for a con- methods) [16, 26] are widely considered to be a practical way stant c, where 0 < c ≤ 1. Probabilistic generators are al- to sample from a distribution of solutions. Several MCMC al- lowed to occasionally “fail” in the sense that no witness may gorithms, such as those based on simulated annealing, Metropolis- be returned even if RF is non-empty. The failure proba- Hastings algorithm and the like, have been studied exten- bility for such generators must be bounded by a constant sively in the literature [15, 19]. While MCMC methods guar- strictly less than 1. The algorithm presented in this pa- antee eventual convergence to a target distribution under per falls in the category of almost-uniform generators. An mild requirements, convergence is often impractically slow in idea closely related to that of almost-uniform generation, practice. The work of [26, 16] proposed several such adapta- and used in a key manner in our algorithm, is approxi- tions for MCMC-based sampling in the context of constrained- mate model counting. Given a CNF formula F , an exact random verification. Unfortunately, most of these adapta- model counter returns the size of RF . An approximate model tions are heuristic in nature, and do not preserve theoret-

ical guarantees of uniformity. constraints, thereby increas- Given a CNF formula F , we use a family of 3-independent ing constraint-solving time. Sampling techniques based on hash functions to randomly partition the set, RF , of wit- interval-propagation and belief networks have been proposed nesses of F . Let h : {0, 1}ⁿ → {0, 1}ᵐ be a hash function in in [7, 10, 13]. The simplicity of these approaches lend scala- the family, and let y be a vector in {0, 1}ⁿ. Let h(y)[i] de- bility to the techniques, but the generated distributions can note the iᵗʰ component of the vector obtained by applying deviate significantly from the uniform distribution, as shown h to y. The family of hash functions of interest is defined as in [17]. {h(y) | h(y)[i] = ai,0 ⊕ (⊕ⁿ a · y[k]), a ∈ {0, 1}, ≤ Sampling techniques based on hashing were originally pi- i ≤ m,0 ≤ j ≤ n}, where ⊕ᵏ=1 i,k i,j 1 denotes the xor operation. By oneered by Sipser [24], and have been used subsequently by choosing values of ai,j randomly and independently, we can several researchers [3, 11, 5]. The core idea in hashing-based effectively choose a random hash function from the family. It sampling is to use r-wise independent hash functions (for has been shown in [11] that this family of hash functions is a suitable value of r) to randomly partition the space of 3-independent. Following notation introduced in Section 2, witnesses into “small cells” of roughly equal size, and then we call this family Hₓₒᵣ(n, m, 3). randomly pick a solution from a randomly chosen cell. The While Hₓₒᵣ(n, m, 3) was used earlier in XORSample′, PAWS, algorithm of Bellare et al. referred to above uses this idea and (in a variant of) UniWit, there is a fundamental differ- with n-wise independent algebraic hash functions (where n ence in the way we use it in UniGen. Let X = {x₁, x₂, . . . x|X|} denotes the size of the support of F ). As noted above, their be the set of variables of F . Given m > 0, the algorithms algorithm scales very poorly in practice. Gomes, Sabhar- XORSample′, PAWS and UniWit partition RF by randomly wal and Selman used 3-wise independent linear hash func- choosing h ∈ Hₓₒᵣ(|X|, m, 3) and∧α ∈ {(0, 1}ᵐ, and by seek- ) tions in [11] to design XORSample′, a near-uniform gener- ing witnesses of F conjoined with m h(x , . . . x i ↔ [ ] ator of SAT witnesses. Nevertheless, to realize the guar- By choosing a random ( 1 |Xi=1|) ∈ Hₓₒᵣ¹ (|X |X|)[ ] α i . h x , . . . x |, m, 3), the antee of near-uniformity, their algorithm requires the user set of all assignments to variables in X (regardless of whether to provide difficult-to-estimate input parameters. Although they are witnesses of F ) is partitioned randomly. This, in XORSample′ has been shown to scale to constraints involv- turn, ensures that the set of satisfying assignments of F is ing a few thousand variables, Gomes et al. acknowledge the also partitioned randomly. Each conjunctive constraint of difficulty of scaling their algorithm to much larger problem the form (h(x₁ . . . x|X|)[i] ↔ α[i]) is an xor of a subset of sizes without sacrificing theoretical guarantees [11]. variables of X and α[i], and is called an xor-clause. Ob- Recently, Chakraborty, Meel and Vardi [5] proposed a new serve that the expected number of variables in each such hashing-based SAT witness generator, called UniWit, that xor-clause is approximately |X|/2. It is well-known (see, for represents a small but significant step towards marrying the example [12]) that the difficulty of checking satisfiability of conflicting goals of scalability and guarantees of uniformity. a CNF formula with xor-clauses grows significantly with the Like XORSample′, the UniWit algorithm uses 3-wise indepen- number of variables per xor-clause. It is therefore extremely dent linear hashing functions. Unlike XORSample′, however, difficult to scale XORSample′, PAWS or UniWit to problems the guarantee of near-uniformity of witnesses generated by involving hundreds of thousands of variables. In [5], an alter- UniWit does not depend on difficult-to-estimate input pa- native family of linear hash functions is proposed to be used rameters. In [5], UniWit has been shown to scale to formulas with UniWit. Unfortunately, this also uses |X|/2 variables with several thousand variables. In addition, Chakraborty per xor-clause on average, and suffers from the same prob- et al proposed a heuristic called “leap-frogging” that allows lem. In [12], a variant of Hₓₒᵣ(|X|, m, 3) is used, wherein UniWit to scale even further – to tens of thousands of vari- each variable in X is chosen to be in an xor-clause with a ables [5]. Unfortunately, the guarantees of near-uniformity small probability q (< 0.5). This mitigates the performace can no longer be established for UniWit with “leap-frogging”. bottleneck significantly, but theoretical guarantees of (near- More recently, Ermon et al. [9] proposed a hashing-based )uniformity are lost. algorithm called PAWS for sampling from a distribution de- We address the above problem in UniGen by making two fined over a discrete set using a graphical model. While the important observations: (i) an independent support I of F algorithm presented in this paper has some similarities with is often far smaller (sometimes by a few orders of magni- PAWS, there are significant differences as well. Specifically, tude) than X, and (ii) since the value of every variable in our algorithm provides much stronger theoretical guaran- X \ I in a satisfying assignment of F is uniquely determined tees vis-a-vis those offered by PAWS in the context of uni- by the values of variables in I, the set RF can be randomly form generation of SAT witness. In addition, our algorithm partitioned by randomly partitioning its projection on I. scales to hundreds of thousands of variables while preserv- This motivates us to design an almost-uniform generator ing the theoretical guarantees. PAWS faces the same scala- that accepts a subset S of the support of F as an additional bility hurdles as UniWit, and is unlikely to scale beyond a input. We call S the set of sampling variables of F , and in- few thousand variables without heuristic adapatations that tend to use an independent support of F (not necessarily compromise its guarantees. a minimal one) as the value of S in any invocation of the 4. THE UNIGEN ALGORITHM generator. Without loss of generality, let S = {x₁, . . . x|S|}, where |S| ≤ |X|. The set RF can now be partitioned by ran- domly choosing h ∈ Hₓₒᵣ(|S∧ The new algorithm, called UniGen, falls in the category |, m, 3) and( α ∈ {0, 1}ᵐ, and) of hashing-based almost-uniform generators. UniGen shares by seeking solutions of F ∧ m h(x , . . . x i ↔ [ ] | | | | i=1 1 |S|)[ ] α i . some features with earlier hashing-based algorithms such as If S X (as is often the case in our experience), the XORSample′ [11], UniWit [5] and PAWS [9], but there are expected number of variables per xor-clause is significantly key differences that allow UniGen to significantly outper- reduced. This makes satisfiability checking easier, and allows form these earlier algorithms, both in terms of theoretical scaling to much larger problem sizes than otherwise possi- ble. It is natural to ask if finding an independent support of guarantees and measured performance.

a CNF formula F is computationally easy. While an algo- Algorithm 2 ComputeKappaPivot(tε) rithmic solution to this problem is beyond the scope of this Find κ ∈ [0, 1) such that ε = (1 + κ)(2.23 + 0.48 ) − 1 ; paper, our experience indicates that a small, not necessar- (1−κ)2 ily minimal, independent support can often be easily deter- pivot ← d3e1/2(1 + 1 )²e; mined from the source domain from which the CNF formula return (κ, pivot) κ F is derived. For example, when a non-CNF formula G is converted to an equisatisfiable CNF formula F using Tseitin The pseudocode for UniGen is shown in Algorithm 1. UniGen encoding, the variables introduced by the encoding form a takes as inputs a Boolean CNF formula F , a tolerance ε dependent support of F . (> 1.71, for teachnical reasons explained in the Appendix) The effectiveness of a hashing-based probabilistic gener- and a set S of sampling variables. It either returns a ran- ator depends on its ability to quickly partition the set RF dom witness of F or ⊥ (indicating failure). The algorithm into “small” and “roughly equal” sized random cells. This, in assumes access to a source of random binary numbers, and turn, depends on the parameter m used in the choice of the to two subroutines: (i) BSAT(F, N), which, for every N > 0, hash function family H(n, m, r). A high value of m leads to returns min(|RF |, N ) distinct witnesses of F , and (ii) an ap- skewed distributions of sizes of cells, while a low value of m proximate model counter ApproxModelCounter(F, ε′, 1 − δ′). leads to cells that are not small enough. The best choice of UniGen first computes two quantities, “pivot” and κ, that m depends on |RF |, which is not known a priori. Different represent the expected size of a “small” cell and the tolerance algorithms therefore use different techniques to estimate a value of m. In XORSample′ , this is achieved by requiring the of this size, respectively. The specific choices of expressions user to provide some difficult-to-estimate input parameters. used to compute κ and “pivot” in ComputeKappaPivot are In UniWit, the algorithm sequentially iterates over values motivated by technical reasons explained in the Appendix. of m until a good enough value is found. The approach of The values of κ and “pivot” are used to determine high and PAWS comes closest to our, although there are crucial dif- low thresholds (denoted “hiThresh” and “loThresh” respec- ferences. In both PAWS and UniGen, an approximate model tively) for the size of each cell. Lines 5–7 handle the easy case counter is first used to estimate |RF | within a specified tol- when F has no more than “hiThresh” witnesses. Otherwise, erance and with a specified confidence. This estimate, along UniGen invokes ApproxModelCounter to obtain an estimate, with a user-provided parameter, is then used to determine C, of |RF | to within a tolerance of 0.8 and with a confi- a unique value of m in PAWS. Unfortunately, this does not dence of 0.8. Once again, the specific choices of the tolerance facilitate proving that PAWS is an almost-uniform genera- and confidence parameters used in computing C are moti- tor. Instead, Ermon, et al. show that PAWS behaves like vated by technical reasons explained in the Appendix. The an almost-uniform generator with probability greater than estimate C is then used to determine a range of candidate 1 − δ, for a suitable δ that depends on difficult-to-estimate qvalues for m. Specifically, this range is {q − 4, . . . q}, where input parameters. In contrast, we use the estimate of |RF | is determined in line 10 of the pseudocode. The loop in to determine a small range of candidate values of m. This lines 12–17 checks whether some value in this range is good allows us to prove that UniGen is almost-uniform generator enough for m, i.e., whether the number of witnesses in a cell with confidence 1. chosen randomly after partitioning RF using Hₓₒᵣ(|S|, m, 3), lies within “hiThresh” and “loThresh”. If so, lines 21–22 re- turn a random witness from the chosen cell. Otherwise, the Algorithm 1 UniGen(F, ε, S) algorithm reports a failure in line 19. /*Assume S = {x₁, . . . x|S|} is an independent support of F , An probabilistic generator is likely to be invoked multi- and ε > 1.71 */ ple times with the same input constraint in constrained- 1: (κ, pivot) ← ComputeKappaPivot(ε); random verification. Towards this end, note than lines 1–11 2: hiThresh ← 1 + (1 + κ)pivot; of the pseudocode need to executed only once for every for- 3: loThresh ← 1+κ¹ pivot; mula F . Generating a new random witness requires execut- 4: Y ← BSAT(F, hiThresh); ing afresh only lines 12–22. While this optimization appears 5: if (|Y | ≤ hiThresh) then similar to “leapfrogging” [5, 6], it is fundamentally different 6: Let y₁, . . . y|Y | be the elements of Y ; since it does not sacrifice any theoretical guarantees, unlike 7: Choose j at random from {1, . . . |Y |}; return yj; “leapfrogging”. 8: else Implementation issues: In our implementation of UniGen, 9: C ← ApproxModelCounter(F, 0.8, 0.8); BSAT is implemented using CryptoMiniSAT [1] – a SAT 10: q ← dlog C + log 1.8 − log pivote; solver that handles xor clauses efficiently. CryptoMiniSAT 11: i ← q − 4; uses blocking clauses to prevent already generated witnesses 12: Choose h at random from Hₓₒᵣ(|S|, n, 3); from being generated again. Since the independent support 13: Choose α at random from {0, 1}ⁿ; of F determines every satisfying assignment of F , blocking 14: repeat clauses can be restricted to only variables in the set S. We 15: i ← i + 1; implemented this optimization in CryptoMiniSAT, leading 16: Y ← BSAT(F ∧ (hi(x₁, . . . x|S|) = αi), hiThresh); to significant improvements in performance. ApproxModelCounter 17: until (loThresh ≤ |Y | ≤ hiThresh) or (i = q) is implemented using ApproxMC [6]. Although the authors 18: if (|Y | > hiThresh) or (|Y | < loThresh) then of [6] used “leapfrogging” in their experiments, we disable 19: return ⊥ this optimization since it nullifies the theoretical guarantees 20: else of [6]. We use “random device” implemented in C++ as the 21: Let y₁, . . . y|Y | be the elements of Y ; source of pseudo-random numbers in lines 7, 14, 15 and 22 of 22: Choose j at random from [|Y |] and return yj; the pseudocode, and also as the source of random numbers in ApproxMC.

Guarantees: The following theorem shows that UniGen is incrementing i. With this set-up, UniGen was able to suc- an almost-uniform generator with a high success probability. cessfully generate random witnesses for formulas having up Theorem 1. If S is an independent support of F and if to 486, 193 variables. ε > 1.71, then for every y ∈ RF , we have For performance comparisons, we also implemented and conducted experiments with UniWit – a state-of-art near-

    for comparison is motivated by several factors. First, UniGen

(1 + ε)(|R1 F | − 1) ≤ Pr [UniGen(F, ε, S) = y] ≤ (1+ε) |RF1| − 1 . uniform generator [5]. Our choice of UniWit as a reference In addition, Pr [UniGen(F, ε, S) = ⊥] ≥ 0.62. and UniWit share some commonalities, and UniGen can be viewed as an improvement of UniWit. Second, XORSample′ For lack of space, we defer the proof to the Appendix. It is known to perform poorly vis-a-vis UniWit [5]; hence, com- can be shown that UniGen runs in time polynomial in ε−1 paring with XORSample′ is not meaningful. Third, the im- and in the size of F , relative to an NP-oracle. plementation of PAWS made available by the authors of [9] The guarantees provided by Theorem 1 are significantly currently does not accept CNF formulae as inputs. It ac- stronger than those provided by earlier generators that scale cepts only a graphical model of a discrete distribution as in- to large problem instances. Specifically, neither XORSample′ [11] put, making a direct comparison with UniGen difficult. Since nor UniWit [5] provide strong upper bounds for the probabil- PAWS and UniWit share the same scalability problem re- ity of generation of a witness. PAWS [9] offers a probabilistic lated to large random xor-clauses, we chose to focus only on guarantee that the probability of generation of a witness lies UniWit. Since the “leapfrogging” heuristic used in [5] nullifies within a tolerance factor of the uniform probability, while the guarantees of UniWit, we disabled this optimization. For the guarantee of Theorem 1 is not prbabilistic. The success fairness of comparison, we used the same timeouts in UniWit probability of PAWS, like that of XORSample′, is bounded as used in UniGen, i.e. 2, 500 seconds for every invocation of below by an expression that depends on difficult-to-estimate BSAT, and 20 hours overall for every invocation of UniWit. input parameters. Interestingly, the same parameters also Table 1 presents the results of our performance-comparison directly affect the tolerance of distribution of the generated experiments. Column 1 lists the CNF benchmark, and columns witnesses. The success probability of UniWit is bounded be- 2 and 3 give the count of variables and size of independent low by 0.125, which is significantly smaller than the lower support used, respectively. The results of experiments with bound of 0.62 guaranteed by Theorem 1. UniGen are presented in the next 3 columns. Column 4 gives Trading scalability with uniformity: The tolerance pa- the observed probability of success of UniGen when gener- rameter ε provides a knob to balance scalability and unifor- ating 1, 000 random witnesses. Column 5 gives the average mity in UniGen. Smaller values of ε lead to stronger guaran- time taken by UniGen to generate one witness (averaged over tees of uniformity (by Theorem 1). Note, however, that the a large number of runs), while column 6 gives the average value of “hiThresh” increases with decreasing values of ε, re- number of variables per xor-clause used for randomly parti- quiring BSAT to find more witnesses. Thus, each invocation tioning RF . The next two columns give results of our exper- of BSAT is likely to take longer as ε is reduced. iments with UniWit. Column 7 lists the average time taken by UniWit to generate a random witness, and column 8 gives 5. EXPERIMENTAL RESULTS the average number of variables per xor-clause used to parti- To evaluate the performance of UniGen, we built a proto- tion RF . A “−” in any column means that the corresponding type implementation and conducted an extensive set of ex- experiment failed to generate any witness in 20 hours. periments. Industrial constrained-random verification prob- It is clear from Table 1 that the average run-time for gen- lem instances are typically proprietary and unavailable for erating a random witness by UniWit can be two to three or- published research. Therefore, we conducted experiments on ders of magnitude larger than the corresponding run-time for CNF SAT constraints arising from several problems avail- UniGen. This is attributable to two reasons. The first stems able in the public-domain. These included bit-blasted ver- from fewer variables in xor-clauses and blocking clauses when sions of constraints arising in bounded model checking of cir- small independent supports are used. Benchmark “tutorial3” cuits and used in [5], bit-blasted versions of SMTLib bench- exemplifies this case. Here, UniWit failed to generate any wit- marks, constraints arising from automated program synthe- ness because all calls to BSAT in UniWit, with xor-clauses sis, and constraints arising from ISCAS89 circuits with par- and blocking clauses containing numbers of variables, timed ity conditions on randomly chosen subsets of outputs and out. In contrast, the calls to BSAT in UniGen took much next-state variables. less time, due to short xor-clauses and blocking clauses us- To facilitate running multiple experiments in parallel, we ing only variables from the independent support. The other used a high-performance cluster and ran each experiment reason for UniGen’s improved efficiency is that the compu- on a node of the cluster. Each node had two quad-core In- tationally expensive step of identifying a a good range of tel Xeon processors with 4 GB of main memory. Recalling values for m (see Section 4 for details) needs to be executed the terminology used in the pseudocode of UniGen (see Sec- only once per benchmark. Subsequently, whenever a random tion 4), we set the tolerance ε to 6, and the sampling set witness is needed, UniGen simply iterates over this narrow S to an independent support of F in all our experiments. range of m. In contrast, generating every witness in UniWit Independent supports (not necessarily minimal ones) for all (without leapfrogging) requires sequentially searching over benchmarks were easily obtained from the providers of the all values afresh to find a good choice for m. Referring to benchmarks on request. We used 2, 500 seconds as the time- Table 1, UniWit requires more than 20, 000 seconds on av- out for each invocation of BSAT and 20 hours as the overall erage to find a good value for m and generate a random timeout for UniGen, for each problem instance. If an invo- witness for benchmark “s953a 3 2”. Unlike in UniGen, there cation of BSAT timed out in line 16 of the pseudocode of is no way to amortize this large time over multiple runs in UniWit, while preserving the guarantee of near-uniformity. UniGen, we repeated the execution of lines 14–16 without

          Table 1 also shows that the observed success probabil-   such generator for Boolean CNF formulae that scales to hun-
ity of          UniGen is almost always 1, much higher than what   dreds of thousands of variables and still preserves strong
Theorem 1 guarantees and better than those from UniWit.            guarantees of uniformity. In future, we wish to investigate
It is clear from our experiments that UniGen        can scale to   the design of scalable generators with similar guarantees for
problems involving almost 500K variables, while preserv-           SMT constraints, leveraging recent progress in satisfiability
ing guarantees of almost uniformity. This goes much beyond         modulo theories.
the reach of any other random-witness generator that gives
strong guarantees on the distribution of witnesses.                Acknowledgments
    500                                                            We profusely thank Mate Soos for implementing required
    450    US                                                      APIs in CryptoMiniSAT without which the experimentation
    400    UniGen                                                  section would have been incomplete. Mate was generous with
    350                                                            his suggestions to improve our implementation. We thank
    300                                                            Ajith John for his help in experimental setup.
    250
    200                                                            7. REFERENCES
    150
    100                                                             [1] CryptoMiniSAT.
     50                                                               http://www.msoos.org/cryptominisat2/.
      0                                                             [2] F. Bacchus, S. Dalmao, and T. Pitassi. Algorithms
    160     180     200   220 240    260 280 300  320                 and complexity results for #SAT and Bayesian
                              Count                                   inference. In Proc. of FOCS, pages 340–351, 2003.
          Figure 1: Uniformity comparison for case110
         Theorem 1 guarantees that the probability of generation    [3] M. Bellare, O. Goldreich, and E. Petrank. Uniform
of every witness lies within a specified tolerance of the uni-        generation of NP-witnesses using an NP-oracle.
form probability. In practice, however, the distribution of           Information and Computation, 163(2):510–526, 1998.
witnesses generated by    UniGen        is much more closer to a    [4] L. Bening and H. Foster. Principles of verifiable RTL
uniform distribution. To illustrate this, we implemented a            design – a functional coding style supporting
uniform sampler, henceforth called US, and compared the               verification processes. Springer, 2001.
distributions of witnesses generated by         UniGen and by US    [5] S. Chakraborty, K. Meel, and M. Vardi. A scalable
for some representative benchmarks. Given a CNF formula               and nearly uniform generator of SAT witnesses. In
F , US first determines       |RF | using an exact model counter      Proc. of CAV, 2013.
(such as sharpSAT). To mimic generating a random witness,           [6] S. Chakraborty, K. S. Meel, and M. Y. Vardi. A
US simply generates a random number i in {1 . . . |RF |}. To          scalable approximate model counter. In Proc. of CP,
ensure fair comparison, we used the same source of random-            2013.
ness in both           UniGen and US. For every problem instance    [7] R. Dechter, K. Kask, E. Bin, and R. Emek.
on which the comparison was done, we generated a large                Generating random solutions for constraint
number N           (= 4 × 10⁶) of sample witnesses using each of      satisfaction problems. In AAAI, 2002.
US and UniGen. In each case, the number of times various            [8] S. Deng, Z. Kong, J. Bian, and Y. Zhao. Self-adjusting
witnesses were generated was recorded, yielding a distribu-           constrained random stimulus generation using
tion of the counts. Figure 1 shows the distributions of counts        splitting evenness evaluation and xor constraints. In
generated by UniGen and by US for one of our benchmarks               Proc. of ASP-DAC, pages 769–774. IEEE, 2009.
(case110) with 16, 384 witnesses. The horizontal axis rep-          [9] S. Ermon, C. P. Gomes, A. Sabharwal, and B. Selman.
resents counts and the vertical axis represents the number            Embed and project: Discrete sampling with universal
of witnesses appearing a specified number of times. Thus,             hashing. In Proc. of NIPS, 2013.
the point (242, 450) represents the fact that each of 450 dis-     [10] V. Gogate and R. Dechter. A new algorithm for
tinct witnesses were generated 242 times in 4 × 10⁶        runs.      sampling csp solutions uniformly at random. In CP,
Observe that the distributions resulting from         UniGen and      pages 711–715, 2006.
US can hardly be distinguished in practice. This holds not         [11] C. Gomes, A. Sabharwal, and B. Selman. Near
only for this benchmark, but for all other benchmarks we
experimented with.                                                    uniform sampling of combinatorial spaces using XOR
    Overall, our experiments confirm that UniGen       is two to      constraints. In Proc. of NIPS, pages 670–676, 2007.
three orders of magnitude more efficient than state-of-the-        [12] C. P. Gomes, J. Hoffmann, A. Sabharwal, and
art random witness generators, has probability of success             B. Selman. Short XORs for model counting; from
almost 1, and preserves strong guarantees about the unifor-           theory to practice. In SAT, pages 100–106, 2007.
mity of generated witnesses. Furthermore, the distribution         [13] M. A. Iyer. Race: A word-level atpg-based constraints
of generated witnesses can hardly be distinguished from that          solver system for smart random simulation. In ITC,
of a uniform sampler in practice.                                     pages 299–308. Citeseer, 2003.
                                                                   [14] M. Jerrum, L. Valiant, and V. Vazirani. Random
6. CONCLUSION                                                         generation of combinatorial structures from a uniform
                                                                      distribution. TCS, 43(2-3):169–188, 1986.
        Striking a balance between scalability and uniformity is   [15] S. Kirkpatrick, C. D. Gelatt, and M. P. Vecchi.
a difficult challenge when designing random witness genera-           Optimization by simulated annealing. Science,
tors for constrained-random verification. UniGen is the first         220(4598):671–680, 1983.

of Solutions

 Table 1: Runtime performance comparison of UniGen and UniWit
                              UniGen        UniWit
                               Succ      Avg         Avg         Avg         Avg    Succ

Benchmark |X| |S| Prob Run Time (s) XOR leng Run Time (s) XOR len Prob Squaring7 1628 72 1.0 2.44 36 2937.5 813 0.87 squaring8 1101 72 1.0 1.77 36 5212.19 550 1.0 Squaring10 1099 72 1.0 1.83 36 4521.11 550 0.5 s1196a 7 4 708 32 1.0 6.9 16 833.1 353 0.37 s1238a 7 4 704 32 1.0 7.26 16 1570.27 352 0.35 s953a 3 2 515 45 0.99 12.48 23 22414.86 257 * EnqueueSeqSK 16466 42 1.0 32.39 21 – – – LoginService2 11511 36 0.98 6.14 18 – – – LLReverse 63797 25 1.0 33.92 13 3460.58 31888 0.63 Sort 12125 52 0.99 79.44 26 – – – Karatsuba 19594 41 1.0 85.64 21 – – – tutorial3 486193 31 0.98 782.85 16 – – – A “*” entry indicates insufficient data for estimating success probability

[16] N. Kitchen. Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation. PhD thesis, University of California, Berkeley, 2010. [17] N. Kitchen and A. Kuehlmann. Stimulus generation for constrained random simulation. In Proc. of ICCAD, pages 258–265, 2007. [18] J. H. Kukula and T. R. Shiple. Building circuits from relations. In Proc. of CAV, pages 113–123, 2000. [19] N. Madras. Lectures on monte carlo methods, fields institute monographs 16. AMS, 2002. [20] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient sat solver. In Proc. of DAC, pages 530–535, 2001. [21] Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, and G. Shurek. Constraint-based random stimuli generation for hardware verification. In Proc of IAAI, pages 1720–1727, 2006. [22] S. M. Plaza, I. L. Markov, and V. Bertacco. Random stimulus generation using entropy and xor constraints. In Proc. of DAC, pages 664–669, 2008. [23] D. Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1):273–302, 1996. [24] M. Sipser. A complexity theoretic approach to randomness. In Proc. of STOC, pages 330–335, 1983. [25] W. Wei, J. Erenrich, and B. Selman. Towards efficient sampling: Exploiting random walk strategies. In Proc. of AAAI, pages 670–676, 2004. [26] W. Wei and B. Selman. A new approach to model counting. In Proc. of SAT, pages 2293–2299, 2005. [27] J. Yuan, A. Aziz, C. Pixley, and K. Albin. Simplifying boolean constraint solving for random simulation vector generation. TCAD, 23(3):412–420, 2004.

APPENDIX Pr [BSAT (F (X~ ) ∧ (h(S[ ) = α), t) = Y ] = In this section, we present a proof of Theorem 1, originally Pr BSAT (F (X ) ∧ (h′(X~ ) = α′), t) = Y ] stated in Section 4, and also present an extended table of performance comparison results. Proof. Since h′ is chosen uniformly at random from Hₓₒᵣ(n, i, 3), Recall that UniGen is a probabilistic algorithm that takes as inputs a Boolean CNF formula F , a tolerance ε and a recalling the definition of ∧ ( Hₓₒᵣ(n, i, 3), we have F (X~ ))∧(h′(X~ ) = subset S of the support of F . We first show that if X is the α′) ≡ F (X~ ) ∧ il=1 (al,0 ⊕ ⊕ⁿj=1 al,j · x[j]) ↔ α′[l] , where support of F , and if S ( X is an independent support of F , the a then UniGen(F , ε, S) behaves identically (in a probabilis- l,js are chosen independently and identically randomly tic sense) to UniGen(F , ε, X). Once this is established, the from {0, 1}. remainder of the proof proceeds by making the simplifying Since S is an independent support of F , from Lemma 1, assumption S = X. there exist Boolean functions∧g₁, . . . gn−k, each with sup- port S, such that F (X~ ) → n−kj (x ↔ g (S~ Clearly, the above claim holds trivially if X = S. There- =1 k+j j )). There- fore, we focus only on the case when S ( X. For nota- fore, F (X~ ) ∧ (h′(X~ ) = α′) is semantically equivalent to tional convenience, we assume X = {x₁, . . . xₙ}, 0 ≤ k < n, F (X~ ) ∧ ∧ⁱ (a ⊕ ⊕ᵏ · x[j] ⊕ B) ↔ α′[l]), where S = {x₁, . . . xₖ} and D = {xₖ₊₁, . . . xₙ} in all the state- ⊕ l=1 l,0 j=1 al,j ments and proofs in this section. We also use X~ to denote B ≡ nj=k+1 al,j·gj−k(S). Rearranging terms, we get F (X )∧ ∧ ( ⊕ ) the vector (x₁, . . . xₙ), and similarly for S~ and D~ . il=1 (al,0 ⊕ kj=1 al,j · x[j]) ↔ (α′[l] ⊕ B) . Since α′ is chosen uniformly at random from {0, 1}ⁱ and Lemma 1. Let F (X~ ) be a Boolean function with support since B is independent of α′, it is easy to see that α′[l]⊕B is a X, and let S be an independent support of F . Then there random binary variable with equal probability of being 0 and[ ] exist Boolean functions g₀, g₁, . . . gn−k, each with support S 1. It follows that Pr BSAT(F (X~ ) ∧ (h′(X~ ) = α′), t) = Y = such that [ ] ( n∧ ) Pr BSAT(F (X~ ) ∧ (h(S) = α), t) = Y . −k F (X ) ↔ g₀(S) ∧ j=1 (xₖ+j ↔ gj(S)) Lemma 2 allows us to continue with the remainder of the proof assuming S = X. It has already been shown in [11] Proof. Since S is an independent support of F , we have that Hₓₒᵣ(n, m, 3) is a 3-independent family of hash func- D = X \ S is a dependent support of F . From the def- tions. We use this fact in a key way in the remainder of inition of a dependent support, there exist Boolean func- our analysis. The following result about Chernoff-Hoeffding tions g₁, . . . gₖ, each with support S, such that F (X~ ) → bounds, proved in [6], plays an important role in our discus- ∧n−k(x ↔ g (S sion. j=1 k+j j )). Let g₀(S) be the characteristic function of the projection Theorem 1. Let Γ be the sum of r-wise independent ran- of RF on S. More formally, g₀(S) ≡ ∨(xₖ₊₁,...xₙ)∈{0,1}n−k F (X ). dom variables, each of which is confined to the interval⌊ [0, 1]⌋, ~ ) → g₀(S). Combining this with the re- It follows that F (X and suppose E[Γ] = μ. For 0 < β ≤ 1, if 2 ≤ r ≤ β²μe−1/2 ≤ sult from the previous paragraph, we get the implication 4 F (X ) → (g₀(S) ∧ ∧n−kj (x g (S ) , then Pr [ |Γ − μ| ≥ βμ ] ≤ e−r/2. =1 k+j ↔ j )) Using notation introduced in Section 2, let RF denote the From the definition of g₀(S) given above, we have g₀(S) → set of witnesses of the Boolean formula F . For convenience F (S, x~ k+1, . . . xn), for some values of xk+1, . . . xn. However, of analysis, we assume that log(|RF | − 1) − log pivot is an we also know that F (X~ ) → ∧n−k(x ↔ (S~ integer, where pivot is the quantity computed by algorithm ( ∧ j=1 )ᵏ⁺ʲ gj )). It follows ComputeKappaPivot (see Section 4). A more careful analy- that g(S) ∧ n−kj=1 (x k+j ↔ gj(S)) → F (X~ ). sis removes this assumption by scaling the probabilities by constant factors. Let us denote log(|RF | − 1) − log pivot by Referring to the pseudocode of UniGen in Section 4, we ob- m. The expression used for computing pivot in algorithm serve that the only steps that depend directly on S are those ComputeKappaPivot ensures that pivot ≥ 17. Therefore, if in line 14, where h is chosen randomly from Hₓₒᵣ(|S|, i, 3), an invocation of UniGen does not return from line 7 of the and line 16, where the set Y is computed by calling BSAT(F ∧ pseudocode, then |RF | ≥ 18. Note also that the expression (h(x₁, . . . x|S|) = α), hiThresh). Since all subsequent steps of εfor computing κ in algorithm ComputeKappaPivot requires the algorithm depend only on Y , it suffices to show that if S ≥ 1.71 in order to ensure that κ ∈ [0, 1) can always be is an independent support of F , the probability distribution found. of Y obtained at line 16 is identical to what we would obtain The following lemma shows that q, computed in line 10 of if S was set equal to the entire support, X, of F . the pseudocode, is a good estimator of m. The following lemma formalizes the above statement. As Lemma 3. Pr[q − 3 ≤ m ≤ q] ≥ 0.8 before, we assume X = {x₁, . . . xₙ} and S = {x₁, . . . xₖ}. Proof. Recall that in line 9 of the pseudocode, an approx- Lemma 2. Let S be an independent support of F (X~ ). Let h imate model counter is invoked to obtain an estimate, C, and h′ be hash functions chosen uniformly at random from of |RF | with tolerance 0.8 and confidence 0.8. By the def- Hₓₒᵣ(k, i, 3) and Hₓₒᵣ(n, i, 3), respectively. Let α and α′ be inition of approximate model counting, we have Pr[ C ≤ tuples chosen uniformly at random from {0, 1}ⁱ. Then, for |R 1. 8 F | ≤ (1.8)C] ≥ 0.8. Thus, Pr[log C −log(1.8) ≤ log |R F | ≤ every Y ∈ {0, 1}ⁿ and for every t > 0, we have log C + log(1.8)] ≥ 0.8. It follows that Pr[log C − log(1.8) −

log pivot−log( 1−1/|R¹ ) ≤ log(|R |−1)−log pivot ≤ log C− The next lemma provides an upper bound of wi,y,α and log pivot + log(1 8) − . Flog(| 1−1/|R1 F)] ≥ 0.8. Substituting q = pi,y. logdlog C + log 1.8 − log pivote, m F= log(|R| F | − 1) − log pivot, Lemma 5. For i < m, both wi,y,α and pi,y are bounded (1.8) = 0.85 and log( 1−1/|R¹ F | ) ≤ 0.12 (since |RF | ≥ 18 above by |R 1 ( 1 ) . on reaching line 10 of the pseudocode), we get Pr[q − 3 ≤ F |−1 1− 21+κ 2 m−i m ≤ q] ≥ 0.8. Proof. We will use the terminology introduced in the proof The next lemma provides a lower bound on the probabil- of Lemma 4. Clearly, μα = |RF₂i|−¹ . Since each γ is a 0-1 ity of generation of a witness. Let[ wi,y,α denote the proba- variable, V [γz,α] ≤ E [γ ]. Therefore, σz,α² ≤ ∑ z,α E [γ ] [Γ ] = 2−m( R F z,α bility Pr pivot ≤ |R | ≤ 1 + (1 + κ)pivot and h(y) = α ≤ ∑ E [γ ] = E z,α z=y,z∈R R 1+κ ] F,h,α z∈RF z,α α | F | − 1). So Pr[ pivot ≤ : h ← |RF,h,α| ≤ 1 + (1 +κ)pivot] ≤ Pr[|R 1+κ − Hₓₒᵣ(n, i, 3) . The proof of the lemma also provides F,h,α| −1 ≤ (1 + κ)pivot]. a lower bound on wm,y,α. From Chebyshev’s inequality, we know that Pr [|Γα − μz,α| ≥ κσz,α] ≤ 1/κ² for every κ > 0. By choosing κ = (1 − 1+κ ) μz,α , we have Pr[|R | − Lemma 4. For every witness y of F , Pr[y is output] ≥ [m−i σz,α F,h,α 1 ≤ (1 + κ)pivot]] ≤ Pr 2 0.8(1−e−1) |(|RF,h,α| − 1) − |RF |−1 | ≥ (1 − 1+κ ) |RF |−1 ≤ 1 (1.06+κ)(|RF |−1) 2i 2m−i 2i (1− 2(1+κ) )2 · m−i Proof. If |RF | ≤ 1 + (1 + κ)pivot, the lemma holds triv- |R 2i . Since h is chosen at random from H (n, m, 3), we F |−1 xor ially (see lines 5–7 of the pseudocode). Suppose |RF | ≥ also have Pr[h(y) = α] = 1/2ⁱ. It follows that wi,y,α ≤ y1 + (1 + κ)pivot and let U denote the event that witness |RF1|−1 (1− 1+κ1 )2 . The bound for pi,y is easily obtained by ∈ RF is output by UniGen on inputs F , ε and X. Let pi,y 2m−i ( ) denote the probability that we return from line 17 for a par- noting that pi,y = Σα∈{0,1}i wi,y,α.2−i . ticular value of i with y in RF,h,α, where α ∈ {0, 1}ⁱ is the Lemma 6. For every witness y of F , Pr[y is output] ≤ value chosen in line 15. Then,Y Pr[U ] = ∪qi=q−3 |Y¹ | pi,y, where 1+κ (2.23 + 0.48 ) is the set of witnesses returned by BSAT in line 16 of the |RF |−1 (1−κ)2 pseudocode. Let fₘ = Pr[q − 3 ≤ m ≤ q]. From Lemma 3, Proof. We will use the terminology introduced in the proof we know that fₘ ≥ 0.8. From the design of the algorithm, of Lemma 4. Pr[U ] = ∪q 1 p ≤ 1+κ ∑q p we also know that 1+κ1 pivot ≤ |Y | ≤ 1 + (1 + κ)pivot. i=q−3 |Y | i,y pivot i=q−3 i,y. We Therefore, Pr[U ] ≥ 1+(1+κ)pivot¹ · pm,y · fₘ. The proof is can sub-divide the calculation of Pr[U ] into three cases based on the range of the values m can take. now completed by showing pm,y ≥ 2¹ₘ (1 − e−1). This gives Case 1 : q − 3 ≤ m ≤ q. Pr[U ] ≥ 0.8(1−e−1) ≥ 0.8(1−e−1) . The last in- Now there are four values that m can take. (1+(1+κ)pivot)2m (1.06+κ)(|R equality uses the observation that 1 pivot / F |−1) To calculate pm,y ≤ 0.06. 1. m = q − 3. We know that pi,y ≤ Pr[h(y) = α] = 21i . , we first note that since y ∈ RF , the Pr[U |m = q − 3] ≤ 1+κ · 1 15 . Substituting the value requirement “y ∈ RF,h,α” reduces to “[ y ∈ h−1(α)”. For α ∈ of pivot and pivot 2q−3 8 m, we get Pr[U |m = q − 3] ≤ 15(1+κ) . {0, 1}ⁿ, we define wm,y,α as Pr pivot ≤ |R 8(|RF |−1) R 1+ κ ] F,h,α| ≤ 1 + (1 + κ) 2. m = q − 2. For i ∈ [q − 2, q] pi,y ≤ Pr[h(y) = α] = pivot and h(y) = α : h ← 2 ) + Σα∈{0,1}ₘ (wm,y,α.2−m)− Hˣᵒʳ(n, m, 3) . Therefore, pm,y = 21i Using Lemma 5, we get pq−3,y ≤ |RF1|−1 (1− 1+κ1 )² . . The proof is now completed by Therefore, Pr[U |m = q − 2] ≤ 1+κ 1 ( 1 showing that w pivot |RF |−1 1− 1+κ and y ∈ {0, 1}ⁿ.m,y,α ≥ (1 − e−1)/2ᵐ for every α ∈ {0, 1}ᵐ 1+κ 1 7 . Noting that pivot = |RF |−1 > 10, Pr[U2 |m = pivot 2q−2 4 2m Towards this end, let us first fix a random y. Now we de- q − 2] ≤ |R1+κF |−1 ( 7₄ + 0.4 ) (1−κ)2 fine an indicator variable γz,α for every z ∈ RF \ {y} such 3. m = q − 1. For i ∈ [q − 1, q], pi,y ≤ Pr[h(y) = α ] = 1 . that γ ( z,α = 1 if h(z) = α, and γz,α = 0 otherwise. Let us 2i fix α and choose h uniformly at random from Hₓₒᵣ(n, m, 3). Using Lemma 5, we get pq−3,y+pq−2,y ≤ |R 1 ( 1 ) + 1 The random choice of h induces a probability distribution on ( 1− 1+22κ (1− 1+κ₂ )) ( F |−1 γz,α such that E[γz,α] = Pr[γz,α = 1] = 2−m. Since we have ( )2 (1− 1+κ )² fixed y, and since hash functions chosen from H pivot |RF |−1 xor(n, m, 3) Therefore, Pr[U |m = q−1] ≤ 1+κ 1 1 + 1 1− 1+κ are 3-wise independent, it follows that for every distinctzₐ , zb ∈ RF {y}, the random variables Noting that pivot = |RF |−1 > 10 and κ ≤ 1, Pr[U 2|m² = 2 independent. Let Γα = ∑ γ γᶻᵃ,α, γᶻᵇ,α are 2-wise q − 1] ≤ 1+κ (1.9 + 2ᵐ0.4 ). z∈R and μ = E[Γ ]. R | − Clearly, Γα = | F,h,α 1 andF {y} z,α∑ α α |RF |−1 (1−κ)2 μα = z∈RF {y} E[γz,α] 4. m = q, pq,y ≤ Pr[h(y) = α] = 2¹q . Using Lemma 5, we = |R₂Fₘ|−1 . Also, Pr[ pivot ≤ |R | ≤ 1 + (1 + κ)pivot] ( = Pr[ pivot − 1 ≤ |R 1+κ| − 1 ≤F,h,α get p 1− 1+κ F,h,α (1 + κ)pivot] ≥ Pr[ pivot ≤ q−3,y+p)q−2,y+pq−1,y ≤ |RF1|−1 (1− 1+κ1 )2 ( 1+κ1 )2 |RF,h,α| − 1 ≤ (1 + 1+κ 23 ( 22 κ)pivot]. Using the expression for pivot, we get 2 ≤ be−1/2(1 + 1/)² · |R₂Fₘ|−1 c. Therefore using The- + 1 . Therefore, Pr[U |m = q] ≤ 1+κ 1 ) |RF |−1 orem 1 and substituting pivot = (|RF | − 1)/2ᵐ, we get ( (1− 1+κ₂ )² ) pivot Pr[ pivot ≤ |R | − 1 ≤ (1 + κ)pivot] ≥ 1 − e−1. Therefore, 1+κ F,h,α ( Pr[ pivot ≤ |R | ≤ 1 + (1 + κ 1− 1+κ123 )2 + (1− 1+κ¹₂₂ )2 + (1− 1+κ¹₂ )² + 1 . Noting that 1+κ F,h,α )pivot] ≥ 1 − e−1 Since h is chosen at random from Hₓₒᵣ(n, m, 3), we also have Pr[h(y) = pivot = |R2Fm|−1 > 10, Pr[U |m = q] ≤ |R1+κ (1.58 + .4 F |−1 α] = 1/2ᵐ. It follows that wm,y,α ≥ (1 − e−1)/2ᵐ. (1−κ)0 2 ).

Pr[U |q − 3 ≤ m ≤ q] ≤ maxi(Pr[U |m = i]). Therefore, Let Γα = ∑ ν and μ = E [Γ ]. Clearly, Γ = y∈R∑ y,α α α α Pr[U |q − 3 ≤ m ≤ q] ≤ Pr[U |m = q − 1] ≤ 1+κ (1.9 + F |RF |−1 |R | and μ = 0.4 ). F,h,α α y∈R E [νy,α] = 2−m|RF |. Since |RF | > (1−κ)2 pivot⌊and i − l > 0, using the expression forF ⌋ pivot, we get Case 2 : m < q − 3. Pr[U |m < q − 3] ≤ 1+κ · 1 15 . 3 ≤ e−1/2(1 + 1 )−2 · |RF | . Therefore, using Theorem 1, Substituting the value of pivot and maximizing we get Pr[U |m < q − 3] ≤ 15(1+κ) . pivotm −2qq−3+ 3,8 Pr [ |R₂ₘF | . (1 − 1+κκε ) ≤ |R²ᵐF,h,α| ≤ (1 + κ) |R₂ₘF | ] > 1− e−3/2. 16(|R F |−1) Simplifying and noting that κ Case 3 : m > q. Using Lemma 5, we know that Pr[U |m > [ 1+κ < κ for all κ > 0, we] ∑ q] ≤ |R1+κF |−1 |R²Fᵐ|−1 qi=q−3 1− 21+κ . The R.H.S. is maxi- obtain Pr (1 + κ)−1 · |R₂ₘF | ≤ |RF,h,α| ≤ (1 + κ) · |R₂ₘF | > m−i 1 − e−3/2. Also, pivot = 1 |RF |−1 ≤ |RF | and 1 + (1 + mized when m = q + 1. Hence Pr[U |m > q] ≤ 1+κ m m F 2 [ m |R2Fm|− ∑qi=q−3 1 . Noting that pivot = |RF|RF |−1 1+κ 1+κ 2m (1+κ)2m 1 1− 1+κ 2m|−1 > κ)pivot = 1 + (1+κ)(|R₂ F |−1) ≥ (1+κ)|R | . Therefore, p = 2q+1−i 10 and expanding the above summation 1+κ F,h,α ] Pr (1 + κ)−1 · |R₂ₘF | ( Pr[U |m > q] )≤ Pr[ pivot ≤ |R | ≤ 1+(1+κ)pivot] ≥ |R1+κF |−1κ101 (1− 1+124κ )2 + (1− 1+κ¹₂₃ )2 + (1− 1+κ122 )2 + (1− 1+κ¹ 2 . ≤ |RF,h,α| ≤ (1 + κ) · |R₂ₘF | ≥ 1 − e−3/2. 21 ) 1 for the first two summation terms, Pr[ Usingq] ≤ U |m > Table 2 presents an extended version of Table 1. We ≤ |R1+κ · 1 · (7.1 + 4 ) F |−1 10 (1−κ)2 Pr[U ] = Pr[U |m < q − observe that UniGen is two to three orders of magnitude Summing up all the above cases, more efficient than state-of-the-art random witness genera- 3] × Pr[m < q − 3] + Pr[U |q − 3 ≤ m ≤ q] × Pr[q − 3 ≤ m ≤ tors, has probability of success almost 1 over a large set of q] + Pr[U |m > q] × Pr[m > q]. Using Pr[m < q − 1] ≤ 0.2, benchmarks arising from different domains. Pr[m > q] ≤ 0.2 and Pr[q − 3 ≤ m ≤ q] ≤ 1. Therefore, Pr[U ] ≤ |R1+κF |−1 (2.23 + 0.48 ) (1−κ)2

     Combining Lemma                     4 and                 6, the following theorem is

obtained.

Theorem 2. For every witness y of F , if ε > 1.71,

(1 + ε)(|R1 F | − 1) ≤ Pr [UniGen(F, ε, X) = y] ≤ (1+ε) |RF1| − 1 .

Proof. The proof is completed by using Lemmas 4 and 6 and substituting (1 + ε) = (1 + κ)(2.23 + 0.48 ). To arrive at (1−κ)2 the results, we use the inequality 1.06+κ ≤ (1 + κ)(2.23 + 0.8(1−e−1) 0.48 ). (1−κ)2

Theorem 3. Algorithm UniGen succeeds (i.e. does not re- turn ⊥) with probability at least 0.62.

Proof. If |RF | ≤ 1 + (1 + κ)pivot, the theorem holds triv- ially. Suppose |RF | > 1 + (1 + κ)pivot and let Psucc de- note the probability that a run of the algorithm UniGen suc- ceeds. Let pi, such that (q − 3 ≤ i ≤ q) denote the condi- tional probability that UniGen (F , ε, X) terminates in it- eration i of the repeat-until loop (line 11-16) with pivot ≤ |RF,h,α| ≤ 1 + (1 + κ∑ 1+κ )pivot, given |RF | > 1 + (1 + κ)pivot. ∏ Therefore, Psucc = qi=q−3 pi ij=q−3(1 − pj). Let fₘ = Pr[q − 3 ≤ m ≤ q]. Therefore, Psucc ≥ pₘfₘ ≥ 0.8pₘ. The theorem is now proved by using Theorem 1 to show that pₘ ≥ 1 − e−3/2 ≥ 0.77. For every y ∈ {0, 1}ⁿ and for every α ∈ {0, 1}ᵐ, define an indicator variable νy,α as follows: νy,α = 1 if h(y) = α, and νy,α = 0 otherwise. Let us fix α and y and choose h uni- formly at random from Hₓₒᵣ(n, m, 3). The random choice of h induces a probability distribution on νy,α, such that Pr[νy,α = 1] = Pr[h(y) = α] = 2−m and E[νy,α] = Pr[νy,α = 1] = 2−m. In addition 3-wise independence of hash func- tions chosen from Hₓₒᵣ(n, m, 3) implies that for every dis- νtinctyc yₐ, yb, yc ∈ RF , the random variables νyₐ,α, νyb,α and ,α are 3-wise independent.

Table 2: Extended Table of Runtime performance comparison of UniGen and UniWit
                            UniGen    UniWit
                             Succ      Avg         Avg        Avg         Avg

Benchmark #Variables |S| Prob Run Time (s) XOR len Run Time (s) XOR len Case121 291 48 1.0 0.19 24 56.09 145 Case1 b11 1 340 48 1.0 0.2 24 755.97 170 Case2 b12 2 827 45 1.0 0.33 22 – – Case35 400 46 0.99 11.23 23 666.14 199 Squaring1 891 72 1.0 0.38 36 – – Squaring8 1101 72 1.0 1.77 36 5212.19 550 Squaring10 1099 72 1.0 1.83 36 4521.11 550 Squaring7 1628 72 1.0 2.44 36 2937.5 813 Squaring9 1434 72 1.0 4.43 36 4054.42 718 Squaring14 1458 72 1.0 24.34 36 2697.42 728 Squaring12 1507 72 1.0 31.88 36 3421.83 752 Squaring16 1627 72 1.0 41.08 36 2852.17 812 s526 3 2 365 24 0.98 0.68 12 51.77 181 s526a 3 2 366 24 1.0 0.97 12 84.04 182 s526 15 7 452 24 0.99 1.68 12 23.04 225 s1196a 7 4 708 32 1.0 6.9 16 833.1 353 s1196a 3 2 690 32 1.0 7.12 16 451.03 345 s1238a 7 4 704 32 1.0 7.26 16 1570.27 352 s1238a 15 7 773 32 1.0 7.94 16 136.7 385 s1196a 15 7 777 32 0.97 8.98 16 133.45 388 s1238a 3 2 686 32 0.99 10.85 16 1416.28 342 s953a 3 2 515 45 0.99 12.48 23 22414.86 257 TreeMax 24859 19 1.0 0.52 10 49.78 12423 LLReverse 63797 25 1.0 33.92 13 3460.58 31888 LoginService2 11511 36 0.98 6.14 18 – – EnqueueSeqSK 16466 42 1.0 32.39 21 – – ProjectService3 3175 55 1.0 71.74 28 – – Sort 12125 52 0.99 79.44 26 – – Karatsuba 19594 41 1.0 85.64 21 – – ProcessBean 4768 64 0.98 123.52 32 – – tutorial3 4 31 486193 31 0.98 782.85 16 – –