GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

• URL: http://arxiv.org/abs/2603.28796v1
• Date: Wed, 25 Mar 2026 19:06:06 GMT
• Title: GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
• Abstract summary: This paper introduces GaloisSAT, a novel hybrid GPU- CPU SAT solver.<n>Results demonstrate substantial improvements in the official SAT Competition metric PAR-2.<n>GaloisSAT achieves an 8.41X speedup in the satisfiable category and a 1.29X speedup in the unsatisfiable category.
• Score: 17.171285034317087
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System [7.530665570222049]
  State-of-the-art satisfiability solvers rely heavily on inherently sequential conflict-driven search algorithms.<n>Inspired by neural network training, we formulate the SAT problem as a binarized matrix-matrix multiplication layer.<n>We combine the strengths of parallel differentiable optimization and sequential search to accelerate SAT on a hybrid GPU- CPU system.
  arXiv  Detail & Related papers  (2025-11-11T01:41:40Z)
• Deeply Optimizing the SAT Solver for the IC3 Algorithm [0.23749905164931204]
  We introduce several optimizations for the SAT solver in IC3 based on our observations.<n>We replace the binary heap with buckets to achieve constant-time operations.<n>We develop a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations.
  arXiv  Detail & Related papers  (2025-01-24T12:40:43Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  We present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances. We enrich the graph representation with domain-specific decisions, such as novel node feature design. We demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime.
  arXiv  Detail & Related papers  (2024-05-17T18:00:50Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
  arXiv  Detail & Related papers  (2023-06-07T12:19:22Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  This paper introduces SATformer, a Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.
  arXiv  Detail & Related papers  (2022-09-02T11:17:39Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks [13.185943308470286]
  Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs) This paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts.
  arXiv  Detail & Related papers  (2021-10-26T22:08:22Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• A Time Leap Challenge for SAT Solving [30.519940269088956]
  We compare 20-year-old SAT-solvers on new computer hardware with modern SAT-solvers on 20-year-old hardware. Our findings show that the progress on the algorithmic side has at least as much impact as the progress on the hardware side.
  arXiv  Detail & Related papers  (2020-08-05T16:33:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.