GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
Authors: Curie Kim, Carsten Portner, Mingju Liu, Steve Dai, Haoxing Ren, Brucek Khailany, Alvaro Velasquez, Ismail Alkhouri, Cunxi Yu
Organizations: University of Maryland, College Park, MD, USA. · NVIDIA Research, Santa Clara, CA, USA. · NVIDIA Research, Austin, TX, USA. · University of Colorado Boulder, Boulder, CO, USA. · University of Michigan,Ann Arbor, MI, USA. · NVIDIA Research, College Park, MD, USA.
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.
Figures & tables
Figure 1: Overview of GaloisSAT architecture and solving flow. (a) GPU Module . Preprocessing and the forward pass for clause evaluation are indicated by solid arrows, while dashed arrows denote backpropagation enabling gradient-based optimization. (b) CPU Module . Parallel CDCL solving, using high-confidence partial assignments for SAT and branching on low-confidence variables for UNSAT to guarantee completeness.
Figure 2: Performance comparison between baseline solvers Kissat , CaDiCaL and their Galois -augmented variants, as well as TurboSAT(CaDiCaL) , on the 179 satisfiable instances from the SAT Competition 2024 dataset. *Note that the PAR-2 scores for GaloisSAT account for the total end-to-end runtime of the entire GPU+CPU solving flow.
Figure 3: Distribution of speedups on satisfiable instances from the SAT Competition 2024 benchmarks. Both (a) GaloisSAT(Kissat) and (b) GaloisSAT(CaDiCaL) achieve substantial improvements on over 70% of the instances.
Solver
Avg. PAR-2 ↓
Solved
Solved Rate
GaloisSAT(Kissat)
174.79
179 /179
100.0%
Kissat
1470.60
157/179
87.7%
GaloisSAT(CaDiCaL)
457.76
174 /179
97.2%
TurboSAT(CaDiCaL)
972.28
165/179
92.2%
CaDiCaL
2076.91
148/179
82.7%
Table 1: Performance comparison with SOTA SAT solvers.
Table 2: Top satisfiable instances showing the largest runtime reductions achieved by GaloisSAT . Both GaloisSAT(Kissat) and GaloisSAT(CaDiCaL) deliver substantial gains, frequently exceeding two-digit speedups and reaching up to three orders of magnitude compared to their backbone solvers. In most cases, GaloisSAT(CaDiCaL) also surpasses TurboSAT(CaDiCaL) . Entries marked as TO indicate timeouts.
Figure 4: Performance comparison between baseline solvers Kissat , CaDiCaL and their Galois -augmented variants on the 214 unsatisfiable instances from the SAT Competition 2024 dataset. *Note that the PAR-2 scores for GaloisSAT account for the total end-to-end runtime of the GPU+CPU solving flow.
# GPUs
Batch
Avg. Load (s)
Avg. Train (s)
Avg. Total GPU (s)
2×A100
500
1.39
9.03
10.42
1,000
1.29
17.90
19.19
3,000
1.46
52.31
53.77
8×A100
3,000
3.45
15.24
18.69
Table 3: Average GPU runtime on the SAT instances from the SAT Competition 2024 benchmarks across different hardware configurations and training settings.
Solver
Batch
Avg. PAR-2 ↓
Solved
Solved Rate
GaloisSAT(Kissat)
3,000
174.79
179/179
100.0%
1,000
229.77
178/179
99.4%
500
241.68
178/179
99.4%
GaloisSAT(CaDiCaL)
3,000
457.76
174/179
97.2%
1,000
367.50
176/179
98.3%
500
394.98
175/179
97.8%
Table 4: End-to-end solver performance across different batch sizes, along with baseline results. All Galois -enhanced solvers were trained using 2 × A100 GPUs with a number of epochs of 10.
Result Type
Proportion (%)
Satisfiable (succeeded partial assignments)
78.58
Timeout
15.44
Unsatisfiable (failed partial assignments)
5.59
Unknown
0.34
Table 5: Candidate pool quality for 100 generated candidates per satisfiable instance (179 instances) from the SAT Competition 2024 dataset, evaluated using Kissat . Each result type shows the proportion of candidates under this configuration.
Department of Computer Science The University of British Columbia Vancouver, Canada · Department of Earth, Ocean and Atmospheric Sciences The University of British Columbia Vancouver, Canada