Sep, 2022

SATformer: 应用于 SAT 求解的 Transformer

PDF
TL;DR本文提出了 SATformer，一种基于 Transformer 的布尔满足性（SAT）求解方法，实现通过学习不可满足问题实例的最小不满足核（MUC），使用图神经网络得到 CNF 中子句的嵌入表示，采用分层 Transformer 体系结构以捕捉这些子句之间的关系，并注重没能同时出现在 UNSAT 核心中的子句的权重，实验结果表明，SATformer 能够优于现有的基于学习的 SAT 求解器。
satformertransformer-basedboolean satisfiabilityminimum unsatisfiable coresgraph neural network
发现论文，激发创造
  • 通过自然语言可满足性推动变形金刚规则推理的极限

    本研究通过提出一种新的方法构建具有挑战性的自然语言可满足性问题数据集，以研究 transformer 模型的推理能力，发现这些模型在解决困难的 NLSat 问题方面表现出非常强的能力，但仍然存在限制，包括需要选取适当的训练数据才能适用于更大的问题和限制其推理能力的问题。

    Dec, 2021

  • G2SAT：学习生成 SAT 公式

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

    Oct, 2019

  • FourierSAT: 一个基于傅里叶展开的代数框架求解混合布尔约束问题

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

    Dec, 2019

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

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

    May, 2024

  • 通用图形 Transformer 自注意力网络

    本文介绍了一种基于 Transformer 的 GNN 模型，叫做 UGformer，用于学习图表示。UGformer 有两个变体，第一个变体利用 Transformer 对每个输入节点的一组采样邻居进行编码，第二个变体利用 Transformer 对所有输入节点进行编码。实验结果表明，第一个变体在归纳和非监督转导设置下实现了基准数据集上的最新最准确统计，第二个变体在归纳文本分类中获得了最高准确率。

    Sep, 2019

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

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

    Feb, 2018

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

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

    Mar, 2019

  • Sumformer: 高效 Transformer 的通用逼近

    本文介绍了一种新的神经网络架构 Sumformer，可以近似等变序列到序列的函数。作者使用 Sumformer 在 Linformer 和 Performer 上实现了第一个通用的逼近结果，并提出了 Transformer 的新证明，仅需要一个注意力层即可实现通用逼近。

    Jul, 2023

  • Heterformer：一种用于异构文本网络节点表征学习的 Transformer 架构

    本文提出了一种名为 Heterformer 的异构图神经网络 - 嵌套变形器，能够融合图神经网络和预训练语言模型来进行节点表示学习，实验结果证明其在链接预测、节点分类、节点聚类以及语义检索方面都优于现有的基准模型。

    May, 2022

  • Boolformer：使用 Transformer 进行逻辑函数的符号回归

    我们介绍了 Boolformer，这是第一个经过训练的 Transformer 架构，能够执行完整的布尔函数符号回归。它能够预测复杂函数的简洁公式，并能够在提供不完整和嘈杂的观测数据时找到近似表达式。我们在广泛的实际二元分类数据集上评估了 Boolformer，展示了它作为解释性机器学习方法的潜力。最后，我们将其应用于基因调控网络动力学建模任务，使用最新的基准测试，展示了 Boolformer 与最先进的遗传算法相竞争，并具有数个量级的加速度。我们的代码和模型公开可用。

    Sep, 2023