用胶合变量预测增强 SAT 求解器

现代 SAT 求解器常规运行的规模使得为每一次分支决策查询神经网络变得不切实际。Selsam 与 Bjorner 提出的 NeuroCore 提供了一个概念验证,表明神经网络仍可通过仅周期性地重新聚焦基于分数的分支启发式来加速 SAT 求解器。然而,该工作存在若干局限:其修改的求解器需要 GPU 加速;进一步消融实验表明在 SATCOMP 2018 基准上它们不优于随机基线;且其训练目标——unsat 核心——需要昂贵的数据管线,仅能标注相对容易的不满足问题。我们解决了所有这些局限,使用更简单的网络架构,即便对含数百万子句的大型工业问题也允许 CPU 推理,并改为训练预测{\em 胶合变量(glue variables)}——一个更易生成标注数据且可表述为强化学习任务的训练目标。我们通过修改最先进的 SAT 求解器 CaDiCaL 证明了方法的有效性:在 SATCOMP 2018 与 SATRACE 2019 上用监督学习提升其性能,并在 SHA-1 原像攻击数据集上用强化学习提升其性能。