High-Throughput SAT Sampling

TL;DR

This paper introduces a GPU-accelerated SAT sampling method that transforms SAT problems into differentiable multi-output functions, enabling faster sampling with significant runtime improvements over existing heuristics.

Contribution

The novel approach reinterprets SAT sampling as a differentiable regression task on circuit-structured problems, achieving substantial speedups.

Findings

Achieves 33.6x to 523.6x faster runtime than state-of-the-art heuristics.

Operates directly on circuit structures for efficient parallel processing.

Demonstrates superior performance on benchmark SAT instances.

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.