Feb, 2024

AutoSAT: 通过大型语言模型自动优化 SAT 求解器

PDF
TL;DRAutoSAT 是一种自动优化 SAT 解算器中启发式算法的新框架，基于大型模型（LLMs），它能够自主生成代码、进行评估，并利用反馈进一步优化启发式算法，从而减少人工干预并增强解算器的能力。AutoSAT 在插拔式基础上操作，不需要广泛的预备设置和模型训练，促进了具有容错性的思维链的合作过程，确保了强大的启发式优化。对 Conflict-Driven Clause Learning (CDCL) 解算器进行的大量实验证明了 AutoSAT 的整体优异性能，特别是在解决一些特定的 SAT 问题实例中。
heuristicssat solversautosatoptimizationproblem instances
发现论文，激发创造
  • SAT 问题的机器学习：约束启发式和新的图表示

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

    Jul, 2023

  • 利用可满足性辅助的语言模型与声明性提示

    本文提出了一种新的满足性辅助语言建模方法，利用自然语言处理模型生成任务的声明性规范，使用现成的自动定理证明器进行推理并验证答案的正确性，在解决需要更复杂的规划与搜索任务时比基于编程范式的模型更加有效。

    May, 2023

  • NLocalSAT: 利用解预测提升局部搜索

    本文介绍了一种结合 solution prediction model 和神经网络的方法 ——NLocalSAT，用于提高 stochastic local search 在解 Boolean satisfiability problem 时的有效性，并且在 SAT Competition 2018 的实验中取得了 27% ~ 62% 的性能提升。

    Jan, 2020

  • SoLA：基于求解器层适应的 LLM 在逻辑推理中的应用

    对大型语言模型（LLMs）在逻辑推理中所面临的挑战，以及利用工具学习改变问题求解的过程进行了探讨。本文提出了一种新颖的解算器层自适应（SoLA）方法，通过将解算器作为 LLMs 的新层，以不同的方式引导解决方案朝着可满足性发展。通过利用 MaxSAT 作为桥梁，定义正向和反向转移梯度，使最终模型能够收敛到满足的解决方案或证明不可满足性。通过验证 SoLA 在各种数据集上的性能，实证证明了其在大规模问题求解的效率上相对于现有的符号求解器（包括 Z3 和 Kissat）和工具学习方法的持续优势。

    Feb, 2024

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

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

    Sep, 2023

  • AutoSurvey：大型语言模型能自动编写调查问卷

    该研究介绍了 AutoSurvey，这是一种快速而有组织的方法，用于自动化创建在人工智能等快速发展领域中的综合文献调查。AutoSurvey 通过初始检索和大纲生成、专门的大语言模型进行的分段起草、整合和完善，以及严格的评估和迭代来解决信息数量和复杂性带来的挑战。研究做出了全面的解决方案，提出了可靠的评估方法，并通过实验证实了 AutoSurvey 的有效性。

    Jun, 2024

  • 利用因果推理解释 SAT 求解

    本文介绍了使用因果推理探究 SAT 求解器内在工作机制的方法 CausalSAT，并通过实验验证了其中四条经验法则和三个与现代 SAT 求解器实现密切相关的问题。

    Jun, 2023

  • 利用大型语言模型进行自动形式化

    本文研究了自动形式化的过程，并发现大型语言模型可用于将自然语言的数学问题翻译为 Isabelle/HOL 的形式化说明，证明了这种方法的实用性，并通过训练预先介绍的神经定理证明器使改进了 MiniF2F 定理证明基准的证明率从 29.6% 提高到 35.2%。

    May, 2022

  • 解决布尔可满足性问题的机器学习方法

    本文综述了近期文献，重点介绍了利用机器学习技术来解决布尔可满足性问题（SAT）的方法，包括从基于手工特征的朴素分类器到最新的端到端 SAT 求解器 NeuroSAT，以及将现有的 CDCL 和本地搜索求解器与机器学习相结合的最新进展。总体而言，利用机器学习解决 SAT 是一个有前途但充满挑战的研究课题，文章指出了当前研究的局限性并提出了未来可能的方向。

    Mar, 2022

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

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

    May, 2022