用图神经网络一键指导求解器，让布尔可满足性求解快两倍以上
Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs
- 用GNN在一次前向计算中为所有变量分配优先级和取值方向
- 在多种问题上使求解时间平均缩短超2倍，且能泛化到更复杂问题
- 无需人工设计规则，直接从求解代价学习，适合优化领域研究者
布尔可满足性（SAT）求解器是计算机科学的基础，但其性能通常依赖手工设计的启发式策略。本文提出强化学习算法反馈（RLAF）范式，利用图神经网络（GNN）学习引导SAT求解器的分支启发式策略。核心是一种新颖且通用的机制，可将推断出的变量权重和极性注入现有求解器的分支策略中。在单次前向传播中，GNN为所有变量分配这些参数。将此一次性引导建模为强化学习问题，使我们能够使用现成的策略梯度方法（如GRPO），仅以求解器的计算成本作为奖励信号训练GNN。大量实验表明，经RLAF训练的策略显著降低了不同基础求解器在多样化SAT问题分布下的平均求解时间，在某些情况下实现超过2倍的加速，且在训练后对更大更难的问题具有良好的泛化能力。值得注意的是，这些策略持续优于基于手工设计加权启发式的专家监督方法，为组合优化中的数据驱动启发式设计提供了有前景的路径。
原文摘要 · Abstract (English)
Boolean Satisfiability (SAT) solvers are foundational to computer science, yet their performance typically hinges on hand-crafted heuristics. This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branching heuristics with Graph Neural Networks (GNNs). Central to our approach is a novel and generic mechanism for injecting inferred variable weights and polarities into the branching heuristics of existing SAT solvers. In a single forward pass, a GNN assigns these parameters to all variables. Casting this one-shot guidance as a reinforcement learning problem lets us train the GNN with off-the-shelf policy-gradient methods, such as GRPO, directly using the solver's computational cost as the sole reward signal. Extensive evaluations demonstrate that RLAF-trained policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than a 2x speedup in some cases, while generalizing effectively to larger and harder problems after training. Notably, these policies consistently outperform expert-supervised approaches based on learning handcrafted weighting heuristics, offering a promising path towards data-driven heuristic design in combinatorial optimization.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。