# Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs

arXiv: https://arxiv.org/abs/2308.15020 · HTML: https://mlsanity.com/paper/2308.15020/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 59 references that are in the map.
- First posted on arXiv 29 Aug 2023.

## Builds on (most cited first, 9 of 9)

- [Automatic differentiation in machine learning: a survey](https://mlsanity.com/paper/1502.05767/) (2015)
- [In-Datacenter Performance Analysis of a Tensor Processing Unit](https://mlsanity.com/paper/1704.04760/) (2017)
- [Efficient and Modular Implicit Differentiation](https://mlsanity.com/paper/2105.15183/) (2021)
- [Non-convex Optimization for Machine Learning](https://mlsanity.com/paper/1712.07897/) (2017)
- [A Regularized Framework for Sparse and Structured Neural Attention](https://mlsanity.com/paper/1705.07704/) (2017)
- [FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints](https://mlsanity.com/paper/1912.01032/) (2019)
- [On Continuous Local BDD-Based Search for Hybrid SAT Solving](https://mlsanity.com/paper/2012.07983/) (2020)
- [A Scalable Shannon Entropy Estimator](https://mlsanity.com/paper/2206.00921/) (2022)
- [Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints](https://mlsanity.com/paper/2301.09833/) (2023)

## Built on by (most cited first, 8 of 8)

- [TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System](https://mlsanity.com/paper/2511.07737/) (2025)
- [Analysis of Higher-Order Ising Hamiltonians](https://mlsanity.com/paper/2412.13489/) (2024)
- [Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization](https://mlsanity.com/paper/2506.00674/) (2025)
- [FourierCSP: Differentiable Constraint Satisfaction Problem Solving by Walsh-Fourier Expansion](https://mlsanity.com/paper/2510.04480/) (2025)
- [GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra](https://mlsanity.com/paper/2603.28796/) (2026)
- [Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver](https://mlsanity.com/paper/2606.06641/) (2026)
- [A Study of Parallel Continuous Local Search](https://mlsanity.com/paper/2606.06656/) (2026)
- [XLOG: A CUDA-Native Engine for Neurosymbolic Integration](https://mlsanity.com/paper/2609.27203/) (2026)

## Abstract (arXiv)

Although state-of-the-art (SOTA) SAT solvers based on conflict-driven clause learning (CDCL) have achieved remarkable engineering success, their sequential nature limits the parallelism that may be extracted for acceleration on platforms such as the graphics processing unit (GPU). In this work, we propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search (CLS). This is realized by a novel parallel algorithm inspired by the Fast Fourier Transform (FFT)-based convolution for computing the elementary symmetric polynomials (ESPs), which is the major computational task in previous CLS methods. The complexity of our algorithm matches the best previous result. Furthermore, the substantial parallelism inherent in our algorithm can leverage the GPU for acceleration, demonstrating significant improvement over the previous CLS approaches. We also propose to incorporate the restart heuristics in CLS to improve search efficiency. We compare our approach with the SOTA parallel SAT solvers on several benchmarks. Our results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes implemented on CPU. Moreover, FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.