Mar, 2024

IB-Net: 变量决策的初始分支网络在布尔可满足性中的应用

PDF
TL;DR提出了 IB-Net 框架，利用图神经网络和新颖的图编码技术来模拟不可满足问题，并与先进的求解器交互，以加速解决逻辑等效性检查工作流程，实验证明其平均运行时间提速了 5.0％（工业数据）和 8.3％（SAT 竞赛数据）。
发现论文，激发创造
  • 使用粘合变量预测增强 SAT 求解器

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

    Jul, 2020

  • NSNet: 一个通用的神经概率框架用于可满足性问题

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

    Nov, 2022

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

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

    Sep, 2023

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

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

    Sep, 2023

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

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

    Sep, 2019

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

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

    Apr, 2023

  • 利用单位监督学习 SAT 求解器

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

    Feb, 2018

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

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

    Jul, 2023

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

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

    May, 2024

  • 利用不可满足核心预测指导高性能 SAT 求解器

    本文介绍了使用改进的 NeuroSAT 架构，通过训练简化的神经网络来直接预测实际问题的不可满足核，以提供有效的指导高性能 SAT 求解器在解决特定问题分布时的问题上的应用。

    Mar, 2019