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

Jul, 2023

提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

May, 2018

本文提出了一种基于神经内存网络的迭代神经推理网络，使用门控机制进行推理，旨在解决多步推理中不平衡推理深度分布的问题，并将其应用于三个数据集上，实验结果表明该模型可以实现比 DeepLogic 和其他 RNN 基准模型更高的测试准确性，并在规则被洗牌时具有更好的超分布泛化能力。

Jul, 2022

使用强化学习和集成方法，借助改进的图神经网络和改良的公式表示方法，成功地构建了一种名称不变的公式表示方法，显着提高了自动定理证明的性能和泛化能力。

May, 2023

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

May, 2024

我们提出了一种利用机器学习技术进行符号计算研究的新方法。我们解释了如何将人类设计的在圆柱代数分解中选择变量顺序的启发式方法表示为受限神经网络。这使我们能够使用机器学习方法进一步优化这个启发式方法，得到与原始人类设计相似复杂度的新网络和新启发式。我们将其作为一种事前可解释性方法用于计算机代数开发。

Apr, 2024

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

May, 2022

本文首次使用图神经网络 (GNNs) 实现高阶证明搜索，并证明 GNNs 能够提高此领域的最新成果。我们考虑了高阶逻辑的几种图形表示，并将它们与 HOList 基准进行了评估。

May, 2019

提出了一种基于 NSR 的神经符号递归机制，通过感知、语法解析和语义推理三个模块的联合学习来实现优越的系统化推广，并通过三个不同领域的基准测试取得了 state-of-the-art 的表现结果。

Oct, 2022

本文介绍了一种新颖的框架 Relational Neural Machines，它可以对学习器的参数和基于一阶逻辑的推理器进行联合训练，下面将介绍其在大规模关系任务中的可行性和良好效果。

Feb, 2020