SOURCE ARCHIVE
EXTRACTED CONTENT
90,803 charsOn Parallel Scalable Uniform SAT Witness Generation ? ??
Supratik Chakraborty1, Daniel J. Fremont2, Kuldeep S. Meel3,
Sanjit A. Seshia2, and Moshe Y. Vardi3
1 Indian Institute of Technology, Bombay
2 University of California, Berkeley
3 Department of Computer Science, Rice University
Abstract. Constrained-random verification (CRV) is widely used in in-
dustry for validating hardware designs. The e↵ectiveness of CRV depends
on the uniformity of test stimuli generated from a given set of constraints.
Most existing techniques sacrifice either uniformity or scalability when
generating stimuli. While recent work based on random hash functions
has shown that it is possible to generate almost uniform stimuli from
constraints with 100,000+ variables, the performance still falls short of
today’s industrial requirements. In this paper, we focus on pushing the
performance frontier of uniform stimulus generation further. We present
a random hashing-based, easily parallelizable algorithm, UniGen2, for
sampling solutions of propositional constraints. UniGen2 provides strong
and relevant theoretical guarantees in the context of CRV, while also of-
fering significantly improved performance compared to existing almost-
uniform generators. Experiments on a diverse set of benchmarks show
that UniGen2 achieves an average speedup of about 20⇥ over a state-of-
the-art sampling algorithm, even when running on a single core. More-
over, experiments with multiple cores show that UniGen2 achieves a near-
linear speedup in the number of cores, thereby boosting performance even
further.
1 Introduction
Functional verification is concerned with the verification and validation of a Design Under Verification (DUV) with respect to design specifications. With the increasing complexity of DUVs, functional verification has become one of the most challenging and time-consuming steps in design validation [3]. In view of the
? The full version is available at http://www.cs.rice.edu/CS/Verification/Projects/UniGen. ?? The authors would like to thank Suguman Bansal and Karthik Murthy for valuable comments on the earlier drafts, Armando Solar-Lezama for benchmarks, and Mate Soos for tweaking CMS to support UniGen2. This work was supported in part by NSF grants CNS 1049862, CCF-1139011, CCF-1139138, by NSF Expeditions in Computing project ”ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096, by a gift from Intel, by a grant from Board of Research in Nuclear Sciences, India, by the Shared University Grid at Rice funded by NSF under Grant EIA-0216467 and a partnership between Rice University, Sun Microsystems, and Sigma Solutions, Inc., and by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA.
high computational cost of formal verification, simulation-based techniques have been extensively employed in industrial practice. The success of such techniques depends on the quality of input stimuli with which the design is simulated. The generation of high-quality stimuli that uncover hidden bugs continues to be a challenging problem even today [21]. The problem of high-quality stimulus generation has led to the emergence of constrained-random simulation, also known as constrained-random verification (CRV) [22]. In CRV, a verification engineer is tasked with the construction of verification scenarios, expressed as constraints over stimuli. Typically, construct- ing these scenarios involves applying past user experience, inputs from design engineers, and domain-specific knowledge. A constraint solver is then invoked to generate random stimuli satisfying the constraints. Since the distribution of errors in the design is not known a priori, each random stimulus is just as likely to produce an error as any other. Therefore, achieving a uniformly random dis- tribution over stimuli satisfying the constraints is highly desirable. While constraint-solving technologies have witnessed significant advance- ments over the last decade, methods of generating uniformly distributed solutions still face huge scalability hurdles. This has been observed repeatedly in the lit- 4 erature [6] and by industry practitioners . In this paper, we take a step towards remedying the current situation by proposing an easily parallelizable sampling algorithm for Boolean constraints that provides strong theoretical guarantees (similar to those provided by an almost-uniform generator) in the context of CRV, and also runs significantly faster than current state-of-the-art techniques on a diverse set of benchmark problems. Since constraints arising in CRV can often be encoded as propositional formu- lae in conjunctive normal form (CNF), we focus on almost-uniform sampling of satisfying assignments of CNF formulae (known as SAT witnesses). This problem has been extensively studied in both theoretical and practical contexts, and has many applications, including probabilistic reasoning, approximate model count- ing, and Markov logic networks [4]. Until recently, approaches to solving this problem belonged to one of two classes: those which provide strong guarantees of uniformity but scale poorly [2,24], and those which scale to large problem instances but rely on heuristics and hence o↵er very weak or no uniformity guar- antees [11,16,14]. Recently, Chakraborty, Meel, and Vardi [4] proposed a new algorithmic ap- proach to bridge the gap between these two extremes. The main idea behind their approach is to use universal hashing in order to partition the space of witnesses into roughly equal “cells”. Under an appropriate partitioning scheme, choosing a random witness from a randomly chosen cell provides strong unifor- mity guarantees. The most recent instance of this approach is called UniGen [6]. While UniGen scales to formulae much larger than those that can be handled by previous state-of-the-art techniques, the runtime performance of UniGen still falls short of industry requirements.
4 Private Communication: R. Kurshan
Since the end of Dennard scaling, there has been a strong revival of interest in parallelizing a wide variety of algorithms to achieve improved performance [10]. One of the main goals in parallel-algorithm design is to achieve a speedup nearly linear in the number of processors, which requires the avoidance of dependencies among di↵erent parts of the algorithm [8]. Most of the sampling algorithms used for uniform witness generation fail to meet this criterion, and are hence not easily parallelizable. In contrast, the algorithm proposed in this paper is inherently parallelizable, and achieves a near-linear speedup. Our primary contribution is a new algorithm, UniGen2, that addresses key performance deficiencies of UniGen. Significantly, UniGen2 generates many more samples (witnesses) per iteration compared to UniGen, thereby reducing the number of SAT calls required per sample to a constant. While this weakens the guarantee of independence among samples, we show that this does not hurt the primary objective of CRV. Specifically, we prove that UniGen2 provides al- most as strong guarantees as UniGen with respect to discovery of bugs in a CRV setting. On the practical front, we present an implementation of UniGen2, and show by means of extensive experiments that it significantly outperforms exist- ing state-of-the-art algorithms, while generating sample distributions that are indistinguishable from those generated by an ideal uniform sampler. UniGen2 is also inherently parallelizable, and we have implemented a parallel version of it, called parallel UniGen2. Our experiments show that parallel UniGen2 achieves a near-linear speedup with the number of cores.
2 Notation and Preliminaries
Let F denote a Boolean formula in conjunctive normal form (CNF), and let X be
the set of variables appearing in F . The set X is called the support of F . Given
a set of variables S ✓ X and an assignment of truth values to the variables in
X , we write |S for the projection of on S. A satisfying assignment or witness
of F is an assignment that makes F evaluate to true. We denote the set of all
witnesses of F by RF and the projection of RF on S by RF |S. For the rest of
the paper, we use S to denote the sampling set, the set of variables on which
we desire assignments to be projected. Even when no projection is explicitly
desired, S can often be restricted to a small subset of X , called an independent
support, such that |RF |S| = RF (see [6] for details). For notational simplicity,
we omit mentioning F and S when they are clear from the context.
We use Pr [X ] to denote the probability of event X . We say that a set
of events {E1, E2, . . . , En} are (l, u) almost-independent almost-identically dis-
tributed (henceforth, (l, u)-a.a.d.) if if 8i, l Pr[Ei] u and l Pr[Ei|({E1, E2, · · · , En}
Ei)] u. Note that this is similar to the notion of independently identically dis-
tributed (i.i.d.) events, but somewhat weaker.
Given a Boolean formula F and sampling set S, a probabilistic generator of
witnesses of RF |S is a probabilistic algorithm that generates a random witness in
RF |S. A uniform generator Gu(·, ·) is a probabilistic generator that guarantees
Pr [Gu(F, S) = y] = 1/|RF |S|, for every y 2
RF |S. An almost-uniform generator
Gau(·, ·, ·) relaxes the above guarantees, ensuring only that 1/((1 + ")|RF |S|) Pr [Gau(F, S, ") = y] (1+")/|RF |S| for every y 2 RF |S. Probabilistic generators are allowed to occasionally “fail” by returning no witness although RF |S = ;. The failure probability must be bounded by a constant strictly less than 1. A special class of hash functions, called r-wise independent hash functions, play a crucial role in our work. Let n, m and r be positive integers, and let H (n, m, r) denote a family of r-wise independent hash functions mapping {0, 1}n to {0, 1}m. We use h R H (n, m, r) to denote the probability space obtained by choosing a hash function h uniformly at random from H (n, m, r). The property of r-wise independence guarantees that for all ↵1, . . . ↵r 2 {0, 1}m and for all distinct y1, . . . yr 2 {0, 1}n, Pr [Vr h(y ) = ↵ : h R i i=1 i i H (n, m, r) = 2mr. For every ↵ 2 {0, 1}m and h 2 H (n, m, r), let h1(↵) denote the set {y 2 {0, 1}n | h(y) = ↵}. Given RF |S ✓ {0, 1}|S| and h 2 H (|S|, m, r), we use RF |S,h,↵ to denote the set RF |S \ h1(↵). If we keep h fixed and let ↵ range over {0, 1}m, the sets RF |S,h,↵ form a partition of RF |S. We use a particular class of such hash functions, denoted by Hxor(n, m), which is defined as follows. Let h(y)[i] denote the ith component of the vector hL (y). This family of hash functions is then defined as {h | h(y)[i] = ai,0 ( nk=1 ai,k · y[k]), ai,j 2 {0, 1}, 1 i m, 0 j n}, where denotes the XOR operation. By choosing values of ai,j randomly and independently, we can e↵ectively choose a random hash function from Hxor(n, m). It was shown in [12] that this family is 3-wise independent.
3 Related Work
Uniform generation of SAT witnesses was first studied by Jerrum, Valiant, and Vazirani [15], who showed that the problem can solved in probabilistic poly- nomial time given access to a ⌃P2 oracle. In addition, they showed that almost- uniform generation is polynomially inter-reducible with approximate model count- ing. Bellare, Goldreich, and Petrank [2] improved this result and provided an algorithm in BPPNP. Unfortunately, their algorithm fails to scale beyond a few tens of variables in practice [4]. A completely di↵erent approach to uniform gen- eration of SAT witnesses is due to Yuan et al. [24], wherein a sample is generated by performing a random walk over a weighted binary decision diagram (WBDD). The high space requirement of this technique limits its applicability in practice. In several settings (some industrial), generation of stimuli for CRV is typically done via heuristic methods that provide very weak or no guarantees of unifor- mity. One of the earliest such methods was to randomly seed a SAT solver [19]. While this is simple in principle, the distributions generated by random seeding have been shown to be highly skewed in practice [17]. An alternative approach focusing on the generation of “diverse” solutions was proposed by Nadel [20], but it also fails to provide theoretical guarantees of coverage. Markov Chain Monte Carlo (MCMC) algorithms, such as those based on simulated annealing or the Metropolis-Hastings algorithm, have been studied
extensively in the literature [18] in the context of generating samples from a probability space. The eventual convergence to the target distribution for MCMC methods is often impractically slow in practice under mild requirements. Most MCMC-based sampling tools therefore use heuristic adaptations [17,16] to im- prove performance and reduce correlation between samples. Unfortunately, these heuristics significantly weaken or even destroy the theoretical guarantees. Interval propagation [14] has been used extensively in industrial practice to achieve scalable stimulus generation. Techniques based on interval propagation, however, generate highly non-uniform distributions. Recent e↵orts via the con- version of constraints into belief networks [11,7] have also failed to achieve the desired balance between performance and guarantees of uniformity. Recently, several random hashing-based techniques have been proposed to bridge the wide gap between scalable algorithms and those that give strong guar- antees of uniformity when sampling witnesses of propositional constraints [4,6,9]. Hashing-based sampling techniques were originally pioneered by Sipser [23] and further used by Jerrum, Valiant, and Vazirani [15], and Bellare, Goldreich, and Petrank [2]. The key idea in hashing-based techniques is to first partition the space of satisfying assignments into small “cells” of roughly equal size using r- wise independent hash functions (for a suitable value of r), and then randomly choose a solution from a randomly picked cell. Bellare et al. showed that by choosing r = n (where the propositional constraint has n variables), we can guarantee uniform generation. The resulting algorithm, however, does not scale in practice. Chakraborty, Meel, and Vardi [4] subsequently showed that with r = 3, a significantly more scalable near-uniform generator named UniWit can be designed. Building on the principle underlying UniWit, Ermon et al. [9] sug- gested further algorithmic improvements to uniform generation of witnesses. Recently, Chakraborty et al. proposed a new algorithm named UniGen [5], which improves upon the ideas of UniWit. In particular, UniGen provides stronger guarantees of uniformity by exploiting a deep connection between approximate counting and almost-uniform sampling [15]. Furthermore, UniGen has been shown to scale to formulae with hundreds of thousands of variables. Even so, UniGen is typically 2-3 orders of magnitude slower than a single call to a SAT solver and therefore, its runtime performance falls short of the performance of heuristic methods commonly employed in industry to generate stimuli for CRV 5. In this paper, we o↵er several improvements to UniGen and obtain an algorithm with substantially improved performance that can be further scaled by parallelization to match the requirements of industry.
4 A Parallel SAT Sampler
In this section, we first motivate the need for sampling solutions of constraints in parallel, and then provide technical details of our algorithm, UniGen2.
5 A random-constrained test case generator is typically allowed to be 10⇥ slower than a constraint solver (private communication with industry expert W. Hung).
Parallelization: While simulation-based verification typically involves running in parallel many simulations with di↵erent input stimuli, the generation of these stimuli is often done sequentially. This is because existing approaches to stimulus generation are not eciently parallelizable without degrading guarantees of uniformity. For example, approaches based on random seeding of a SAT solver maintain informa- tion about which regions of the solution space have already been explored, since the random seed often is not enough to steer the solver towards new regions of the solution space [17]. Di↵erent threads generating solutions must therefore com- municate with each other, impeding ecient parallelization. In MCMC-based approaches, to generate independent samples in parallel each thread has to take a walk until a stationary distribution is reached. This often takes exponential time in the case of hard combinatorial spaces with complex internal structure [9]. Heuristics to speed up MCMC-based techniques destroy guarantees of uniformity even in the sequential case [17]. Methods based on random walks on WBDDs are amenable to parallelization, but they are known not to scale beyond a few hundred variables. The lack of techniques for sampling solutions of constraints in parallel while preserving guarantees of e↵ectiveness in finding bugs is therefore a major impediment to high-performance CRV. The algorithm UniGen2 presented in this section takes a step forward in addressing the above problem. It has an initial preprocessing step that is se- quential but low-overhead, followed by inherently parallelizable sampling steps. It generates samples (stimuli) that are provably almost as e↵ective as those gen- erated by a uniform sampler for purposes of detecting a bug. Furthermore, our experiments demonstrate that a parallel implementation of UniGen2 achieves a near-linear speedup in the number of processor cores. Given that current prac- titioners are forced to trade guarantees of e↵ectiveness in bug hunting for scal- ability, the above properties of UniGen2 are significant. Specifically, they enable a new paradigm of CRV wherein parallel stimulus generation and simulation can provide the required runtime performance while also providing theoretical guarantees.
Algorithm: Our algorithm, named UniGen2, bears some structural similarities with the UniGen algorithm proposed earlier in [6]. Nevertheless, there are key di↵erences that al- low UniGen2 to outperform UniGen significantly. Like UniGen, UniGen2 takes a CNF formula F , a sampling set S and a tolerance " (that is chosen to be at least 6.84 for technical reasons). Note that the formula F and set S uniquely define the solution set RF |S. Similarly to UniGen, UniGen2 works by partitioning RF |S into “cells” using random hash functions, then randomly selecting a cell by adding appropriate constraints to F . If the chosen cell has the right size (where the acceptable size range depends on the desired tolerance "), we can enumerate all the solutions in it and return a uniform random sample from among them. Unlike UniGen, however, UniGen2 samples multiple times from the same cell. This decreases the
generation time per sample by a large factor (about 10⇥ in our experiments),
while preserving strong guarantees of e↵ectiveness of the samples in finding bugs.
Algorithm 1 EstimateParameters(F, S, ")
/* Returns (hashBits, loThresh, hiThresh) as required by GenerateSamples */
1: Find 2l(0, 1) such that m " = (1 + )(7.44 + 0.392 ) 1
(1)2
2: pivot 4.03 1 + 1 2
⌃ p
3: hiThresh 1 + 2(1 + )pivot⌥; loThresh j p2(1+)₁ pivotk
4: i 0
5: while i < n do
6: i i + 1
7: Choose h at random from Hₓₒᵣ(|S|, i)
8: Choose ↵ at random from {0, 1}ⁱ
9: Y BSAT(F ^ (h(S) = ↵), 61, S)
10: if 1 |Y | 60 then
11: return (round (log |Y | + i + log 1.8 log pivot) , loThresh, hiThresh)
12: return ?
Algorithm 2 GenerateSamples(F, S, hashBits, loThresh, hiThresh)
1: Pick an order V of the values {hashBits 2,hashBits 1, hashBits}
2: for i 2 V do
3: Choose h at random from Hₓₒᵣ(|S|, i)
4: Choose ↵ at random from {0, 1}ⁱ
5: Y BSAT(F ^ (h(S) = ↵), hiThresh, S)
6: if (loThresh |Y | < hiThresh) then
7: return loThresh distinct random elements of Y
8: return ?
UniGen2 is an algorithmic framework that operates in two stages: the first stage, EstimateParameters (Algorithm 1), performs low-overhead one-time pre- processing for a given F , S, and " to compute numerical parameters ‘hashBits’, ‘loThresh’, and ‘hiThresh’. The quantity hashBits controls how many cells RF |S will be partitioned into, while loThresh and hiThresh delineate the range of ac- ceptable sizes for a cell. In the second stage, GenerateSamples (Algorithm 2) uses these parameters to generate loThresh samples. If more samples are required, GenerateSamples is simply called again with the same parameters. Theorem 3 below shows that invoking GenerateSamples multiple times does not cause the loss of any theoretical guarantees. We now explain the operation of the two subroutines in detail. Lines 1–3 of EstimateParameters compute numerical parameters based on the tolerance " which are used by GenerateSamples. The variable ‘pivot’ can be thought of as the ideal cell size we are aiming for, while as mentioned above ‘loThresh’ and ‘hiThresh’ define the allowed size range around this ideal. For simplicity of exposition, we assume that |RF |S| > max(60, hiThresh). If not,
there are very few solutions and we can do uniform sampling by enumerating all of them as in UniGen [6]. Lines 4–11 of EstimateParameters compute ‘hashBits’, an estimate of the num- ber of hash functions required so that the corresponding partition of RF |S (into 2hashBits cells) has cells of the desired size. This is done along the same lines as in UniGen, which used an approximate model counter such as ApproxMC [5]. The procedure invokes a SAT solver through the function BSAT(, m, S). This returns a set, consisting of models of the formula which all di↵er on the set of variables S, that has size m. If there is no such set of size m, the function returns a maximal set. If the estimation procedure fails, EstimateParameters returns ? on line 12. In practice, it would be called repeatedly until it succeeds. Theorem 10 below shows that on average few repetitions are needed for EstimateParameters to succeed, and this is borne out in practice. The second stage of UniGen2, GenerateSamples, begins on lines 1–2 by picking a hash count i close to hashBits, then selecting a random hash function from the family Hxor(|S|, i) on line 3. On line 4 we pick a random output value ↵, so that the constraint h(S) = ↵ picks out a random cell. Then, on line 5 we invoke BSAT on F with this additional constraint, obtaining at most hiThresh elements Y of the cell. If |Y | < hiThresh then we have enumerated every element of RF |S in the cell, and if |Y | loThresh the cell is large enough for us to get a good sample. So if loThresh |Y | < hiThresh, we randomly select loThresh elements of Y and return them on line 7. If the number of elements of RF |S in the chosen cell is too large or too small, we choose a new hash count on line 2. Note that line 1 can pick an arbitrary order for the three hash counts to be tried, since our analysis of UniGen2 does not depend on the order. This allows us to use an optimization where if we run GenerateSamples multiple times, we we choose an order which starts with the value of i that was successful in the previous invocation of GenerateSamples. Since hashBits is only an estimate of the correct value for i, in many benchmarks on which we experimented, UniGen2 initially failed to generate a cell of the right size with i = hashBits2, but then succeeded with i = hashBits1. In such scenarios, beginning with i = hashBits1 in subsequent iterations saves considerable time. This heuristic is similar in spirit to “leapfrogging” in ApproxMC [5] and UniWit [4], but does not compromise the theoretical guarantees of UniGen2 in any way. If all three hash values tried on line 2 fail to generate a correctly-sized cell, GenerateSamples fails and returns ? on line 8. Theorem 1 below shows that this happens with probability at most 0.38. Otherwise, UniGen2 completes by return- ing loThresh samples.
Parallelization of UniGen2 As described above, UniGen2 operates in two stages: EstimateParameters is ini- tially called to do one-time preprocessing, and then GenerateSamples is called to do the actual sampling. To generate N samples, we can invoke EstimateParameters once, and then GenerateSamples N/loThresh times, since each of the latter calls generates loThresh samples (unless it fails). Furthermore, each invocation of
GenerateSamples is completely independent of the others. Thus if we have k pro- cessor cores, we can just perform N/(k ·loThresh) invocations of GenerateSamples on each. There is no need for any inter-thread communication: the “leapfrogging” heuristic for choosing the order on line 1 can simply be done on a per-thread ba- sis. This gives us a linear speedup in the number of cores k, since the per-thread work (excluding the initial preprocessing) is proportional to 1/k. Furthermore, Theorem 3 below shows that assuming each thread has its own source of ran- domness, performing multiple invocations of GenerateSamples in parallel does not alter its guarantees of uniformity. This means that UniGen2 can scale to an arbitrary number of processor cores as more samples are desired, while not sacrificing any theoretical guarantees.
5 Analysis
In this section, we present a theoretical analysis of the uniformity, e↵ectiveness in discovering bugs, and runtime performance of UniGen2. For lack of space, we defer all proofs to the full version. For technical reasons, we assume that " > 6.84. Our first result bounds the failure probabilities of EstimateParameters and GenerateSamples. Theorem 1. EstimateParameters and GenerateSamples return ? with probabili- ties at most 0.009 and 0.38 respectively. Next we show that a single invocation of GenerateSamples provides guarantees nearly as strong as those of an almost-uniform generator.
Theorem 2. For given F , S, and ", let L be the set of samples generated using UniGen2 with a single call to GenerateSamples. Then for each y 2 RF |S, we have loThresh Pr[y 2 L] 1.02 loThresh (1 + ")|RF |S| · (1 + ") |RF |S| .
Now we demonstrate that these guarantees extend to the case when GenerateSamples is called multiple times, sequentially or in parallel.
Theorem 3. For given F , S, and ", and for hashBits, loThresh, and hiThresh as estimated by EstimateParameters, let GenerateSamples be called N times with these parameters in an arbitrary parallel or sequential interleaving. Let Ey,i de- note the event that y 2 RF |S is generated in the ith call to GenerateSamples. Then the events Ey,i are (l, u)-a.a.d. with l = loThresh and u = 1.02·(1+")loThresh . (1+")|RF |S | |RF |S | Next we show that the above result establishes very strong guarantees on the e↵ectiveness of UniGen2 in discovering bugs in the CRV context. In this context, the objective of uniform generation is to maximize the probability of discovering a bug by using a diverse set of samples. Let us denote the fraction of stimuli that trigger a bug by f , i.e. if B is the set of stimuli that trigger a bug, then f = |B|/|RF |S|. Furthermore, if N is the desired number of stimuli we wish to
generate, we want to minimize the failure probability, i.e. the probability that the N randomly generated stimuli fail to intersect the set B. If the stimuli are generated uniformly, the failure probability is (1 f )N . Using binomial expan- sion, the failure probability can be shown to decrease exponentially in N , with decay rate of f (henceforth denoted as failure decay rate ). We can evaluate the e↵ectiveness of a stimulus-generation method by comparing the failure decay rate it achieves to that of a uniform generator. Alternatively, given some > 0, we can ask how many samples are needed to ensure that the failure probability is at most . Normalizing by the number of samples needed by an ideal uni- form generator gives the relative number of samples needed to find a bug. Our next theorem shows that UniGen2 is as e↵ective as an almost-uniform generator according to both of these metrics but needs many fewer SAT calls. Theorem 4. Given F , S, ", and B ✓ RF |S, let f = |B|/|RF |S| < 0.8, ⌫ = 1 (1 + ")f , and ⌫b = 1.02 · loThresh · ⌫ < 1. Then we have the following bounds: 2
generator type uniform UniGen UniGen2
failure decay rate f 1+"f (1 ⌫b) 1+"ᶠ
relative # of samples needed 1 (1 + ⌫)(1 + ") 1+⌫b (1 + ") 1⌫b relative expected # of SAT calls 1 3·hiThresh(1+⌫ 0.52 )(1+") 3·hiThresh 1+⌫b (1 + ") 0.62·loThresh 1⌫b If 8.07 " 243 and f 1/1000, then UniGen2 uses fewer SAT calls than UniGen on average. Thus under reasonable conditions such as occur in industrial applications, UniGen2 is more ecient than UniGen at finding bugs. We illustrate the significance of this improvement with an example. Suppose 1 in 104 inputs causes a bug. Then to find a bug with probability 1/2, we would need approximately 6.93 · 103 uniformly generated samples. To achieve the same target, we would need ap- proximately 1.17 · 105 samples from an almost-uniform generator like UniGen, and approximately 1.20 · 105 samples from UniGen2, using a tolerance (") of 16 in both cases. However, since UniGen2 picks multiple samples from each cell, it needs fewer SAT calls. In fact, the expected number of calls made by UniGen2 is only 3.38 · 106, compared to 4.35 · 107 for UniGen – an order of magnitude di↵erence! Therefore, UniGen2 provides as strong guarantees as UniGen in terms of its ability to discover bugs in CRV, while requiring far fewer SAT calls. Finally, since the ratio of hiThresh to loThresh can be bounded above, the average number of SAT calls per generated sample in UniGen2 can be bounded by a constant. Theorem 5. There exists a fixed constant = 40 such that for every F , S, and ", the expected number of SAT queries made by UniGen2 per generated sample is at most . In contrast, the number of SAT calls per generated sample in UniGen is propor- tional to hiThresh and thus to "2. An upper bound on the expected number of SAT queries makes it possible for UniGen2 to approach the performance of
heuristic methods like random seeding of SAT solvers, which make only one SAT query per generated sample (but fail to provide any theoretical guarantees).
6 Evaluation
To evaluate the performance of UniGen2, we built a prototype implementation in C++ that employs the solver CryptoMiniSAT [1] to handle CNF-SAT aug- mented with XORs eciently 6. We conducted an extensive set of experiments on diverse public domain benchmarks, seeking to answer the following questions:
- How does UniGen2’s runtime performance compare to that of UniGen, a state- of-the-art almost-uniform SAT sampler?
- How does the performance of parallel UniGen2 scale with the # of cores?
- How does the distribution of samples generated by UniGen2 compare with the ideal distribution?
- Does parallelization a↵ect the uniformity of the distribution of the samples?
Our experiments showed that UniGen2 outperforms UniGen by a factor of about 20⇥ in terms of runtime. The distribution generated by UniGen2 is statistically indistinguishable from that generated by an ideal uniform sampler. Finally, the runtime performance of parallel UniGen2 scales linearly with the number of cores, while its output distribution continues to remain uniform.
6.1 Experimental Setup
We conducted experiments on a heterogeneous set of benchmarks used in earlier related work [6]. The benchmarks consisted of ISCAS89 circuits augmented with parity conditions on randomly chosen subsets of outputs and next-state variables, constraints arising in bounded model checking, bit-blasted versions of SMTLib benchmarks, and problems arising from automated program synthesis. For each benchmark, the sampling set S was either taken to be the independent support of the formula or was provided by the corresponding source. Experiments were conducted on a total of 200+ benchmarks. We present results for only a subset of representative benchmarks here. A detailed list of all the benchmarks is available in the Appendix. For purposes of comparison, we also ran experiments with UniGen [6], a state- of-the-art almost-uniform SAT witness generator. We employed the Mersenne Twister to generate pseudo-random numbers, and each thread was seeded in- dependently using the C++ class random device. Both tools used an overall timeout of 20 hours, and a BSAT timeout of 2500 seconds. All experiments used " = 16, corresponding to loThresh = 11 and hiThresh = 64. The experiments were conducted on a high-performance computer cluster, where each node had a 12-core, 2.83 GHz Intel Xeon processor, with 4GB of main memory per core. 6 The tool (with source code) is available at http://www.cs.rice.edu/CS/ Verification/Projects/UniGen
6.2 Results
Runtime performance
We compared the runtime performance of UniGen2 with that of UniGen for
all our benchmarks. For each benchmark, we generated between 1000 and 10000
samples (depending on the size of the benchmark) and computed the average
time taken to generate a sample on a single core. The results of these experiments
for a representative subset of benchmarks are shown in Table 1. The columns
in this table give the benchmark name, the number of variables and clauses,
the size of the sampling set, the success probability of UniGen2, and finally the
average runtime per sample for both UniGen2 and UniGen in seconds. The success
probability of UniGen2 was computed as the fraction of calls to GenerateSamples
that successfully generated samples.
UniGen2 UniGen
Succ.
Benchmark #vars #clas |S| Prob Runtime(s) Runtime(s)
s1238a 3 2 686 1850 32 1.0 0.3 7.17
s1196a 3 2 690 1805 32 1.0 0.23 4.54
s832a 15 7 693 2017 23 1.0 0.04 0.51
case 1 b12 2 827 2725 45 1.0 0.24 6.77
squaring16 1627 5835 72 1.0 4.16 79.12
squaring7 1628 5837 72 1.0 0.79 21.98
doublyLinkedList 6890 26918 37 1.0 0.04 1.23
LoginService2 11511 41411 36 1.0 0.05 0.55
Sort 12125 49611 52 1.0 4.15 82.8
20 15475 60994 51 1.0 19.08 270.78
enqueue 16466 58515 42 1.0 0.87 14.67
Karatsuba 19594 82417 41 1.0 5.86 80.29
lltraversal 39912 167842 23 1.0 0.18 4.86
llreverse 63797 257657 25 1.0 0.73 7.59
diagStencil new 94607 2838579 78 1.0 3.53 60.18
tutorial3 486193 2598178 31 1.0 58.41 805.33
demo2 new 777009 3649893 45 1.0 3.47 40.33
Table 1. Runtime performance comparison of UniGen2 and UniGen (on a single core).
Table 1 clearly shows that UniGen2 significantly outperforms UniGen on all types of benchmarks, even when run on a single core. Over the entire set of 200+ benchmarks, UniGen2’s runtime performance was about 20⇥ better than that of UniGen on average (using the geometric mean). The observed performance gain can be attributed to two factors. First, UniGen2 generates loThresh (11 in our experiments) samples from every cell instead of just 1 in the case of UniGen. This provides a speedup of about 10⇥. Second, as explained in Section 4, UniGen2 uses “leapfrogging” to optimize the order in which the values of i in line 2 of Algorithm 2 are chosen. In contrast, UniGen uses a fixed order. This provides an additional average speedup of 2⇥ in our experiments. Note also that the success probability of UniGen2 is consistently very close to 1 across the entire set of benchmarks. Parallel speedup To measure the e↵ect of parallelization on runtime performance, we ran the parallel version of UniGen2 with 1 to 12 processor cores on our benchmarks. In each experiment with C cores, we generated 2500 samples per core, and
computed the C-core resource usage as the ratio of the average individual core
runtime to the total number of samples (i.e. C ⇥ 2500). We averaged our compu-
tations over 7 identical runs. The speedup for C cores was then computed as the
ratio of 1-core resource usage to C-core resource usage. Figure 1 shows how the
speedup varies with the number of cores for a subset of our benchmarks. The
figure illustrates that parallel UniGen2 generally scales almost linearly with the
number of processor cores.
To obtain an estimate of how close UniGen2’s performance is to real-world
requirements (roughly 10⇥ slowdown compared to a simple SAT call), we mea-
sured the slowdown of UniGen2 (and UniGen) running on a single core relative
to a simple SAT call on the input formula. The (geometric) mean slowdown
for UniGen2 turned out to be 21 compared to 470 for UniGen. This shows that
UniGen2 running in parallel on 2–4 cores comes close to matching the require-
ments of CRV in industrial practice.
14
s1238a_7_4 enqueue
s953a_3_2 LoginService2
12 s1196a_7_4 karatsuba
squaring10 Sort
10 squaring7 LLReverse
squaring8
8
6
4
2
2 4 6 8 10 12
Cores
Fig. 1. E↵ect of parallelization on the runtime performance of UniGen2.
Uniformity comparison
To measure the quality of the distribution generated by UniGen2 and parallel
UniGen2 in practice, we implemented an ideal sampler, henceforth denoted as
IS. Given a formula F , the sampler IS first enumerates all witnesses in RF |S,
and then picks an element of RF |S uniformly at random. We compared the dis-
tribution generated by IS with that generated by UniGen2 run sequentially, and
with that generated by UniGen2 run in parallel on 12 cores. In the last case,
the samples generated by all the cores were aggregated before comparing the
distributions. We had to restrict the experiments for comparing distributions to
a small subset of our benchmarks, specifically those which had less than 100, 000
solutions. We generated a large number N ( 4⇥106) of samples for each bench-
mark using each of IS, sequential UniGen2, and parallel UniGen2. Since we chose
N much larger than |RF |S|, all witnesses occurred multiple times in the list of
samples. We then computed the frequency of generation of individual witnesses,
and grouped witnesses appearing the same number of times together. Plotting
the distribution of frequencies — that is, plotting points (x, y) to indicate that
Speedup
each of x distinct witnesses were generated y times — gives a convenient way to
visualize the distribution of the samples. Figure 2 depicts this for one represen-
tative benchmark (case110, with 16,384 solutions). It is clear from Figure 2 that
500
Ideal
450 ScalGen
ParaScalGen
400
350
300
250
200
150
100
50
0
180 200 220 240 260 280 300
Solution Count
Fig. 2. Uniformity comparison between an ideal sampler (IS), UniGen2, and parallel
UniGen2. Results from benchmark ‘case110’ with N = 4 · 10⁶.
the distribution generated by UniGen2 is practically indistinguishable from that
of IS. Furthermore, the quality of the distribution is not a↵ected by paralleliza-
tion. Similar observations also hold for the other benchmarks for which we were
able to enumerate all solutions. For the example shown in Fig. 2, the Jensen-
Shannon distance between the distributions from sequential UniGen2 and IS is
0.049, while the corresponding figure for parallel UniGen2 and IS is 0.052. These
small Jensen-Shannon distances make the distribution of UniGen2 (whether se-
quential or parallel) indistinguishable from that of IS (See Section IV(C) of [13]).
7 Conclusion
Constrained-random simulation has been the workhorse of functional verification
for the past few decades. In this paper, we introduced a new algorithm, UniGen2,
that outperforms state-of-the-art techniques by a factor of about 20⇥. UniGen2
trades o↵ independence of samples for speed while still providing strong guar-
antees of discovering bugs with high probability. Furthermore, we showed that
the parallel version of UniGen2 achieves a linear speedup with increasing num-
ber of cores. This suggests a new paradigm for constrained-random verification,
wherein we can obtain the required runtime performance through parallelization
without losing guarantees of e↵ectiveness in finding bugs.
References
1. CryptoMiniSAT. http://www.msoos.org/cryptominisat2/.
Occurrences
- M. Bellare, O. Goldreich, and E. Petrank. Uniform generation of NP-witnesses using an NP-oracle. Information and Computation, 163(2):510–526, 2000.
- L. Bening and H. Foster. Principles of verifiable RTL design – a functional coding style supporting verification processes. Springer, 2001.
- S. Chakraborty, K. S. Meel, and M. Y. Vardi. A scalable and nearly uniform generator of SAT witnesses. In Proc. of CAV, pages 608–623, 2013.
- S. Chakraborty, K. S. Meel, and M. Y. Vardi. A scalable approximate model counter. In Proc. of CP, pages 200–216, 2013.
- S. Chakraborty, K. S. Meel, and M. Y. Vardi. Balancing scalability and uniformity in SAT-witness generator. In Proc. of DAC, pages 1–6, 2014.
- R. Dechter, K. Kask, E. Bin, and R. Emek. Generating random solutions for constraint satisfaction problems. In AAAI, pages 15–21, 2002.
- D. L. Eager, J. Zahorjan, and E. D. Lazowska. Speedup versus eciency in parallel systems. IEEE Trans. on Computers, 38(3):408–423, 1989.
- S. Ermon, C. P. Gomes, A. Sabharwal, and B. Selman. Embed and project: Discrete sampling with universal hashing. In Proc. of NIPS, 2013.
- H. Esmaeilzadeh, E. Blem, R. St Amant, K. Sankaralingam, and D. Burger. Dark
silicon and the end of multicore scaling. In Proc. of ISCA, pages 365–376. IEEE,
- V. Gogate and R. Dechter. A new algorithm for sampling CSP solutions uniformly at random. In Proc. of CP, pages 711–715. Springer, 2006.
- C. P. Gomes, A. Sabharwal, and B. Selman. Near uniform sampling of combina- torial spaces using XOR constraints. In Proc. of NIPS, pages 670–676, 2007.
- I. Grosse, P. Bernaola-Galv´an, P. Carpena, R. Rom´an-Rold´an, J. Oliver, and H. E. Stanley. Analysis of symbolic sequences using the Jensen-Shannon divergence. Physical Review E, 65(4):041905, 2002.
- M. A. Iyer. Race: A word-level ATPG-based constraints solver system for smart random simulation. In Proc. of ITC, pages 299–308. Citeseer, 2003.
- M. Jerrum, L. Valiant, and V. Vazirani. Random generation of combinatorial structures from a uniform distribution. TCS, 43(2-3):169–188, 1986.
- N. Kitchen. Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation. PhD thesis, University of California, Berkeley, 2010.
- N. Kitchen and A. Kuehlmann. Stimulus generation for constrained random sim- ulation. In Proc. of ICCAD, pages 258–265, 2007.
- N. Madras. Lectures on Monte Carlo Methods, volume 16 of Fields Institute Mono- graphs. AMS, 2002.
- M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Cha↵: Engi- neering an ecient SAT solver. In Proc. of DAC, pages 530–535. ACM, 2001.
- A. Nadel. Generating diverse solutions in SAT. In Proc. of SAT, pages 287–301. Springer, 2011.
- R. Naveh and A. Metodi. Beyond feasibility: CP usage in constrained-random functional hardware verification. In Proc. of CP, pages 823–831. Springer, 2013.
- 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 AAAI, pages 1720–1727, 2006.
- M. Sipser. A complexity theoretic approach to randomness. In Proc. of STOC, pages 330–335, 1983.
- 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
In this section, we first provide an extended version of Table 1 in Section A. Section B then provides detailed proofs for the theorems stated in Section 5.
A Detailed Experimental Results
Table 2: Extended Runtime performance comparison of UniGen2 and UniGen (on a single core)
UniGen2 UniGen
Benchmark #vars #clas |S| Succ.
Prob Runtime(s) Runtime(s)
109 new 60 55 36 1.0 0.14 19.35
32 new 60 49 38 1.0 0.12 22.66
70 new 62 49 40 1.0 0.13 16.34
29 new 69 55 45 1.0 0.12 6.05
case100 72 178 24 1.0 0.01 0.2
case101 72 178 24 1.0 0.01 0.2
10 new 103 135 46 1.0 0.14 2.18
case47 118 328 28 1.0 0.01 0.08
case124 133 386 31 1.0 0.12 3.43
case55 149 442 26 1.0 0.01 0.15
case8 160 525 26 1.0 0.04 0.96
lltraversal new 163 359 41 1.0 0.19 9.73 case105 170 407 59 1.0 0.3 7.07 case5 176 518 36 1.0 0.65 5.09 treemin new 177 451 29 1.0 0.12 2.55 s344 3 2 197 464 24 1.0 0.12 1.38 s349 3 2 198 469 24 1.0 0.12 1.46 case201 200 544 45 1.0 0.17 5.46 case202 200 544 45 1.0 0.18 5.44 case56 202 722 23 1.0 0.01 0.17 case54 203 725 23 1.0 0.01 0.17 case106 204 509 60 1.0 0.35 8.61 19 new 211 594 48 1.0 0.11 6.76 case133 211 615 42 0.98 136.04 1330.62 case136 211 615 42 0.98 128.91 1710.95 case203 214 580 49 1.0 0.13 5.22 case205 214 580 49 1.0 0.13 5.24 case204 214 580 49 1.0 0.13 5.23 tree delete3 new 215 521 44 0.99 0.27 2.81 s344 7 4 215 540 24 1.0 0.2 1.66 Continued on next page
UniGen2 UniGen
Benchmark #vars #clas |S| Succ. Prob Runtime(s) Runtime(s) s349 7 4 216 545 24 1.0 0.2 1.58 case146 219 558 64 1.0 24.22 386.47 case145 219 558 64 1.0 17.49 478.73 case132 236 708 41 1.0 0.14 2.04 case135 236 708 41 1.0 0.15 2.02 case 1 b14 1 238 681 45 1.0 0.16 5.47 case 2 b14 1 238 681 45 1.0 0.15 5.28 case 3 b14 1 238 681 45 1.0 0.18 5.26 case109 241 915 31 1.0 0.03 0.39 case14 247 649 67 1.0 108.11 2675.16 s382 3 2 263 635 24 1.0 0.04 0.41 case123 267 980 34 1.0 0.4 5.22 case119 267 787 59 1.0 1.21 39.86 case 1 b14 2 270 805 43 1.0 0.17 5.38 case 2 b14 2 270 805 43 1.0 0.16 5.34 case 3 b14 2 270 805 43 1.0 0.18 5.59 case9 279 753 67 1.0 91.03 4632.83 s382 7 4 281 711 24 1.0 0.04 0.47 case61 282 753 66 1.0 103.77 1964.81 s344 15 7 284 824 24 1.0 0.08 1.27 case120 284 851 61 1.0 4.18 198.08 s349 15 7 285 829 24 1.0 0.09 1.23 case57 288 1158 32 1.0 0.85 4.88 s444 3 2 290 712 24 1.0 0.04 0.4 case121 291 975 48 1.0 0.17 5.5 case62 291 1165 33 1.0 0.21 5.59 s420 3 2 294 694 34 1.0 0.36 7.38 s420 new1 3 2 294 694 34 1.0 0.35 7.41 s420 new 3 2 294 694 34 1.0 0.24 6.2 case3 294 1110 26 1.0 0.04 0.84 case2 296 1116 26 1.0 0.05 0.83 s510 3 2 298 768 25 1.0 0.1 1.27 case126 302 1129 34 1.0 0.24 4.88 case 1 b14 3 304 941 40 1.0 0.18 5.61 case 2 b14 3 304 941 40 1.0 0.18 5.62 case 3 b14 3 304 941 40 1.0 0.18 5.76 s444 7 4 308 788 24 0.99 0.13 1.28 s420 new1 7 4 312 770 34 1.0 0.22 5.79 s420 new 7 4 312 770 34 1.0 0.17 5.81 s420 7 4 312 770 34 1.0 0.24 5.79 Continued on next page
UniGen2 UniGen
Benchmark #vars #clas |S| Succ.
Prob Runtime(s) Runtime(s)
case122 314 1258 27 1.0 0.07 1.46
s510 7 4 316 844 25 1.0 0.1 1.21
case6 329 996 52 1.0 0.2 6.96
case 0 b11 1 340 1026 48 1.0 0.21 6.06
case 1 b11 1 340 1026 48 1.0 0.23 6.16
s510 15 7 340 948 25 1.0 0.09 1.23
s382 15 7 350 995 24 1.0 0.14 1.41
s420 new 15 7 351 934 34 1.0 0.16 5.31 s526 3 2 365 943 24 1.0 0.04 0.87 s420 15 7 366 994 34 1.0 0.18 5.3 s420 new1 15 7 366 994 34 1.0 0.19 5.37 s526a 3 2 366 944 24 1.0 0.06 0.6 s444 15 7 377 1072 24 1.0 0.06 0.84 s526 7 4 383 1019 24 1.0 0.09 0.86 77 new 384 2171 44 1.0 0.12 26.92 s526a 7 4 384 1020 24 1.0 0.08 0.98 case125 393 1555 35 1.0 0.44 6.48 case35 400 1414 46 1.0 0.27 8.88 case34 409 1597 39 1.0 0.2 5.78 case143 427 1592 48 1.0 0.2 5.24 case 0 b12 1 427 1385 37 1.0 0.17 4.41 case 2 b12 1 427 1385 37 1.0 0.18 4.39 case 1 b12 1 427 1385 37 1.0 0.19 4.57 case115 428 1851 28 1.0 0.11 2.44 case114 428 1851 28 1.0 0.1 2.43 case131 432 1830 36 1.0 0.26 2.97 case116 438 1881 28 1.0 0.09 2.4 s526 15 7 452 1303 24 1.0 0.07 1.4 s526a 15 7 453 1304 24 1.0 0.07 1.37 isolateRightmost new 483 1498 64 1.0 0.28 18.56 squaring51 496 1947 42 1.0 0.13 2.86 squaring50 500 1965 42 1.0 0.14 2.86 s953a 3 2 515 1297 45 1.0 0.67 11.6 s953a 7 4 533 1373 45 1.0 22.42 1303.7 s953a 15 7 602 1657 45 1.0 0.49 10.64 s820a 7 4 616 1703 23 1.0 0.01 0.15 s832a 7 4 624 1733 23 1.0 0.01 0.12 s820a 15 7 685 1987 23 1.0 0.01 0.11 s1238a 3 2 686 1850 32 1.0 0.3 7.17 s1196a 3 2 690 1805 32 1.0 0.23 4.54 Continued on next page
UniGen2 UniGen
Benchmark #vars #clas |S| Succ. Prob Runtime(s) Runtime(s) s832a 15 7 693 2017 23 1.0 0.04 0.51 squaring24 695 2193 61 1.0 0.29 6.98 squaring22 695 2193 61 1.0 0.28 6.89 squaring20 696 2198 61 1.0 0.29 6.96 squaring21 697 2203 61 1.0 0.27 6.78 s1238a 7 4 704 1926 32 1.0 0.23 3.11 s1196a 7 4 708 1881 32 1.0 0.29 3.3 squaring23 710 2268 61 1.0 0.28 7.05 GuidanceService2 715 2181 27 1.0 0.02 0.34 s1238a 15 7 773 2210 32 1.0 0.21 3.55 s1196a 15 7 777 2165 32 1.0 0.18 4.87 tree delete3 795 2734 32 1.0 0.2 3.64 case 0 b12 2 827 2725 45 1.0 0.25 6.74 case 2 b12 2 827 2725 45 1.0 0.24 6.72 case 1 b12 2 827 2725 45 1.0 0.24 6.77 squaring27 837 2901 61 1.0 0.36 6.39 squaring25 846 2947 61 1.0 0.35 6.66 squaring3 885 2809 72 1.0 0.58 15.94 squaring2 885 2809 72 1.0 0.6 17.15 squaring6 885 2809 72 1.0 0.76 15.81 squaring5 885 2809 72 1.0 0.58 15.49 squaring1 891 2839 72 1.0 0.69 16.0 squaring4 891 2839 72 1.0 0.66 15.49 squaring26 894 3187 61 1.0 0.4 6.92 squaring11 966 3213 72 1.0 0.85 18.53 GuidanceService 988 3088 27 1.0 0.02 0.23 squaring30 1031 3693 61 1.0 0.55 15.3 squaring28 1060 3839 61 1.0 0.46 15.67 llreverse new 1096 4217 47 1.0 0.18 10.1 squaring10 1099 3632 72 1.0 0.73 20.65 squaring8 1101 3642 72 1.0 0.76 19.64 squaring29 1141 4248 61 1.0 0.65 19.42 79 new 1217 4034 40 1.0 2.93 21.24 IssueServiceImpl 1393 4319 30 1.0 0.01 0.1 squaring9 1434 5028 72 1.0 1.03 20.35 squaring14 1458 5009 72 1.0 2.62 48.73 10 1494 2215 46 1.0 0.33 85.45 squaring12 1507 5210 72 1.0 3.25 62.44 27 1509 2707 32 1.0 0.22 6.37 squaring16 1627 5835 72 1.0 4.16 79.12 Continued on next page
UniGen2 UniGen
Benchmark #vars #clas |S| Succ.
Prob Runtime(s) Runtime(s)
squaring7 1628 5837 72 1.0 0.79 21.98
PhaseService 1686 5655 27 1.0 0.01 0.18
27 new 1792 6717 32 1.0 0.38 13.45
ActivityService 1837 5968 27 1.0 0.01 0.17
55 new 1874 8384 46 1.0 3.05 146.83
IterationService 1896 6732 27 1.0 0.01 0.23
ActivityService2 1952 6867 27 1.0 0.01 0.19
aig insertion1 2296 9326 60 1.0 0.18 3.57
111 2348 5479 36 1.0 0.48 15.79
ConcreteActivityService 2481 9011 28 1.0 0.02 0.36 53 2586 10747 32 1.0 0.26 6.96 aig insertion2 2592 10156 60 1.0 0.18 3.54 55 3128 12145 46 1.0 31.11 178.17 ProjectService3 3175 11019 55 1.0 0.68 17.32 NotificationServiceImpl2 3540 13425 36 1.0 0.12 1.34 109 3565 14012 36 1.0 0.88 12.99 51 3708 14594 38 1.0 0.52 18.77 32 3834 13594 38 1.0 0.47 19.39 70 4670 15864 40 1.0 0.78 24.58 ProcessBean 4768 14458 64 1.0 0.8 32.2 56 4842 17828 38 1.0 0.61 15.98 35 4915 10547 52 1.0 1.33 65.12 80 4969 17060 48 1.0 0.98 181.87 tree delete 5758 22105 30 1.0 0.02 0.35 7 6683 24816 50 1.0 1.69 160.65 doublyLinkedList 6890 26918 37 1.0 0.04 1.23 19 6993 23867 48 1.0 3.34 52.28 LoginService 8200 26689 34 1.0 0.08 0.9 29 8866 31557 45 1.0 8.19 100.46 17 10090 27056 45 1.0 35.0 526.58 parity new 10137 44830 50 1.0 4.09 41.08 81 10775 38006 51 1.0 15.19 285.7 LoginService2 11511 41411 36 1.0 0.05 0.55 Sort 12125 49611 52 1.0 4.15 82.8 77 14535 27573 44 1.0 11.33 38.54 20 15475 60994 51 1.0 19.08 270.78 enqueue 16466 58515 42 1.0 0.87 14.67 Karatsuba 19594 82417 41 1.0 5.86 80.29 lltraversal 39912 167842 23 1.0 0.18 4.86 LLReverse 63797 257657 25 1.0 0.73 7.59 Continued on next page
UniGen2 UniGen
Benchmark #vars #clas |S| Succ.
Prob Runtime(s) Runtime(s)
diagStencil new 94607 2838579 78 1.0 3.53 60.18
demo4 new 381129 1801463 45 1.0 4.01 74.68
tutorial3 486193 2598178 31 1.0 58.41 805.33
demo2 new 777009 3649893 45 1.0 3.47 40.33
demo3 new 865935 3509158 45 1.0 6.36 87.12
B Detailed Proofs
In this section, we provide proofs of the various theorems stated previously.
Section B.1 presents proofs of our main results, Theorems 1–5. We also include
a result (Theorem 6) bounding the probability of a particular witness being
generated by UniGen2, which we omitted above for lack of space. These proofs
depend on a number of lemmas about GenerateSamples and EstimateParameters,
presented in Sections B.2 and B.3 respectively.
B.1 Analysis of UniGen2
Theorem 1. EstimateParameters and GenerateSamples return ? with probabili-
ties at most 0.009 and 0.38 respectively.
Proof. By Lemmas 14 and 11 below respectively.
Theorem 2. For given F , S, and ", let L be the set of samples generated using
UniGen2 with a single call to GenerateSamples. Then for each y 2 RF |S, we have
loThresh Pr[y 2 L] 1.02 loThresh
(1 + ")|RF |S| · (1 + ") |RF |S| .
Proof. By Lemma 10 below.
Theorem 3. For given F , S, and ", and for hashBits, loThresh, and hiThresh as estimated by EstimateParameters, let GenerateSamples be called N times with these parameters in an arbitrary parallel or sequential interleaving. Let Ey,i de- note the event that y 2 RF |S is generated in the ith call to GenerateSamples. Then the events Ey,i are (l, u)-a.a.d. with l = loThresh and u = 1.02·(1+")loThresh . (1+")|RF |S | |RF |S |
Proof. Di↵erent invocations of GenerateSamples use independent randomness for
the choices on lines 3, 4, and 7. Therefore the only part of GenerateSamples which
can be a↵ected by earlier invocations is the ordering heuristic used on line 1. But
Lemma 10 shows that the probability that GenerateSamples returns a particular
witness is between l and u regardless of the order used. Therefore l Pr[Ey,i] u
even if conditioned on the results of previous invocations, and so the events Ey,i
are (l, u)-a.a.d..
In the following results, given F , S, ", and B ✓ RF |S, we define f = |B|/|RF |S|, ⌫ = 12 (1+")f , and ⌫b = 1.02·loThresh ·⌫. We also denote the number of independent uniform samples from RF |S needed to hit B with probability at least by Nideal(|B|, ). Theorem 4. Given F , S, ", B, f , ⌫, and ⌫b as above, assume f < 0.8 and ⌫b < 1. Then we have the following bounds:
generator type uniform UniGen UniGen2
failure decay rate f 1+"f (1 ⌫b) 1+"ᶠ
relative # of samples needed 1 (1 + ⌫)(1 + ") 1+⌫b (1 + ")
1⌫b
relative expected # of SAT calls 1 3·hiThresh(1+⌫
0.52 )(1+") 3·hiThresh 1+⌫b (1 + ")
0.62·loThresh 1⌫b
If 8.07 " 243 and f 1/1000, then UniGen2 uses fewer SAT calls than UniGen on average. Proof. The failure decay rates and relative numbers of samples needed for UniGen and UniGen2 are from Lemmas 2 and 3 below respectively. Both UniGen and GenerateSamples make at most hiThresh SAT calls per iteration of their loops, and iterate at most 3 times (see [6] for UniGen). Since UniGen succeeds with probability at least 0.52 (by Theorem 1 of [6]), the expected number of SAT calls it makes per generated sample is at most 3·hiThresh . Since GenerateSamples 0.52 succeeds with probability at least 0.62 (by Theorem 1), and generates loThresh samples when it does, its expected number of SAT calls per sample is at most 3·hiThresh . 0.62·loThresh Finally, the last statement can be checked by numerical computation, noting that under the given conditions we have loThresh 6. Lemma 1. Given F , S, B, f < 0.8, and ⌫ as above, and 0 < 1, we have
Nideal(|B|, ) fln(1/) .
(1 + ⌫)
Proof. First observe that for any x 2 [0, 1),
1 xi x2 X
X
ln(1x) = xi=2 i x 2 1 xi x 2(1x2 x) = x ✓1 + 2(1 x x) ◆ .
i=0
Now since (1 f )Nideal(|B|,) = , we have
Nideal(|B|,) = ln ⇣ ln(1/) ⌘ .
ln (1 f ) f 1 + 2(1ff )
Therefore we obtain the desired result by noting that since " > 6.84, we have
⌫ = 12 (1 + ")f > 3.42f 2(1 f 0.8) 2(1 f f ) .
Lemma 2. Given F , S, ", B, f < 0.8, and ⌫ as above, let an almost-uniform generator Gau(F, ", S) generate N independent samples in a list L. Then h ⇣ ⌘i
Pr[B \ L = ;] 1 exp N 1+"f .- For 0 < 1, if N (1+⌫)(1+")Nideal(|B|, ), then Pr[B\L = ;] 1.
Proof. Index the elements of L as (yi)1i|L|. For any b 2 B, define pb = Pr[ b], where the value is the same for all i 2 P yi = {1, . . . , |L|}, and put P = b2B pb. By the definition of an almost-uniform generator, we have 1/((1 +pb ")|RF |S|) (1 + ")/|RF |S|. Therefore, |B|/(|RF |S|(1 + ")) P |B|(1 + ")/|RF |S|. So
Pr[L \ B = ;] 1 (1 P )N
1 exp (N P )
1 exp ✓ (1 +N |B| ◆ .
")|RF |S|
This proves the first part of the theorem. Now if N (1 + ")(1 + ⌫)Nideal, using the bound on Nideal from Lemma 1 and the fact that P 1+"f gives
Pr[B \ L = ;] (1 P )N
exp [ln(1 P ) · N ]
exp [ln(1 P ) · (1 + ⌫)(1 + ")Nideal]
exp ln(1 P ) · (1 +f ⌫)(1 + ") · ln(1/)
exp ln(1 P ) · (1 + ⌫)
P ln(1/)
exp [1 · ln(1/)]
where we have used the fact that ln(1 x) x for x 2 [0, 1).
Lemma 3. Given F , S, ", B, f < 0.8, and ⌫b < 1 as above, let UniGen2 generate N samples in a list L (by running GenerateSamples N/loThresh times). Then h ⇣ ⌘i
Pr[B \ L = ;] 1 exp N (1 ⌫b) 1+"f .- For 0 < 1, if N 1+⌫b (1 + ")N (|B|, ) 1⌫b ideal then Pr[B \ L = ;] 1 .
Proof. Let R be the set returned by an invocation of GenerateSamples, and r1, . . . , rloThresh be the elements of R. For any b 2 B, define pb = Pr[ where the value is the same for all i 2 Pri = b], {1, . . . , loThresh}, and P = b2B pb.
Now we have
Pr[R \ B = ;] Pr[{r1, . . . , rloThresh} \ B = ;] loThresh · Pr[r1✓2 B] ✓loThresh2 ◆ · Pr[r1, r2 2 B] =loThresh · P loThresh2 ◆ X X pbpb₀ (by pairwise independence) b2B b02B{b} =loThresh · P ✓loThresh2 ◆ X pb(P pb) ✓loThresh◆ b2B loThresh · P 2 X pbP
loThresh · P · ✓1 loThreshb2B· P ◆ .
2
Now since 1/((1 + ")|RF |S|) pb 1.02(1 + ")/|RF |S| by Theorem 3, we have
f /(1 + ") P 1.02f (1 + "). So
Pr[R\B = ;] loThresh·P ·✓1 loThresh · 1.02f2 (1 + ") ◆ = (1⌫b)·loThresh·P.
Now by Theorem 3 this holds even when conditioned on the results of prior calls
to GenerateSamples, so
Pr[L \ B = ;] 1 (1 (1 ⌫b) · loThresh · P )N/loThresh
1 exp ((1 ⌫b) · N P )
1 exp N (1 ⌫b) ✓ 1 +f " ◆ .
This proves the first part of the theorem. Now since ⌫b ⌫, Lemma 1 shows that
Nideal(|B|, ) fln(1/) .
(1 + ⌫b)
Therefore if N 1+⌫b (1 + ")N , from above we have
1⌫b ideal
Pr[L \ B = ;] exp N (1 ⌫b) ✓ 1 +f " ◆
exp ✓ 1 +1 ⌫b◆ (1 + ")N · (1 ⌫b) ✓ f ◆
⌫b ideal 1 + "
= exp (f (1 + ⌫b) · Nideal)
exp [1 · ln(1/)]
.
Theorem 5. There exists a fixed constant = 40 such that for every F , S, and
", the expected number of SAT queries made by UniGen2 per generated sample is
at most .
Proof. A successful invocation of GenerateSamples produces loThresh samples and makes at most 3 · hiThresh SAT queries (at most hiThresh for each call to BSAT). Since by Lemma 1 GenerateSamples succeeds with probability at least 0.62, the expected number of SAT queries per generated sample is at most (3 · hiThresh)/(0.62 · loThresh). Optimization shows that hiThresh/loThresh < 8.2, so the expected number of queries per sample is less than 40.
Finally, we give a theorem left out of Section 5 for lack of space, bounding the
probability of generating a given witness with multiple calls to GenerateSamples.
Theorem 6. Given F , S, and " as above, let UniGen2 generate N samples in a
list L (by running GenerateSamples N/loThresh times). Then for each y 2 RF |S,
0.93 · N Pr[y 2 N
(1 + ")|RF |S| L] 1.02(1 + ") |RF |S| .
Proof. By Theorem 3, if R is the set returned by a single invocation of GenerateSamples
we have
(1 +loThresh Pr[y 2 R] 1.02 · loThresh(1 + ")
")|RF |S| |RF |S|
regardless of the results of any prior invocations. Therefore
Pr[y 2 L] = 1 Pr[y 2 L] 1 ✓ 1 loThresh ◆N/loThresh
(1 + ")|RF |S| .
Now noting that
(1 +loThresh · N = N 1 ,
")|RF |S| loThresh (1 + ")|RF |S| 7.84
applying the binomial theorem and observing that the sum of the cubic and
higher order terms is positive, we have
Pr[y 2 L] N ✓1 1 ◆ 0.93 · N
(1 + ")|RF |S| 2! · 7.84 = (1 + ")|RF |S| .
For the upper bound, a similar argument shows that
Pr[y 2 L] 1 ✓1 1.02(1 + ")loThresh ◆N/loThresh 1.02(1 + ")N .
|RF |S| |RF |S|
B.2 Analysis of GenerateSamples
Throughout this section, we use the notations RF |S and RF |S,h,↵ introduced in Section 2. We denote by Uy the event that witness y 2 RF |S is output by GenerateSamples when called with the parameters calculated by EstimateParameters on inputs F , S, and ". We are interested in providing lower and upper bounds for Pr[Uy]. The proofs presented here follow the structure of the proofs in [6]. We make use of the following fact from probability theory.
Lemma 4. Let E1, E2, · · · En be a sequence of events returning values in {0, 1}, where event Ei is performed only after all events Ej for j < i return 0. Let E be the event that at least one 1. Then P Ei returns ni Pr[Ei = 1]. maxi Pr[Ei = 1] Pr[E]
Proof. Let us denote prob[Ei = 0|Ej = 0] to denote the conditional probability of Ei returning 0 given that Ej returns 0. Let Pr[ E¯] denote the probability of complement of E. By definition of E, we have Pr[ E¯] = Qni=1 Pr[ E¯i|Ej,j<i¯ , ] mini Pr[Ei = 0]. Therefore, Pr[E] maxi Pr[Ei = 1]
The following result about Cherno↵-Hoe↵ding bounds, proved in [5], plays an
important role in the analysis of UniGen2.
Lemma 5. Let be the sum of r-wise independent random variables, each of
which is confined to the interval2 ⌅ ⇧ [0, 1], and suppose E[ ] = μ. For 0 < 1, if
r 3 2μe1/2 , then Pr [ | μ| μ ] e3/2.
Let us denote round(log(|RF |S| 1) log pivot) by m, where ‘pivot’ is the
quantity computed on line 2 of EstimateParameters. The expression used for
computing pivot ensures that pivot 17. Also, as mentioned in Section 4, for
simplicity we assume that |RF |S| > max(60, hiThresh) (in practice this can
be checked by simply enumerating up to max(60, hiThresh) witnesses). Finally,
note that the expression for computing on line 1 of EstimateParameters requires
" 6.84 in order to ensure that 2 [0, 1) can always be found.
The next lemma provides a lower bound on the probability of generationh
of a witness. Let wi,y,↵ denote the probability Pr pivot |R | 1+
p2(1 + )pivot and h(y) = ↵ : h R i 2(1+) F |S,h,↵
Hxor(n, i) . The proof of the lemma also
provides a lower bound on wm,y,↵. Let pi,y denote the probability that GenerateSamples returns on line 7 with a particular value of i and with y in RF |S,h,↵, where ↵ 2 {0, 1}i is the value chosen on line 4. Also let fm = Pr[q 2 m q], where q is shorthand for the quantity hashBits computed by EstimateParameters.
Lemma 6. Regardless of the order chosen on line 1 of
have loThresh · f · p Pr[ loThresh Pq p GenerateSamples, we
hiThresh m m,y Uy] |Y | i=q2 i,y for each y 2 RF |S.
Proof. By Lemma 4, it follows that Pr[Uy] loThresh max p loThresh |Y | i i,y hiThresh · pm,y · fm. Lemma 4 also implies the upper bound, since |Y | loThresh.
All subsequent results in this section will bound Pr[Uy] using Lemma 6, so
they also hold regardless of the order of hash counts. For notational simplicity
we do not always mention this fact in the lemma statements.
Lemma 7. For every y 2 RF |S, Pr[Uy] 0.8(1e3/2)
2(1.05+)(|RF |S |1)
Proof. From Lemma 6, we have Pr[Uy] loThresh · fm · pm,y . Therefore, Pr[Uy] hiThresh 1+ploThresh · p · f . By Lemma 16, f > 0.8. The proof is now completed 2(1+)pivot m,y m m by showing pm,y 21ₘ (1 e3/2). This gives Pr[Uy] 0.8(1pe3/2)loThresh (1+ 2(1+p )pivot)2m 0.8(1e3/2)loThresh . The last inequality uses the observation that 1/( 2·pivot) 2(1.05+)(|RF |S |1) p 0.05 and p12 |RF2|Sm|1 pivot 2 |RF |S |1 . 2 m To calculate pm,y , we first note that since y 2 RF |S, the requirement “yh 2 RF |S,h,↵” reduces to “y 2 h1(↵)”. For ↵ 2 2(1+) p {0, 1}n, we define wm,y,↵ asi Pr pivot |RF |S,h,↵| 1+ 2(1 + ) pivot and h(y) = ↵ : h R Hxor(n, m) . Therefore, pm,y = ⌃↵2{0,1}ₘ (wm,y,↵ · 2m). The proof is now completed by showing that wm,y,↵ (1 e3/2)/2m for every ↵ 2 {0, m and y 2 {0, 1}n. 1} Towards this end, let us first fix a random y. Now we define an indicator variable z,↵ for every z 2 RF \ {y} such that z,↵ = 1 if h(z) = ↵, and z,↵ = 0 otherwise. Let us fix ↵ and choose h uniformly at random from Hxor(n, m). The random choice of h induces a probability distribution on z,↵ such that E[z,↵] = Pr[z,↵ = 1] = 2m. Since we have fixed y, and since hash func- tions chosen from Hxor(n, m, 3) are 3-wise independent, it follows that for every distinct za, zb 2 R dent. Let ↵ = PF \ {y}, the random variables zₐ,↵, zb,↵ are 2-wise indepen- 1 and μ↵ = P z2RF {yE}[z,↵ and μ↵ = E[↵]. Clearly, ↵ = |RF |S,h,↵| 2 m p z2RF {y} z,↵] = |RF |1 . Also, Pr[ pivot | 1 + 2(1 + )pivot] = Pr[ pivot p2(1+) p |RF |S,h,↵ 2(1+) 1 |RF |S,h,↵| 1 2(1 + )pivot] Pr[ pivot |R 1 p 2(1+) F |S,h,↵| 2(1 + )pivot]. Using the expression for pivot, we get 2 be1/2(1 + 1/✏)2 · |R2Fₘ|1 c. Therefore using Lemma 5 and substituting pivot = (|RF | 1)/2m, we get Pr[ pivot |R | 1 p2(1 + )pivot] 1 e3/2. Therefore, Pr[ pivot 2(1+) F |S,h,p↵ 2(1+) |RF |S,h,↵| 1 + 2(1 + )pivot] 1 e3/2 Since h is chosen at random from Hxor(n, m), we also have Pr[h(y) = ↵] = 1/2m. It follows that wm,y,↵ (1 e3/2)/2m.
The next lemma provides an upper bound on wi,y,↵ and pi,y.
Lemma 8. For i < m1, both wi,y,↵ and pi,y are bounded above by |RF |S1 |1 (1 2(1+)₂1 )² . mi Proof. We will use the terminology introduced in the proof of Lemma 7. Clearly, μ↵ = |RPF 2|Si|1 . Since each z,↵ is a 0-1 variable, V [ ] E [ ]. Therefore, 2 E [ ] P E [ ] = Ez,↵ z,↵ z,↵ z=y,z2RF |S z,↵ z2RF |S z,↵ [↵] = 2i(|RF |S| 1).
So Pr[ pivot |R p [ R | 1
)p 2(1+) F |S,h,↵| 1 + (1 + ) 2pivot] Pr | F |S,h,↵ (1 +
2pivot] Pr[|RF |S,h,↵|1 2(1+) |RF |S |1 ]. From Chebyshev’s inequality,
2
we know that Pr [|↵ μz,↵| z,↵] m 2 for every > 0. By choosing 1/ = (1 2(1+)2 ) μz,↵ (Note that > 0 for i < m 1), we have Pr[|R | mi z,↵ h F,h,↵ i 1 (1 + )2 |RF2|Sₘ|1 ] Pr |(|RF,h,↵| 1) |RF 2|Si|1 | (1 2(1+)2 ) |RF |S |1 mi 2i (1 2(1+)₂1 )² · |R 2i . Since h is chosen at random from H (n, m), we also mi F |S |1 xor have Pr[h(y) = ↵] = 1/2i. It follows that wi,y,↵ |RF |S1 |1 (1 2(1+)₂1 )² . The bound for pi,y is easily obtained by noting that pi,y = ⌃↵2{0,1}i w mi i i,y,↵ · 2 .
This allows us to give an upper bound for Pr[Uy].
Lemma 9. For every y 2 RF |S, Pr[Uy] |RF1+ (7.55 + 0.29 ).
|S |1 (1)2
Proof. We will use the terminology introduced in the proof of Lemma 7. The
proof below uses the inequality 2m⇥pivot |RFp|S | at several points. Also, From
Lemma 6, we have Pr[Uy] Pqi=q2 loThresh p 2 p2(1+)loThresh Pq p .
|Y | i,y pivot i=q2 i,y
We can sub-divide the calculation of Pr[Uy] into three cases based on the range
of the values m can take.
Case 1 : q 2 m q.
Now there are three values that m can take.
m = q 2. We know that pi,y Pr[h(y) = ↵] = 1 . Therefore, Pr[U |m = p 2i y q 2] 2(1+)loThresh · 1 7 . Substituting the value of pivot and m, we pivot 2q2 4 get Pr[Uy|m = q 2] 7(1+)loThresh . 2(|RF |S |1)
m = pq 1. For i 2 [q 2, q] pi,y Pr[h(y) = ↵] = 21i . Pr[Uy|m = q 1] 2(1+)loThresh · 1 7 . Substituting the value of pivot and m, we get pivot 2q2 2 Pr[Uy|m = q 2] 7(1+)loThresh . |RF |S |1
- m = q. For i 2 [q Pr[h(y) = ↵] = 21i .. Using Lemma 8, we get ✓ 1, q] pi,y ◆ p p✓q2,y |✓ 1 1 . Therefore, Pr[U |m = q] 2(1+)loThresh 1 RF |S |11 (1+1+₂3 )² . Noting that pivot y 17 and 1, Prpivot |RF |S |1 (1 1+₂ )² 2q [Uy|m = q] (1+)loThresh (6 + 0.333 ). |RF |S |1 (1)2
Pr[Uy|q 2 m q] maxi(Pr[Uy|m = i]). Therefore, Pr[Uy|q 2 m q] Pr[Uy|m = q] (1+)loThresh (6.667 + 0.333 |RF |S |1 (1p) 2 ).
Case 2 : m < q 2. Pr[Uy|m < q 3] 2(1+) · 1 7 . Substituting the value pivot 2q3 4 of pivot and maximizing m = q + 3, we get Pr[Uy|m < q 2] 7(1+)loThresh . 4(|RF |S |1)
p
Case 3 :Pm > q.Pr[Uy|m > q] Pr[Uy|m = q + 1] = 2(1+)loThresh ( 2 + pivot 2m i=q2 1 2(1+)2 |RF |S1 |1 ( q1 1 )). Noting that pivot 17 and expanding the sum- mation, Pr[U mi (1+ ✓ p ✓ ◆◆ y|m > q] |RF)loThresh 4 + 2 1 + 1 . |S |1 17 (1 2(1+)23 )2 (1 2(1+)22 )2 Using < 1 for the first term, Pr[Uy|m > q] (1+|R)loThreshF (4.333 + 0.333 ) Summing up all the above cases, Pr[Uy] = Pr |S |1 (1)2 [Uy|m < q 2] ⇥ Pr[m < q 2] + Pr[Uy|q 2 m q] ⇥ Pr[q 2 m q] + Pr[Uy|m > q] ⇥ Pr[m > q]. From Lemma 15, we have Pr[m < q 1] + Pr[m > q] 0.177 and Pr[q 3 m q] 1. Also, Pr[Uy|m < q 2] Pr[Uy|m > q]. Therefore, Pr[Uy|m < q 2] ⇥ Pr[m < q 2] + Pr[Uy|m > q] ⇥ Pr[m > q] 0.177 ⇥ Pr[Uy|m > q] Therefore, Pr[Uy] (1+)loThresh (7.44 + 0.392 |RF |S |1 (1)2 ). Combining Lemmas 7 and 9, the following lemma is obtained. Lemma 10. Regardless of the order chosen on line 1 of GenerateSamples, for every y 2 RF |S and " > 6.84 we have
loThresh Pr[U 1 loThresh
(1 + ")|RF |S| y] .02(1 + ") |RF |S| .
Proof. The proof is completed by using Lemmas 7 and 9 and substituting (1 + ") = (1 + )(7.44 + 0.392 ). To arrive at the results, we use the inequality (1)2 2(1.05+) (1+)(7.44+ 0.392 ). Furthermore, we use loThresh < loThresh . 0.8(1e3/2) (1)2 (1+")|RF |S | (1+")(|RF |S |1) Also, since we assume |RF |S| 1 60, we have (1+")loThresh < 1.02(1+")loThresh . |RF |S |1 |RF |S | Lemma 11. GenerateSamples succeeds (i.e. does not return ?) with probability at least 0.62.
Proof. As mentioned above, we are assuming |RF |S| > 1 + p2(1 + )pivot. Let Psucc denote the probability that GenerateSamples succeeds. Let pi with q 2 i q denote the conditional probability that the condition on line 6 of GenerateSamples evaluates to true with pivot |R | 1 + p )pivot, given that |RF |S| > 1 + p2(1 + 2(1+) F |S,h,↵ 2(1 + )pivot. Let fm = Pr[q 2 m q]. Therefore as shown in Lemma 6, Psucc pmfm 0.8pm. The theorem is now proved by using Lemma 5 to show that pm 1 e3/2 0.77. For every y 2 {0, 1}n and for every ↵ 2 {0, 1}m, define an indicator variable ⌫y,↵ as follows: ⌫y,↵ = 1 if h(y) = ↵, and ⌫y,↵ = 0 otherwise. Let us fix ↵ and y and choose h uniformly at random from Hxor(n, m). The random choice of h induces a probability distribution on ⌫y,↵, such that Pr[⌫y,↵ = 1] = Pr[h(y) = ↵] = 2m and E[⌫y,↵] = Pr[⌫y,↵ = 1] = 2m. In addition 3-wise independence of hash functions chosen from Hxor(n, m) implies that for every distinct ya, yb, yc 2 RF |S, the random variables Let ↵ = P ⌫ and⌫yᵃ,↵μ, ⌫y=ᵇ,↵Eand ⌫yc,↵ are 3-wise independent. P E [⌫ y2RF |S y,↵ ↵ [↵]. Clearly, ↵ = |RF,h,↵| and μ↵ = y2RF |S y,↵] = 2 m|RF |S|. Since |RF |S| > pivot and i l > 0, using the
j k
expression for pivot we get 3 e1/2(1 + 1
h ⇣ ⌘ )2 · |R2Fm|Si| . Therefore, by Lemma
5, Pr |R2Fm|S | . 1 1+ |RF |S,h,↵| (1 + ) |R2Fₘh|S | > 1 e3/2. Simplifying and noting that 1+i < for all > 0, we obtain Pr (1 + )1 · |R2Fₘ|S | |RF |S,h,↵| (1 + ) · |R2F |S | > 1 e3/2. Also, pivot 1 |RF |S |1 |RF |S | and 1 + p m 2(1+) 1+ 2m (1+)2m 2(1+)pivot 1+ (1+)(|RF |S |1) (1+)|RF |S | . Therefore, p = Pr[ pivot 2m 2 p h m m p2(1+) i |RF |S,h,↵| 1+ 2(1+)pivot] Pr (1 + )1 · |R2Fₘ|S | |RF |S,h,↵| (1 + ) · |R2Fₘ|S | 1 e3/2.
B.3 Analysis of EstimateParameters
In this section we define ` = log(60) 1 and μ = E[|RF |S,h,↵|] = 2i|RF |S|. Putting HC(x) = round(log x + log 1.8 log pivot), we show that the value hashBits computed by EstimateParameters is a good estimate of HC(|RF |S|) with high probability. The following property of pairwise independent hash functions is the main tool in our analysis. Lemma 12. With h and ↵ chosen as in EstimateParameters, for each > 0 we have Pr[(1 )μ |RF |S,h,↵| (1 + )μ] 1 12μ .
Proof. By pairwise independence, the variance of |RF |S,h,↵| is at most μ. The
result then follows from Chebyshev’s inequality.
Lemma 13. Let EstimateParameters return a hashBits value of c, with i being
the final value of its loop counter. Then
h i
Pr HC((1.8)1 · |RF |S|) c HC(1.8 · |RF |S|) c = ? and i + ` log2 |RF |S| 0.831.
Proof. Since c = ?, by line 11 of the pseudocode we have c = HC(2i ·|RF |S,h,↵|),
where ↵, i and h denote (with abuse of notation) the values of the corresponding
variables in the final iteration of the loop. As mentioned above, we are assuming
that |RF |S| > 60. Since i + ` log2 |RF |S|, we have μ = 2i|RF |S| 2` = 30.
Applying Lemma 12 with = 0.8/(1 + 0.8) < 0.8, we obtain
Pr[(1.8)1 · 2i|RF |S| |RF |S,h,↵| (1.8) · 2i|RF |S|] 1 5.0625 0.831.
μ
Lemma 14. Given |RF |S| > 60, the probability that EstimateParameters returns
non-? with i + ` log |R |, is at least 0
2 F |S .991.
Proof. Let us denote log2 |RF |S| = log2 |R | (blog (60)c 1) by . Since n, we have < m + n. Let pi (
|RF |S| > 60 as noted above and |RF |S| F |S 2 m
2
i n) denote the conditional probability that EstimateParameters terminates
in iteration i of its loop with 1 |RF |S,h,↵| 60, given |RF |S| > 60. Since
the choice of h and ↵ in each iteration of the loop are independent of those in
previous iterations, the conditional probability that EstimateParameters returns
non-? with i log2 |RF |S| = m + l, given |RF |S| > 60, is p + (1 p)p+1 + · · · + (1 p)(1 p+1) · · · (1 p ⇣+. Let us denote this sum by
P Q m+1)pm P = p + m+ i1 (1 p )p p + Pm+1 Qi1 (1 ⌘P . Thus,
Qm+1(1pi=+1 k= k i i=+1 k= pk)pi pm+ + s= s)pm+ = pm+. The lemma is now proved by showing that pm+0.991. Applying Lemma 12 with = 1 1/30 and i = m = log2 |RF |S|, and
noting that μ = 2i|RF |S| = 2` = 30, we have Pr[1 |RF |S,h,↵| 59] 0.991.
Now we can establish that EstimateParameters provides a good estimate of
HC(|RF |S|).
Lemma 15. With hashBits computed by EstimateParameters, we have
Pr ⇥c = ? and HC((1.8)1 · |RF |S|) hashBits HC((1.8) · |RF |S|)⇤ > 0.823.
Proof. Combine Lemmas 13 and 14, getting an overall success probability of at
least 0.831 · 0.991 > 0.823.
This in turn means that hashBits is a good estimate of the quantity m used
in the analysis of GenerateSamples.
Lemma 16. Let m = round(log(|RF |S| 1) log pivot) be defined as in Sec-
tion B.2. For the value hashBits computed by EstimateParameters, we have
Pr[hashBits 2 m hashBits] > 0.823.
Proof. Straightforward computation from Lemma 15, noting that |RF |S| > 60.