SAT Sampling at Scale via GPU-based Boolean Constraint Propagation

Overview & Synopsis

Constrained-random verification tests hardware designs by sampling solutions of Boolean formulas. Existing samplers largely follow one of two approaches: CPU-based SAT samplers (e.g., CMSGen), which remain effective even at rare targets but offer limited throughput, and GPU-based gradient samplers, which achieve high throughput at high-probability targets but collapse at rare ones. We introduce Gpap-S, the first GPU sampler built on Boolean constraint propagation (BCP). At its core is Gpap, a new GPU engine for BCP that efficiently propagates many independent partial assignments concurrently on a shared Boolean formula. This capability allows Gpap-S to combine the rare-target robustness of SAT-based sampling with the throughput of GPU parallelism by exploring thousands of decide-and-propagate trajectories simultaneously. On the benchmark families used to evaluate prior GPU gradient samplers, Gpap-S is 2.2-18.7x faster at the high-probability targets considered in those evaluations. At rare targets, where those samplers often fail to generate any samples, Gpap-S achieves a geometric-mean speedup of roughly two orders of magnitude. Across all benchmarks, Gpap-S is also 83.4-1,571x faster than the CPU-based CMSGen. This throughput does not come at the expense of sample quality: under Barbarik, the statistical tester used to evaluate CMSGen, Gpap-S is accepted on every instance we test, as is CMSGen. We release Gpap as a reusable GPU library for high-throughput BCP.