GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
For the SAT solving community, this work provides a novel hybrid approach that significantly improves performance on satisfiable instances, though gains on unsatisfiable instances are modest.
GaloisSAT introduces a hybrid GPU-CPU SAT solver that combines differentiable SAT solving on GPUs with traditional CDCL solving on CPUs, achieving an 8.41X speedup on satisfiable instances and a 1.29X speedup on unsatisfiable instances over state-of-the-art solvers on SAT Competition 2024 benchmarks.
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.