Balancing Scalability and Uniformity in SAT Witness Generator

Abstract

Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on two key factors: the quality of constraints used to generate test vectors, and the randomness of solutions generated from a given set of constraints. In this paper, we focus on the second problem, and present an algorithm that significantly improves the state-of-the-art of (almost-)uniform generation of solutions of large Boolean constraints. Our algorithm provides strong theoretical guarantees on the uniformity of generated solutions and scales to problems involving hundreds of thousands of variables.

arXiv commentThis is a full version of DAC 2014 paper

References in corpus (1)

• A Scalable Approximate Model Counter

Cited by in corpus (10)

• Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
• Sampling Techniques for Boolean Satisfiability
• Constrained Counting and Sampling: Bridging the Gap between Theory and Practice
• Combining the $k$-CNF and XOR Phase-Transitions
• Sound Probabilistic #SAT with Projection
• Beginner's Luck: A Language for Property-Based Generators
• Projected Model Counting: Beyond Independent Support
• Building Very Small Test Suites (with Snap)
• Faster SAT Solving for Software with Repeated Structures (with Case Studies on Software Test Suite Minimization)
• On Uniformly Sampling Traces of a Transition System (Extended Version)