TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System

TL;DR

This work tackles accelerating Boolean SAT solving on heterogeneous GPU-CPU systems by reformulating SAT as a differentiable binarized matrix-multiplication task. It introduces a binary-minary matrix encoding with $P \in \{0,1\}^{C \times 2V}$ and $A \in \{0,1\}^{2V \times N}$, producing $R=PA$ and a differentiable $S$ via a soft minimum to drive a loss $\mathcal{L} = -\sum_i S_i$, with gradients flowing through a STE-enabled binarization of $A_{real}$. The solver runs a gradient-guided exploration on the GPU to propose promising partial assignments and then uses CDCL-based refinement on the CPU to complete solutions, seeded by high-confidence variables extracted from gradient magnitudes. Empirically, on satisfiable benchmarks from the 2024 SAT Competition, the approach achieves substantial speedups over CPU-only solvers (up to over $200\times$) and an average speedup of about $27.3\times$, validating the viability and value of GPU-accelerated differentiable SAT on hybrid hardware.

Abstract

While accelerated computing has transformed many domains of computing, its impact on logical reasoning, specifically Boolean satisfiability (SAT), remains limited. State-of-the-art SAT solvers rely heavily on inherently sequential conflict-driven search algorithms that offer powerful heuristics but limit the amount of parallelism that could otherwise enable significantly more scalable SAT solving. Inspired by neural network training, we formulate the SAT problem as a binarized matrix-matrix multiplication layer that could be optimized using a differentiable objective function. Enabled by this encoding, we combine the strengths of parallel differentiable optimization and sequential search to accelerate SAT on a hybrid GPU-CPU system. In this system, the GPUs leverage parallel differentiable solving to rapidly evaluate SAT clauses and use gradients to stochastically explore the solution space and optimize variable assignments. Promising partial assignments generated by the GPUs are post-processed on many CPU threads which exploit conflict-driven sequential search to further traverse the solution subspaces and identify complete assignments. Prototyping the hybrid solver on an NVIDIA DGX GB200 node, our solver achieves runtime speedups up to over 200x when compared to a state-of-the-art CPU-based solver on public satisfiable benchmark problems from the SAT Competition.

Figures (5)

• Figure 1: SAT problem in CNF with 4 variables and 5 clauses -- The problem is satisfiable because each clause has at least one satisfied (bold) literal.
• Figure 2: Binary matrix multiplication encoding for our differentiable SAT formulation -- Each row of the Problem Matrix encodes one corresponding CNF clause. Each column of the Assignment Matrix represents one candidate assignment being attempted. Each element in the Result Matrix indicates the number of literals that each candidate assignment satisfies in each clause. The Satisfiability Matrix indicates whether each assignment is satisfying all clauses.
• Figure 3: Computation graph of the binary matrix multiplication for SAT solving -- In the forward pass (solid arrows), the trainable weights are normalized and binarized prior to multiplication. In the backward pass (dash arrows), an identity function is used as a proxy for gradient propagation through the non-differentiable Binarization layer.
• Figure 4: Hybrid SAT solving on GPU-CPU system -- GPUs perform differentiable optimization on matrix-multiply units. CPUs leverage CDCL search on many threads to determine complete satisfying assignments.
• Figure 5: Cumulative performance curve -- Compares the number of solved problems for a given time limit between our solvers and baseline solvers.