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

Sep, 2023

提出了 DeepSAT 框架，使用 EDA 领域的知识来解决布尔可满足性问题（Boolean satisfiability），通过逻辑合成算法将 SAT 实例预处理为优化的与非图（AIGs），并利用 DAGNN 训练条件生成模型，在各种 SAT 实例上实现了显著的准确度提高。

May, 2022

应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性（SAT）问题，并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器，我们对现有的最先进模型进行训练，以预测具有 10,000 个变量的公式的可满足性，提出了新的分类器，可以对大多数困难水平的相同数据集进行显着改进，从而打破了过去基于公式的句法特征学习的方法，并使用求解器计算的简短前缀进行学习。

Nov, 2022

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

Sep, 2023

通过引入微观控制机制，提出用于 SAT 公式生成的 HardSATGEN 神经分裂 - 合并模型，从而更好地恢复工业基准的结构和计算特性。实验证明，与先前的方法相比，HardSATGEN 在结构统计方面平均性能提高了 38.5％，在计算指标方面提高了 88.4％，并且在指导求解器开发方面的有效性提高了超过 140.7％。

Feb, 2023

本文提出了一种基于 WLIG 的 SAT 公式生成框架 W2SAT，并通过实验证明了 WLIG 的优越性及其与其他方法的差异，并讨论了其在实际应用中的局限性以及可能的解决方案。

Feb, 2023

FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。

Dec, 2019

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

Jul, 2023

本文综述了近期文献，重点介绍了利用机器学习技术来解决布尔可满足性问题（SAT）的方法，包括从基于手工特征的朴素分类器到最新的端到端 SAT 求解器 NeuroSAT，以及将现有的 CDCL 和本地搜索求解器与机器学习相结合的最新进展。总体而言，利用机器学习解决 SAT 是一个有前途但充满挑战的研究课题，文章指出了当前研究的局限性并提出了未来可能的方向。

Mar, 2022

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

May, 2024