Automatically discovering heuristics in a complex SAT solver with large language models
作者: Yiwen Sun, Furong Ye, Zhihan Chen, Ke Wei, Shaowei Cai
分类: cs.AI, cs.LO
发布日期: 2025-07-30
💡 一句话要点
AutoModSAT：利用大语言模型自动发现复杂SAT求解器中的启发式策略
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: SAT求解器 大语言模型 自动优化 启发式搜索 进化算法
📋 核心要点
- 现代SAT求解器架构复杂，难以优化，现有的自动配置框架依赖于手动约束的搜索空间，性能提升有限。
- AutoModSAT利用大语言模型，通过模块化求解器设计、自动提示优化和高效搜索策略，自动发现并优化SAT求解器的启发式策略。
- 实验结果表明，AutoModSAT相比基线求解器性能提升50%，优于SOTA求解器30%，且比参数调优的SOTA求解器平均加速20%。
📝 摘要（中文）
本文提出了一种新颖的范式，通过大语言模型（LLM）有效地优化复杂的SAT求解器，并开发了一个名为AutoModSAT的工具。为了实现卓越的性能，本文解决了三个根本挑战：（1）LLM友好的求解器：提出了系统性的指导方针，用于开发满足LLM兼容性的模块化求解器，强调代码简化、信息共享和减少错误；（2）自动提示优化：引入了一种无监督的自动提示优化方法，以提高LLM输出的多样性；（3）高效搜索策略：设计了一种预搜索策略和一个EA进化算法，用于最终高效地发现启发式策略。广泛的实验表明，AutoModSAT在各种数据集上实现了比基线求解器高50%的性能提升，并且比最先进（SOTA）的求解器优越30%。此外，与SOTA求解器的参数调整替代方案相比，AutoModSAT平均实现了20%的加速，展示了其在处理复杂问题实例方面的增强能力。这项工作弥合了AI驱动的启发式发现与关键任务系统优化之间的差距，并为下一代复杂求解器的开发提供了方法论上的进步和经验验证的结果。
🔬 方法详解
问题定义：论文旨在解决复杂SAT求解器难以优化的问题。现有方法，如自动配置框架，依赖于手动设计的搜索空间，限制了性能提升，无法充分利用求解器内部的复杂结构和潜在的优化空间。
核心思路：论文的核心思路是利用大语言模型（LLM）的强大生成和推理能力，自动探索和发现更有效的启发式策略。通过将求解器模块化，使其更易于被LLM理解和操作，并结合自动提示优化和高效搜索策略，实现对求解器的优化。
技术框架：AutoModSAT的整体框架包含以下几个主要模块：1) LLM友好的模块化求解器：对现有求解器进行重构，使其更易于被LLM理解和控制。2) 自动提示优化：利用无监督方法自动生成和优化LLM的提示，以提高LLM输出的多样性。3) 高效搜索策略：包括预搜索阶段和基于进化算法（EA）的优化阶段，用于高效地搜索最优的启发式策略。
关键创新：最重要的创新点在于将大语言模型引入到SAT求解器的自动优化过程中，并提出了一套完整的解决方案，包括LLM友好的求解器设计、自动提示优化和高效搜索策略。与传统方法相比，AutoModSAT能够自动探索更广阔的搜索空间，发现更有效的启发式策略。
关键设计：LLM友好的求解器设计强调代码简化、信息共享和减少错误。自动提示优化采用无监督方法，例如使用变分自编码器（VAE）生成多样化的提示。高效搜索策略中的预搜索阶段用于快速筛选有潜力的启发式策略，进化算法则用于进一步优化这些策略。具体的参数设置和网络结构在论文中未详细说明，属于未知信息。
🖼️ 关键图片
📊 实验亮点
AutoModSAT在广泛的数据集上进行了实验，结果表明，相比基线求解器，AutoModSAT实现了50%的性能提升。与最先进的（SOTA）求解器相比，AutoModSAT的性能提升了30%。此外，与参数调优后的SOTA求解器相比，AutoModSAT平均实现了20%的加速，尤其在处理复杂问题实例时表现出更强的能力。
🎯 应用场景
该研究成果可应用于各种需要高性能SAT求解器的领域，如软件验证、硬件设计、人工智能规划等。AutoModSAT能够自动优化求解器，降低人工调优成本，提高问题求解效率，具有重要的实际应用价值和潜力。未来，该方法可以推广到其他复杂系统的优化中。
📄 摘要（原文）
Satisfiability problem (SAT) is a cornerstone of computational complexity with broad industrial applications, and it remains challenging to optimize modern SAT solvers in real-world settings due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces and yield limited performance gains. This work introduces a novel paradigm which effectively optimizes complex SAT solvers via Large Language Models (LLMs), and a tool called AutoModSAT is developed. Three fundamental challenges are addressed in order to achieve superior performance: (1) LLM-friendly solver: Systematic guidelines are proposed for developing a modularized solver to meet LLMs' compatibility, emphasizing code simplification, information share and bug reduction; (2) Automatic prompt optimization: An unsupervised automatic prompt optimization method is introduced to advance the diversity of LLMs' output; (3) Efficient search strategy: We design a presearch strategy and an EA evolutionary algorithm for the final efficient and effective discovery of heuristics. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves 50% performance improvement over the baseline solver and achieves 30% superiority against the state-of-the-art (SOTA) solvers. Moreover, AutoModSAT attains a 20% speedup on average compared to parameter-tuned alternatives of the SOTA solvers, showcasing the enhanced capability in handling complex problem instances. This work bridges the gap between AI-driven heuristics discovery and mission-critical system optimization, and provides both methodological advancements and empirically validated results for next-generation complex solver development.