GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

arXiv cs.AI / 4/1/2026

💬 OpinionIdeas & Deep AnalysisTools & Practical UsageModels & Research

共有:

Key Points

The paper presents GaloisSAT, a hybrid GPU-CPU SAT solver that combines a differentiable SAT-solving engine running on GPUs with a conventional CDCL-based solving stage on CPUs.
It uses modern machine-learning infrastructure to make the SAT-solving process differentiable, then leverages finite-field (Galois field) algebra as part of the approach.
Benchmarked on the SAT Competition 2024 benchmark suite against leading solvers Kissat and CaDiCaL, GaloisSAT improves the official PAR-2 metric under a 5,000-second timeout.
Reported gains include an 8.41× speedup on satisfiable instances and a 1.29× speedup on unsatisfiable instances versus the strongest baselines.
The authors position the work as addressing the historically slow performance gains of SAT solvers, which have shown limited multi-decade improvement relative to earlier competition winners.

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.