学习排序SAT求解器的初始分支顺序
人工智能
2026-03-10 v1 计算机科学中的逻辑
摘要
找到好的分支顺序是高效求解SAT问题的关键，但找到这样的分支顺序本身是一个难题。因此，在求解之前使用基于学习的方法预测一个好的分支顺序具有潜力。在本文中，我们研究使用图神经网络作为冲突驱动子句学习（CDCL）SAT求解器的预处理步骤来预测分支顺序。我们表明，通过提供良好的初始分支，现有的CDCL SAT求解器可以获得显著的性能提升。此外，我们提供了三种标记方法，以可处理的方式找到这样的初始分支顺序。最后，我们训练一个图神经网络来预测这些分支顺序，并通过我们的评估表明，GNN初始化的顺序在随机3-CNF和伪工业基准测试上产生了显著的加速，并且具有泛化到远大于训练集实例的能力。然而，我们也发现这些预测未能加速更困难和工业化的实例。我们将此归因于求解器的动态启发式策略，该策略会迅速覆盖提供的初始化，以及这些实例的复杂性，使得GNN预测变得困难。
引用
@article{arxiv.2603.07176,
title = {Learning to Rank the Initial Branching Order of SAT Solvers},
author = {Arvid Eriksson and Gabriel Poesia and Roman Bresson and Karl Henrik Johansson and David Broman},
journal= {arXiv preprint arXiv:2603.07176},
year = {2026}
}
备注
Published at VerifAI-2: The Second Workshop on AI Verification in the Wild