The Boolean Satisfiability problem (SAT) is the most prototypical NP-complete problem and of great practical relevance. One important class of solvers for this problem are stochastic local search (SLS) algorithms that iteratively and randomly update a candidate assignment. Recent breakthrough results in theoretical computer science have established sufficient conditions under which SLS solvers are guaranteed to efficiently solve a SAT instance, provided they have access to suitable "oracles" that provide samples from an instance-specific distribution, exploiting an instance's local structure. Motivated by these results and the well established ability of neural networks to learn common structure in large datasets, in this work, we train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers, allowing them, on average, to solve 17% more difficult instances (as measured by the ratio between clauses and variables), and to do so in 35% fewer steps, with improvements in the median number of steps of up to a factor of 8. As such, this work bridges formal results from theoretical computer science and practically motivated research on deep learning for constraint satisfaction problems and establishes the promise of purpose-trained SAT solvers with performance guarantees.

翻译：布尔可满足性问题（SAT）是最典型的NP完全问题，具有重要的实际意义。解决该问题的一类重要求解器是随机局部搜索（SLS）算法，这类算法通过迭代随机更新候选赋值来求解。理论计算机科学领域的最新突破性成果已建立了充分条件，在此条件下，若能访问合适的"预言机"（oracle）——即利用实例局部结构从实例特定分布中提供样本——则SLS求解器保证能高效求解SAT实例。受这些成果以及神经网络在大型数据集中学习共同结构的成熟能力启发，本研究采用图神经网络（GNN）训练预言机，并在两种SLS求解器上对难度各异的随机SAT实例进行评估。我们发现，基于GNN的预言机显著提升了两种求解器的性能：平均而言，它们能解决难度（以子句数与变量数之比衡量）高出17%的实例，求解步数减少35%，中位数求解步数改进幅度最高达8倍。因此，本研究在理论计算机科学的形式化结果与面向实践的约束满足问题深度学习研究之间架起桥梁，确立了具有性能保证的专用训练SAT求解器的应用前景。