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

Sep, 2023

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

Mar, 2022

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

Feb, 2018

提出一种基于连续局部搜索与信念传播结合的算法 GradSAT，能在求解混合布尔约束问题方面有很好的应用表现，对称布尔约束和小系数伪布尔约束也可适用，并有望成为解决布尔满足性和优化问题的有效方法之一。

Dec, 2020

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

Jul, 2023

本研究使用 MaxSAT 问题中的 SPB 约束和子句权重技术，提出了一种新的局部搜索算法 SPB-MaxSAT，为 MaxSAT 局部搜索求解器的子句权重方法提供了新的视角和优秀的性能。

Jan, 2024

本论文研究了使用随机局部搜索解决基于满足性问题的 SAT 问题的流行范式，以及通过学习逻辑蕴含来改善求解器性能，并提出了一种生成逻辑等价问题形式的方法，进一步深入研究学习逻辑蕴含如何影响 SLS 运行时间的问题。

Oct, 2022

本文通过分析顺序版本算法的运行时行为，提出了一种评估给定算法并行性能的框架，并将此方法应用于研究两种 SAT 局部搜索求解器的并行性能，结果表明模型能够准确预测性能并展示了不同情况下局部搜索求解器的运行时分布。

Jan, 2024

介绍了一种名为 NSNet 的神经网络模型，通过使用一种新型的图神经网络 (GNN) 在潜在空间中对 BP 进行参数化，可以灵活配置以解决 SAT 和 #SAT 问题。

Nov, 2022

AutoSAT 是一种自动优化 SAT 解算器中启发式算法的新框架，基于大型模型（LLMs），它能够自主生成代码、进行评估，并利用反馈进一步优化启发式算法，从而减少人工干预并增强解算器的能力。AutoSAT 在插拔式基础上操作，不需要广泛的预备设置和模型训练，促进了具有容错性的思维链的合作过程，确保了强大的启发式优化。对 Conflict-Driven Clause Learning (CDCL) 解算器进行的大量实验证明了 AutoSAT 的整体优异性能，特别是在解决一些特定的 SAT 问题实例中。

Feb, 2024