GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

TL;DR

GaloisSAT is a hybrid GPU-CPU SAT solver that combines differentiable machine learning techniques with traditional methods, achieving significant speedups over state-of-the-art solvers in benchmark tests.

Contribution

This paper introduces GaloisSAT, a novel differentiable SAT solver that integrates machine learning with classical algorithms, improving performance on standard benchmarks.

Findings

GaloisSAT achieves 8.41X speedup on satisfiable benchmarks.

GaloisSAT achieves 1.29X speedup on unsatisfiable benchmarks.

GaloisSAT outperforms leading solvers Kissat and CaDiCaL in SAT Competition 2024.

Abstract

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.