Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

Curie Kim, Carsten Portner, Mingju Liu, Steve Dai, Haoxing Ren, Brucek Khailany, Alvaro Velasquez, Ismail Alkhouri, Cunxi Yu

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.

GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

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.

Paper Structure

This paper contains 27 sections, 1 theorem, 19 equations, 4 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Methodology
  3. GaloisSAT Architecture Overview
  4. Differentiable SAT Formulation
  5. Differentiable SAT Encoding via Finite Field Algebra
  6. Gradient-based Optimization with Gumbel-Softmax
  7. Clause Normalization for Vectorization
  8. GaloisSAT Solving Flow
  9. Partial Assignment Extraction for SAT Instances
  10. Sampling via Multiple Gumbel Perturbations
  11. Confidence-guided Partial Assignment Encoding
  12. Guided Branching for UNSAT Instances
  13. Parallel Symbolic Solving on CPUs
  14. Experiments
  15. SAT Performance against SOTA Solvers
  16. ...and 12 more sections

Key Result

Lemma 1

If $\varphi(x_1, \dots, x_n)$ is a CNF formula and let $S = \{i_1, \dots, i_d\} \subseteq \{1, \dots, n\}$ be any subset of $d$ variables, then where $\ell_{i_r}^{(1)} := x_{i_r}$, $\ell_{i_r}^{(0)} := \lnot x_{i_r}$, and $\varphi\!\upharpoonright_{\mathbf{x}_S=\alpha}$ is the restriction of $\varphi$ under the assignment $\mathbf{x}_S = \alpha$. If all subformulas $\varphi\!\upharpoonright_{\mat

Figures (4)

  • 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.
  • 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.

Theorems & Definitions (1)

  • Lemma 1