Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

High-Throughput SAT Sampling

Arash Ardakani, Minwoo Kang, Kevin He, Qijing Huang, John Wawrzynek

TL;DR

Problem addressed: the need for high-throughput, diverse SAT sampling to aid verification and testing workflows. Approach: transform CNF into a simplified multi-level, multi-output Boolean function and optimize using gradient descent on probabilistic logic operators, enabling data-parallel sampling on GPUs. Key contributions: (i) a general CNF-to-circuit transformation, (ii) a differentiable, GPU-enabled sampling pipeline, and (iii) experimental validation showing speedups from $33.6\times$ to $523.6\times$ over leading solvers on 60 instances. Significance: demonstrates a scalable path to high-throughput SAT sampling that can operate directly on circuit-like representations and high-level formats.

Abstract

In this work, we present a novel technique for GPU-accelerated Boolean satisfiability (SAT) sampling. Unlike conventional sampling algorithms that directly operate on conjunctive normal form (CNF), our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions. It then leverages gradient-based optimization to guide the search for a diverse set of valid solutions. Our method operates directly on the circuit structure of refactored SAT instances, reinterpreting the SAT problem as a supervised multi-output regression task. This differentiable technique enables independent bit-wise operations on each tensor element, allowing parallel execution of learning processes. As a result, we achieve GPU-accelerated sampling with significant runtime improvements ranging from $33.6\times$ to $523.6\times$ over state-of-the-art heuristic samplers. We demonstrate the superior performance of our sampling method through an extensive evaluation on $60$ instances from a public domain benchmark suite utilized in previous studies.

High-Throughput SAT Sampling

TL;DR

Problem addressed: the need for high-throughput, diverse SAT sampling to aid verification and testing workflows. Approach: transform CNF into a simplified multi-level, multi-output Boolean function and optimize using gradient descent on probabilistic logic operators, enabling data-parallel sampling on GPUs. Key contributions: (i) a general CNF-to-circuit transformation, (ii) a differentiable, GPU-enabled sampling pipeline, and (iii) experimental validation showing speedups from to over leading solvers on 60 instances. Significance: demonstrates a scalable path to high-throughput SAT sampling that can operate directly on circuit-like representations and high-level formats.

Abstract

In this work, we present a novel technique for GPU-accelerated Boolean satisfiability (SAT) sampling. Unlike conventional sampling algorithms that directly operate on conjunctive normal form (CNF), our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions. It then leverages gradient-based optimization to guide the search for a diverse set of valid solutions. Our method operates directly on the circuit structure of refactored SAT instances, reinterpreting the SAT problem as a supervised multi-output regression task. This differentiable technique enables independent bit-wise operations on each tensor element, allowing parallel execution of learning processes. As a result, we achieve GPU-accelerated sampling with significant runtime improvements ranging from to over state-of-the-art heuristic samplers. We demonstrate the superior performance of our sampling method through an extensive evaluation on instances from a public domain benchmark suite utilized in previous studies.

Paper Structure

This paper contains 12 sections, 10 equations, 4 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. SAT Sampling
  4. Multi-Output Regression Task
  5. Methodology
  6. Transformation Algorithm
  7. Experimental Results
  8. Runtime Performance
  9. Learning Dynamics
  10. Ablation Study
  11. Related Work
  12. Conclusion

Figures (4)

  • Figure 1: The overall workflow of our sampling approach is illustrated including (a) a CNF example with comments highlighted in green, (b) its simplified multi-level, multi-output Boolean function in a circuit form for illustrative purposes with unconstrained and constrained paths highlighted in blue and red, respectively, and (c) its corresponding PyTorch description.
  • Figure 2: A log-log plot showing the runtime in milliseconds versus the number of unique satisfying solutions across all $60$ instances from the sampling benchmark. The dotted lines represent the performance trends for each sampler.
  • Figure 3: (Left) Learning curve showing the number of unique satisfying solutions over iterations. (Right) Log-log plot of GPU memory usage (MB), measured by "nvidia-smi", across different batch sizes for a subset of $4$ CNF instances.
  • Figure 4: Comparison of GPU speedup over CPU (left), reduction rate of bit-wise operations in $2$-input gate equivalents (middle), and transformation time from CNF to a simplified multi-level, multi-output Boolean function (right) for a subset of $4$ instances.