# GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 30 references that are in the map.
- First posted on arXiv 25 Mar 2026.

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

- [Categorical Reparameterization with Gumbel-Softmax](https://mlsanity.com/paper/1611.01144/) (2016)
- [The Concrete Distribution: A Continuous Relaxation of Discrete Random Variables](https://mlsanity.com/paper/1611.00712/) (2016)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints](https://mlsanity.com/paper/1912.01032/) (2019)
- [Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs](https://mlsanity.com/paper/2308.15020/) (2023)
- [HordeSat: A Massively Parallel Portfolio SAT Solver](https://mlsanity.com/paper/1505.03340/) (2015)
- [TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System](https://mlsanity.com/paper/2511.07737/) (2025)

## Abstract (arXiv)

Boolean satisfiability (SAT) problem, the first problem proven to be NP-complete, has become a fundamental challenge in computational complexity, with widespread applications in optimization and verification across many domains. Despite significant algorithmic advances over the past two decades, the performance of SAT solvers has improved at a limited pace. Notably, the 2025 competition winner shows only about a 2X improvement over the 2006 winner in SAT Competition performance after nearly 20 years of effort. This paper introduces GaloisSAT, a novel hybrid GPU-CPU SAT solver that integrates a differentiable SAT solving engine powered by modern machine learning infrastructure on GPUs, followed by a traditional CDCL-based SAT solving stage on CPUs. GaloisSAT is benchmarked against the latest versions of state-of-the-art solvers, Kissat and CaDiCaL, using the SAT Competition 2024 benchmark suite. Results demonstrate substantial improvements in the official SAT Competition metric PAR-2 (penalized average runtime with a timeout of 5,000 seconds and a penalty factor of 2). Specifically, GaloisSAT achieves an 8.41X speedup in the satisfiable category and a 1.29X speedup in the unsatisfiable category compared to the strongest baselines.