用可微代数方法加速布尔可满足性求解，显著提升求解效率。
GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
- 结合可微代数与传统CDCL算法，实现GPU加速的混合求解流程。
- 在可满足实例上快8.41倍，在不可满足实例上快1.29倍。
- 适合需要高速求解布尔逻辑问题的研究者与工程应用。
布尔可满足性（SAT）问题作为首个被证明为NP完全的问题，是计算复杂性中的核心挑战，广泛应用于优化与验证等领域。尽管过去二十年算法持续演进，但求解器性能提升缓慢：2025年竞赛冠军相比2006年仅提升约2倍。本文提出GaloisSAT，一种融合可微SAT求解引擎（基于有限域代数与现代机器学习框架）与传统CDCL求解阶段的混合式GPU-CPU SAT求解器。在SAT Competition 2024基准测试集上，GaloisSAT相较最新领先求解器Kissat与CaDiCaL，在官方指标PAR-2（超时5000秒，惩罚因子2）下取得显著进展：可满足类别提速8.41倍，不可满足类别提速1.29倍。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。