布尔可满足性 (SAT) 是一个基础的 NP-complete 问题，具有许多应用，包括自动计划和调度。为了解决大规模的情况，SAT 求解器必须依赖启发式算法，如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法，通过减少步数来降低运行时间，但是由于有用的模型相对较大和较慢，这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤，然后将控制权交给经典启发式算法，这简化了 SAT 求解的冷启动，并可以减少步数和总运行时间，但需要单独决定何时将控制权交给求解器。此外，我们介绍了一种改进的 Graph-Q-SAT，专门针对从其他领域转换而来的 SAT 问题，例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。

Jul, 2023

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

Sep, 2023

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

Sep, 2023

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

May, 2024

本文提出了一种结合深度 Q 学习算法、定制奖励信号和异构图神经网络架构的通用学习过程，用于在约束编程求解器中获取值选择启发式，并在图着色、最大独立集和最大割问题上进行实验，表明该框架能够在通用的前提下，找到更接近最优解的更好解决方案，而无需大量回溯。

Jan, 2023

提出了一种通用的图神经网络架构，该架构可以作为任何约束满足问题的端到端搜索启发式进行训练。该方法基于一种新颖的 CSP 图形表示，可以以纯数据驱动的方式为任何 CSP 生成问题特定的启发式，对于从随机数据中学习启发式，该方法在已知的 CSP 上优于以前的 RL 方法，并且可以与传统搜索启发式竞争或更好地处理结构更为复杂的测试实例。

Aug, 2022

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

May, 2022

提出了一种新方法来提升用于求解逻辑可满足性问题（SAT）的 NeuroCore 算法，此方法使用简化的神经网络架构作为分支启发式算法预测目标，而训练目标则是预测黏合变量，证明了该方法比其他方法更加有效。

Jul, 2020

本文提出了一种聚合图神经网络和指针机制的图指针网络模型来学习分支定界中的变量选择策略，结果表明该模型在求解速度和搜索树大小方面都优于现有的机器学习和专家设计的分支规则。

Jul, 2023

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

Feb, 2018