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.

This is a full version of DAC 2014 paper

Cited by in corpus (6)

• Sampling Techniques for Boolean Satisfiability
• Combining the $k$-CNF and XOR Phase-Transitions
• Sound Probabilistic #SAT with Projection
• Projected Model Counting: Beyond Independent Support
• On Uniformly Sampling Traces of a Transition System (Extended Version)
• Faster SAT Solving for Software with Repeated Structures (with Case Studies on Software Test Suite Minimization)