GraSS: 将图神经网络与专家知识结合，用于 SAT 求解器选择

KDDMay, 2024

GraSS: 将图神经网络与专家知识结合，用于 SAT 求解器选择

GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection

Zhanguang Zhang, Didier Chetelat, Joseph Cotnareanu, Amur Ghose, Wenyi Xiao...

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

Abstract

boolean satisfiability (SAT) problems are routinely solved by sat solvers in real-life applications, yet solving time can vary drastically between solvers for the same instance. This has motivated research into <

boolean satisfiability sat solvers machine learning models solver selection graph neural network

发现论文，激发创造

G4SATBench：使用图神经网络对 SAT 求解进行基准测试和推进

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

Sep, 2023

利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

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

Sep, 2023

基于 GNN 的 SAT 求解中的变量依赖问题解决

AsymSAT 是一种基于 GNN 的架构，能够扩展 GNN-based 方法的解题能力，改善 SAT 问题求解的性能，并通过使用生成的相关预测来维护变量之间的依赖关系。

Apr, 2023

命题模型计数的图神经网络

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

May, 2022

能否通过 Graph Networks 的 Q-Learning 学习适用于 SAT Solver 的可推广分支启发式策略？

本文介绍了使用图神经网络进行函数逼近的增强学习的 Graph-Q-SAT 分支启发式算法，该算法可用于解决 SAT 问题，并且在使用 MiniSat 求解器进行交互时可以减少解决 SAT 问题所需的迭代次数 2-3 倍。

Sep, 2019

SAT 问题的机器学习：约束启发式和新的图表示

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

Jul, 2023

图着色遇上深度学习：用于组合问题的有效图神经网络模型

本文介绍了如何使用简单的 GNN 架构来解决图着色的基本组合问题，并且展示了该模型在独立于训练数据的图数据上的泛化能力以及优于其他基线模型的表现。同时，我们还展示了如何将节点嵌入在多维空间中进行聚类，从而获得构造性解决方案。我们的结果有助于缩小人们对 GNN 算法学习的差距，并提供了符号推理与深度学习系统集成的可靠方法。

Mar, 2019

使用粘合变量预测增强 SAT 求解器

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

Jul, 2020

DeepSAT: 一种基于 EDA 驱动的 SAT 学习框架

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

May, 2022

G2SAT：学习生成 SAT 公式

本研究提出了 G2SAT 这一深度生成式框架，可以学习从输入公式集生成满足真实世界 SAT 实例特征的 SAT 公式，旨在扩展现有的数据集，为 SAT 求解器的性能提供优化方案。

Oct, 2019