利用不可满足核心预测指导高性能 SAT 求解器
提出了一种新方法来提升用于求解逻辑可满足性问题（SAT）的 NeuroCore 算法，此方法使用简化的神经网络架构作为分支启发式算法预测目标，而训练目标则是预测黏合变量，证明了该方法比其他方法更加有效。
Jul, 2020
我们介绍了一种神经符号证明型 SAT 求解器 NeuRes。与其他神经 SAT 求解方法不同，NeuRes 能够证明不可满足性而不仅仅是预测。通过使用命题证明来证明不可满足以及在不可满足和可满足公式的情况下加速找到满足真值分配的过程，NeuRes 以证书驱动的方式运行。为了实现这一点，我们提出了一种新颖的架构，该架构从图神经网络和指针网络中选择动态图结构的节点对，这对于生成解析证明至关重要。我们使用与 NeuroSAT 相同的随机公式分布编制了一组教师证明和真值分配的数据集，对我们的模型进行训练和评估。在实验中，我们展示了 NeuRes 在不同分布上比 NeuroSAT 解决更多的测试公式，而且数据效率更高。此外，我们还展示了 NeuRes 能够大大缩短教师证明的长度。我们利用这个特性设计了一种引导训练程序，在没有额外指导的情况下，成功将由高级求解器生成的证明数据集减少了约 23%。
Feb, 2024
介绍了一种名为 NSNet 的神经网络模型，通过使用一种新型的图神经网络 (GNN) 在潜在空间中对 BP 进行参数化，可以灵活配置以解决 SAT 和 #SAT 问题。
Nov, 2022
AsymSAT 是一种基于 GNN 的架构，能够扩展 GNN-based 方法的解题能力，改善 SAT 问题求解的性能，并通过使用生成的相关预测来维护变量之间的依赖关系。
Apr, 2023
本文介绍了一种结合 solution prediction model 和神经网络的方法 ——NLocalSAT，用于提高 stochastic local search 在解 Boolean satisfiability problem 时的有效性，并且在 SAT Competition 2018 的实验中取得了 27% ~ 62% 的性能提升。
Jan, 2020
通过三分图表示的实例和异构图神经网络模型，我们提出了一种基于 GraSS 的自动 SAT 求解器选择方法，该方法使用了特定领域决策，如新的节点特征设计、图中子句的位置编码、针对三分图的 GNN 架构以及运行时间敏感的损失函数，通过广泛的实验，我们证明了这种组合对于七种最先进的求解器来说在回路设计基准测试和 2022 SAT 大赛 20 年纪念赛道的实例中都能提高运行时间。
May, 2024
本文提出了 SATformer，一种基于 Transformer 的布尔满足性（SAT）求解方法，实现通过学习不可满足问题实例的最小不满足核（MUC），使用图神经网络得到 CNF 中子句的嵌入表示，采用分层 Transformer 体系结构以捕捉这些子句之间的关系，并注重没能同时出现在 UNSAT 核心中的子句的权重，实验结果表明，SATformer 能够优于现有的基于学习的 SAT 求解器。
Sep, 2022