知识卡片：自动发现复杂SAT求解器中的启发式策略——基于大型语言模型

• 英文标题：Discovering heuristics in a complex SAT solver with large language models
• 英文关键词：SAT solving, heuristic discovery, large language models, evolutionary algorithm, benchmark evaluation
• 原始来源：Sun, Y. et al. Nature Communications (2026). DOI: 10.1038/s41467-026-74949-2

一句话结论

AutoModSAT 利用大型语言模型（LLM）自动发现并优化 SAT 求解器的启发式策略，在多个基准测试中性能相比基线求解器提升 40%，相比当前最优求解器提升 30%。

事件概述或研究问题

SAT 问题（可满足性问题）是计算复杂性理论的基础问题，并广泛用于工业应用。现代 SAT 求解器架构复杂，传统自动配置框架需要人工定义搜索空间，难以自动适应新问题的启发式策略。本研究提出 AutoModSAT，用 LLM 替代手动设计过程，实现启发式策略的自动生成与优化。

方法/产品要点

• LLM 兼容的模块化求解器设计：将求解器拆分为 LLM 易于理解和修改的模块。
• 无监督提示优化：自动生成多样化功能，避免提示工程带来的主观限制。
• 高效搜索机制：结合预搜索策略（presearch strategy）与 (1 + λ) 进化算法，在候选函数空间中快速迭代。

主要结果或产业意义

• 在广泛的数据集上，AutoModSAT 比基线求解器性能提升 40%，比最先进求解器（state-of-the-art）提升 30%。
• 相较于对最优求解器进行参数调优的替代方案，AutoModSAT 在大多数测试数据集上还实现了明显加速。
• 展示了 LLM 引导的启发式自动发现对于优化复杂 SAT 求解器的潜力。

为什么重要

• 克服了传统自动配置依赖“人工定义搜索空间”的根本局限，将启发式发现从手工设计推向自动化。
• 为计算机科学基础算法（SAT）与 LLM 的结合提供了一条可扩展的路径，有望推广到其他复杂求解器优化任务。

局限与不确定性

• 该论文在发布时仍为“未经编辑的早期手稿”，最终版本可能经过进一步编辑，当前内容可能存在错误。
• 具体细节（如进化算法的 λ 值、预搜索策略的实现方式、数据集具体构成等）在摘要中未完全披露，需查阅完整正文确认。
• 论文未明确说明 AutoModSAT 在不同规模（小/中/大）SAT 实例上的表现差异。

可用于图书/PPT/简报的角度

• 作为“LLM 自动化算法设计”的典型案例，可对比传统超参数优化方法。
• 引用原始数据：40% 与 30% 的性能提升，适合制作图表展示 AI 对传统计算问题的提升效果。
• 探讨“AI 辅助科学发现”在计算理论中的边界：从 SAT 求解延伸到其他 NP 难问题。

与既有脉络的关系

本卡片聚焦 LLM 直接优化 SAT 求解器中的启发式函数，与已有卡片（如 DataGovBench 评测 LLM 在数据分析中的不足）属于不同方向：前者是 LLM 作为优化工具，后者是 LLM 作为被评测对象。无重复陈述。

原始材料

• 论文标题：Discovering heuristics in a complex SAT solver with large language models
• 期刊：Nature Communications
• 发表日期：2026年7月17日（在线）
• 开源许可：CC BY 4.0
• 原文链接：https://www.nature.com/articles/s41467-026-74949-2