本研究将自我注意的图神经网络应用于基于 BP 的计数问题，成功地在产生概率接近于技术先进的问题解决器的解的同时，保证了模型性能的扩展性。

May, 2022

NeuroSAT 是一种信息传递神经网络，通过分类器训练来预测可满足性，在解决图着色、团检测、支配集和顶点覆盖等问题上具有较好的泛化性能。

Feb, 2018

利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

Sep, 2023

通过建立一个全面的评估框架，我们提出了第一个用于 GNN-based SAT solvers 的基准研究，对各种预测任务、训练目标和推理算法的广泛范围的 GNN 模型进行了基准测试，结果展示了 GNN-based SAT solvers 的性能以及现有模型在学习策略方面的局限性。

Sep, 2023

引入一种新的约束求解方法 NeuralSAT，用作深度神经网络 (DNN) 验证的符号化求解器。

Jul, 2023

提出了 IB-Net 框架，利用图神经网络和新颖的图编码技术来模拟不可满足问题，并与先进的求解器交互，以加速解决逻辑等效性检查工作流程，实验证明其平均运行时间提速了 5.0％（工业数据）和 8.3％（SAT 竞赛数据）。

Mar, 2024

本文介绍了使用改进的 NeuroSAT 架构，通过训练简化的神经网络来直接预测实际问题的不可满足核，以提供有效的指导高性能 SAT 求解器在解决特定问题分布时的问题上的应用。

Mar, 2019

我们介绍了一种神经符号证明型 SAT 求解器 NeuRes。与其他神经 SAT 求解方法不同，NeuRes 能够证明不可满足性而不仅仅是预测。通过使用命题证明来证明不可满足以及在不可满足和可满足公式的情况下加速找到满足真值分配的过程，NeuRes 以证书驱动的方式运行。为了实现这一点，我们提出了一种新颖的架构，该架构从图神经网络和指针网络中选择动态图结构的节点对，这对于生成解析证明至关重要。我们使用与 NeuroSAT 相同的随机公式分布编制了一组教师证明和真值分配的数据集，对我们的模型进行训练和评估。在实验中，我们展示了 NeuRes 在不同分布上比 NeuroSAT 解决更多的测试公式，而且数据效率更高。此外，我们还展示了 NeuRes 能够大大缩短教师证明的长度。我们利用这个特性设计了一种引导训练程序，在没有额外指导的情况下，成功将由高级求解器生成的证明数据集减少了约 23%。

Feb, 2024

通过三分图表示的实例和异构图神经网络模型，我们提出了一种基于 GraSS 的自动 SAT 求解器选择方法，该方法使用了特定领域决策，如新的节点特征设计、图中子句的位置编码、针对三分图的 GNN 架构以及运行时间敏感的损失函数，通过广泛的实验，我们证明了这种组合对于七种最先进的求解器来说在回路设计基准测试和 2022 SAT 大赛 20 年纪念赛道的实例中都能提高运行时间。

May, 2024

本论文提出了一种基于图神经网络的通用框架，可用于以完全无监督的方式通过能量最小化解决 CSP 问题，并通过在图模型中传播、减少和预测的方法学习搜索策略，从而比现有的神经网络和基线模型更有效地解决 SAT 问题。

Mar, 2019