Feb, 2024

NeuRes: 学习命题可满足性的证明

PDF
TL;DR我们介绍了一种神经符号证明型 SAT 求解器 NeuRes。与其他神经 SAT 求解方法不同，NeuRes 能够证明不可满足性而不仅仅是预测。通过使用命题证明来证明不可满足以及在不可满足和可满足公式的情况下加速找到满足真值分配的过程，NeuRes 以证书驱动的方式运行。为了实现这一点，我们提出了一种新颖的架构，该架构从图神经网络和指针网络中选择动态图结构的节点对，这对于生成解析证明至关重要。我们使用与 NeuroSAT 相同的随机公式分布编制了一组教师证明和真值分配的数据集，对我们的模型进行训练和评估。在实验中，我们展示了 NeuRes 在不同分布上比 NeuroSAT 解决更多的测试公式，而且数据效率更高。此外，我们还展示了 NeuRes 能够大大缩短教师证明的长度。我们利用这个特性设计了一种引导训练程序，在没有额外指导的情况下，成功将由高级求解器生成的证明数据集减少了约 23%。
neuresneuro-symbolic proof-based sat solverpropositional resolutiongraph neural networkspointer networks
发现论文，激发创造
  • 利用不可满足核心预测指导高性能 SAT 求解器

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

    Mar, 2019

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

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

    Feb, 2018

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

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

    Nov, 2022

  • 用于验证深度神经网络的 DPLL (T) 框架

    引入一种新的约束求解方法 NeuralSAT，用作深度神经网络 (DNN) 验证的符号化求解器。

    Jul, 2023

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

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

    Jul, 2020

  • 面向大规模神经定理证明

    提出了一种新型的神经定理证明器，通过仅考虑最高证明分数相关的证明路径，可以在以前无法应用的知识库上进行推理和学习。

    Jul, 2018

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

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

    Sep, 2023

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

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

    May, 2022

  • G2SAT：学习生成 SAT 公式

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

    Oct, 2019

  • 高效的认证分辨率证明检查

    该论文介绍了一种新的命题证明追踪格式，可以消除复杂的处理，从而实现有效（正式）证明检查。通过使用 C 实现证明检查器来证明该格式的好处。然后在 Coq 中形式化命题证明检查的理论，并从形式化中提取出该格式的一个正确性自证明的证明检查器。使用 280 个不可满足的实例对其性能进行了评估，并使用该格式正式验证了布尔勾股三元组猜想的最近 200 TB 的证明。

    Oct, 2016