Source-linked AI summary
SAT Sampling at Scale via GPU-based Boolean Constraint Propagation
Alexander Nadel, Yogev Shalmon, Ofer Strichman
TL;DR
Constrained-random verification needs many valid stimuli, including for scenarios random inputs rarely reach, while existing CPU SAT and GPU gradient samplers prioritize different strengths. Gpap-S uses GPU-based Boolean constraint propagation to explore many independent sampling trajectories, combining SAT-based robustness with GPU throughput. It outperforms the compared samplers across the reported target settings, and Gpap is also released as a reusable BCP library.
Problem
Existing CPU SAT samplers prioritize deductive power and GPU gradient samplers prioritize throughput, while constrained-random verification needs many valid stimuli that reach targeted scenarios.
Source: §1 · pp. 1–2Method
Gpap-S runs many independent decide-and-propagate trajectories in parallel on a GPU using Gpap, an engine that propagates partial assignments against a shared formula.
Source: §1 · pp. 2–3Results
83.4–1,571× faster than CMSGen across benchmarks, Gpap-S is also 2.2× faster than Demotic and 8.0–18.7× faster than Recurrent at their original evaluation targets.
Source: §1 · p. 3Takeaways & Limitations
Gpap is released as a reusable BCP library, and Gpap-S combines the rare-target robustness of SAT sampling with GPU throughput.
Source: §7 · p. 18The pipeline’s treatment of variable elimination is constrained because variable elimination can change the relevant property; CMSGen also turns it off.
Source: §5.2 · p. 13
Abstract
from arXiv · showhide
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.
1 Introduction
Constrained-random verification needs many valid, well-spread stimuli, including stimuli for rare corner cases. Gpap-S combines SAT-based propagation with GPU parallelism, and Gpap supplies a reusable engine for propagating many assignments concurrently.
1 Introduction
- Constrained-random verification samples legal stimuli that steer hardware tests toward useful scenarios, including corner cases that random inputs rarely reach.When constraints target design outputs, the formula also encodes the circuit, and a solution is a stimulus that drives it to the required outputs.Source: §1 · pp. 1–2
- Existing samplers prioritize different goals: CPU-based SAT samplers emphasize deductive power, while GPU gradient samplers emphasize throughput but can lose orders of magnitude at rare targets.Gradient samplers round continuous-search results to Boolean assignments, which count only when they satisfy the formula.Source: §1 · p. 2
- Gpap-S is the first GPU sampler built on SAT propagation, running thousands of independent decide-and-propagate trajectories concurrently and discarding trajectories that reach conflicts.Each completed trajectory yields a model by construction, without rounding or repair.Source: §1 · pp. 2–3
- Gpap-S is 83.4–1,571× faster than CMSGen across benchmarks, 2.2× faster than Demotic and 8.0–18.7× faster than Recurrent at their original targets, and roughly two orders faster than Recurrent at rare targets.Demotic fails to produce samples on most rare-target instances; under Barbarik, Gpap-S and CMSGen are accepted on every tested circuit instance.Source: §1 · p. 3
- Gpap is released as an open-source BCP library with C++ and Python interfaces, and its batched-propagation primitive also applies to probing, SAT sweeping, and look-ahead.Its clause-state design uses one 32-bit word per clause so literal falsification can be performed with one atomic instruction.Source: §1 · pp. 3–4
2 Preliminaries
The preliminaries define Boolean formulas, assignments, and propagation, then describe the GPU execution model that shapes the paper’s design. They also introduce projected sampling and the counter-and-key clause bookkeeping used for propagation.
2.1 SAT, Propagation, and Projected Sampling
- A CNF formula is a conjunction of clauses; under a partial assignment, a clause is satisfied, conflicting, or unit, with its sole free literal forced in every satisfying extension.BCP repeatedly asserts forced literals until no unit clause remains or a conflict occurs; for a given assignment, processing order does not change the fixpoint or whether conflict is reached.Source: §2.1 · p. 4
- Counter-and-key bookkeeping tracks each clause’s surviving-literal count and XOR of their indices, identifying conflict at zero survivors and the forced literal at one.Unlike two-watched literals, this scheme updates every clause containing the falsified literal and requires undoing updates when backtracking.Source: §2.1 · p. 5
- Projected sampling draws models’ restrictions to a designated support, while circuit benchmarks treat primary inputs across cycles as support and constrain final-cycle outputs to a target pattern.Rare targets are the least frequent patterns observed in a large simulation batch; they are reachable and therefore satisfiable by construction.Source: §2.1 · p. 5
2.2 The GPU Execution Model
- GPU throughput depends on keeping enough warps resident to hide memory latency, while compact per-job state helps fit more jobs concurrently.Warps execute groups of 32 lanes in lockstep; jobs occupy separate warps, limiting divergence interference across jobs.Source: §2.2 · pp. 5–6
3 Related Work
Prior work addresses sampling, propagation data structures, and GPU SAT in distinct ways. The related-work discussion positions Gpap’s counter-and-key bookkeeping and many-assignment propagation against those approaches.
3.1 Solution Sampling
- Almost-uniform SAT sampling with guarantees is expensive, requiring repeated SAT calls with random XOR constraints, d-DNNF compilation, or exact model counting; practical samplers instead target empirical uniform-like behavior and use testers such as Barbarik.CMSGen uses the term uniform-like for its practical distribution goal.Source: §3.1 · p. 6
3.2 BCP and Its Data Structures
- Gpap’s counter-and-key bookkeeping revives a scheme from NanoSAT and local search, and replaces XOR with a sum so counter and key can update together in one atomic.The earlier bookkeeping’s uniform, branch-free update suits parallel GPU clause-state maintenance.Source: §3.2 · p. 6
3.3 Propagation and SAT on GPU
- Most prior GPU propagation parallelizes one call or accelerates components around CPU-based BCP, and the cited SAT efforts do not report GPU BCP outperforming CPU two-watched literals.Turbo runs GPU propagation and backtracking for many constraint subproblems but fits only a few hundred at once; Gpap likewise keeps independent work in flight.Source: §3.3 · p. 7
4 The Gpap Engine
Gpap propagates many independent partial assignments to BCP fixpoint against one shared CNF formula, reporting conflicts or implied literals. Its design combines private per-job state with compact atomic clause bookkeeping and GPU execution across jobs and within each job.
4 The Gpap Engine
- Gpap independently propagates K partial assignments against a fixed CNF formula to fixpoint, reporting conflicts or implied literals for each assignment.It can also decide by choosing free variables, assigning them, and propagating.Source: §4 · p. 7
4.1 Jobs and the Shared Formula
- Each job is a partial assignment with private mutable state, while jobs share read-only formula data, including negated occurrence lists and initial clause state.Private state includes the assignment, trail, and per-clause counter and key.Source: §4.1 · pp. 7–8, Figure 1 · p. 8
4.2 How Many Jobs Fit
- On a 24 GB GPU, the example formula with 32,000 clauses uses 128 KB per job for clause bookkeeping, allowing on the order of 10^5 partial assignments per launch.The launch size is bounded by device memory and available warp residency; the implementation packs each clause’s counter and key into one 32-bit word.Source: §4.2 · pp. 8–9
4.3 The Sum-Packed Word
- A sum-packed word stores a clause’s counter and the sum of its surviving literal indices, so one atomic arithmetic update handles both when a literal is falsified.The returned prior word identifies whether the update caused a unit clause or conflict; atomic serialization ensures exactly one lane observes each transition.Source: §4.3 · pp. 9–10
4.4 The Assignment: One Bit per Literal
- The assignment bitmap uses one bit per literal, and an atomic OR both records a forced literal and detects whether its opposite polarity already causes a conflict.The two polarities of a variable occupy adjacent indices and therefore the same bitmap word.Source: §4.4 · p. 10
4.5 Two Kernels, One Propagation Core
- Gpap exposes separate kernels for propagation to fixpoint and for a complete randomized decide-and-propagate trajectory within one launch.For formulas below roughly 2,000 clauses, propagation instead runs serially within each warp; both variants reach the same fixpoint.Source: §4.5 · pp. 10–11
4.6 Using the Engine
- Gpap is released as a C library with C++ and Python interfaces, allowing users to check batches of partial assignments through an API call without GPU programming.The kernels are written in Triton and compiled ahead of time.Source: §4.6 · p. 11
5 Gpap-S: GPU-based SAT Sampling
Gpap-S samples projected solutions by running randomized decide-and-propagate trajectories in parallel, with preprocessing and online configuration selection built on Gpap. Its pipeline mines consequences, simplifies the formula while preserving projected solutions, and projects samples onto the support; Barbarik accepts it on all tested instances.
5 Gpap-S: GPU-based SAT Sampling
- Gpap-S uses Gpap to sample projected solutions from a CNF formula and support by running many independent randomized decide-and-propagate trajectories.The pipeline also uses Gpap for preprocessing and online configuration selection.Source: §5 · p. 11, §5.2 · p. 12
5.1 The Sampling Algorithm
- A trajectory decides support variables first, propagates to fixpoint, and is discarded on conflict; a completed model yields a sample restricted to the support.For circuits, primary inputs determine the remaining variables, so no decisions beyond the support are needed.Source: §5.1 · p. 11
5.2 The Sampling Pipeline
- Mining probes support-literal sets for entailed backbone, binary, and ternary clauses in parallel, retaining mined clauses only when a warm-up run completes more trajectories.Probes test single literals, then pairs and triples as the fixed time budget allows.Source: §5.2 · p. 12
- Simplification asserts units and substitutes equivalent literals while preserving the projected solution set exactly; variable elimination can change that set.Substitutions are recorded so samples can be reconstructed at readout.Source: §5.2 · pp. 12–13
- Gpap-S chooses online between circuit configurations using throughput after one full launch per configuration, with random order and B = 8 or B = 1 as the options.Each launch measures K independent trajectories for that configuration.Source: §5.2 · p. 13
5.3 Using Gpap-S
- The output contains one row per sample over the support, projected on the GPU so the full assignment does not leave the device.The command accepts CNF or circuit inputs and stops at the requested sample count or time limit.Source: §5.2 · p. 13, §5.3 · p. 13
5.4 Sample Uniformity
- Barbarik accepts Gpap-S on all 65 tested instances, as it does CMSGen under the same test.The 65-instance set comprises cases where Barbarik terminates and accepts the reference sampler Spur.Source: §5.4 · p. 13
6 Experimental Evaluation
The evaluation compares Gpap-S with CMSGen and GPU gradient samplers on circuit benchmarks at original and rare targets. It finds strong throughput advantages, with the size of the advantage shaped by target rarity and work per sample.
6.1 Benchmarks and Protocol
- The benchmarks include 11 ISCAS-85 and 30 sequential circuits, tested at original and rare targets; sequential circuits are evaluated at T = 25 and 50.The protocol gives Gpap-S and CMSGen a 60-second sampling budget; geometric means exclude instances that do not measure sampling and instances where neither sampler emits.Source: §6.1 · pp. 14–15
6.2 Comparison against CMSGen
- 83.4–1,571×: Gpap-S is faster than CMSGen in steady state across all benchmark rows, and 31.0–494× faster end to end.Gpap-S delivered all 50,000 requested samples within budget on 93 of 110 unfiltered instances, compared with 44 for CMSGen.Source: §6.2 · p. 15, Table 1 · p. 15
- End to end, Gpap-S’s speedup is a quarter to a half of its steady-state speedup because preparation takes a median 33–67% of wall time on these rows.Because preparation is a fixed cost, larger sample requests move the end-to-end speedup toward the steady-state speedup.Source: §6.2 · pp. 15–16
6.3 Comparison against the GPU Gradient Samplers
- At original targets, Gpap-S is 2.2× faster than Demotic and 18.7× and 8.0× faster than Recurrent at T = 25 and 50; at rare targets, its speedups over Recurrent rise to 147× and 84.7×.At rare targets, Demotic produces no solution on five of seven instances and is over five orders of magnitude slower on the other two; Recurrent fails to initialize on four instances at T = 25 and nine at T = 50.Source: §6.3 · pp. 16–17, Table 2 · p. 17
6.4 Where the Speed Comes From
- Gpap-S sustains 1.59 × 10^9 to 2.27 × 10^9 implications per second, while target-dependent work per sample explains the spread in its speedups.Its propagation-rate geometric mean is 568× CMSGen’s; at rare sequential targets, Gpap-S spends 6.41× and 6.59× CMSGen’s work per sample at T = 25 and 50, respectively.Source: §6.4 · pp. 17–18, Table 3 · p. 18
7 Conclusion
The conclusion presents Gpap-S, built on the general-purpose BCP engine Gpap, as bringing GPU throughput to SAT-based sampling. It identifies potential uses for Gpap beyond sampling and notes that both tools are open source under the MIT license.
7 Conclusion
- Gpap-S uses Gpap to propagate many independent partial assignments concurrently against one shared formula.The conclusion frames this as bringing the rare-target robustness of SAT-based sampling to GPU throughput; conflicting trajectories are discarded rather than learned from.Source: §7 · p. 18
- Gpap performs two to three orders of magnitude more implications per second on one GPU than a CDCL solver on one CPU core.The paper expects Gpap to be useful for probing, SAT sweeping, look-ahead, preprocessors, model checkers, and test generators.Source: §7 · p. 18
Data Availability Statement
- Gpap-S and Gpap are open source under the MIT license.The paper gives their repository location in its Data Availability Statement.Source: Data Availability Statement · p. 18