基于图网络的 Q 学习能否为 SAT 求解器学习到可泛化的分支启发式
机器学习
2020-11-26 v2 人工智能
摘要
我们提出 Graph--SAT，一种用于布尔 SAT 求解器的分支启发式，其使用基于价值的强化学习（RL）进行训练，并以图神经网络作为函数近似器。使用 Graph--SAT 的求解器是完备的 SAT 求解器，能够提供满足赋值或不可满足性证明，而这正是许多 SAT 应用所需要的。SAT 求解器中常用的分支启发式在预热阶段会做出糟糕的决策，而 Graph--SAT 经过训练可审视特定问题实例的结构，从而在搜索早期做出更好的决策。训练 Graph--SAT 数据高效，且不需要繁琐的数据集准备或特征工程。我们使用与 MiniSat 求解器交互的 RL 训练 Graph--SAT，并表明 Graph--SAT 可将求解 SAT 问题所需的迭代次数减少 2-3 倍。此外，它能泛化到不可满足的 SAT 实例，以及变量数量比训练时多 5 倍的问题。我们表明对于更大的问题，迭代次数的减少会带来挂钟时间的减少，这正是设计启发式时的最终目标。我们还展示了在不同于训练所用任务族上测试 Graph--SAT 时的正向零样本迁移行为。虽然还需更多工作以将 Graph--SAT 应用于减少现代 SAT 求解环境中的挂钟时间，但它是一个令人信服的概念验证，表明配备图神经网络的 RL 能够学习到用于 SAT 搜索的可泛化分支启发式。
引用
@article{arxiv.1909.11830,
title = {Can $Q$-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?},
author = {Vitaly Kurin and Saad Godil and Shimon Whiteson and Bryan Catanzaro},
journal= {arXiv preprint arXiv:1909.11830},
year = {2020}
}
备注
Camera-ready for NeurIPS 2020