基于算法反馈的学习：使用GNN实现单次SAT求解器指导
机器学习
2025-05-23 v1
摘要
布尔满足问题（SAT）求解器是计算机科学的基石，但其性能通常取决于手工制作的启发式方法。本工作引入基于算法反馈的强化学习（RLAF）作为一种范式，用于使用图神经网络（GNN）学习指导SAT求解器分支启发式方法。我们方法的核心是一种新颖且通用的机制，用于将推断得到的变量权重和极性注入到现有SAT求解器的分支启发式方法中。在单次前向传递中，GNN为所有变量分配这些参数。将这种单次指导作为强化学习问题处理，使我们能够直接使用求解器的计算成本作为唯一奖励信号，通过诸如GRPO等标准策略梯度方法训练GNN。广泛的评估表明，RLAF训练的策略在不同基准求解器跨越多样化SAT问题分布的平均求解时间显著降低，某些情况下实现了2倍以上的加速，同时在训练后对更大更难的问题具有良好的泛化能力。值得注意的是，这些策略一致地优于基于学习手工制作加权启发式方法的专家监督方法，为Combinatorial优化中的数据驱动启发式设计开辟了可前景的道路。
引用
@article{arxiv.2505.16053,
title = {Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs},
author = {Jan Tönshoff and Martin Grohe},
journal= {arXiv preprint arXiv:2505.16053},
year = {2025}
}