近期，arXiv上陆续出现了大模型自动优化约束求解器的论文，一个是当下热门的 AI 方向，一个是比较传统的算法研究方向，它们的碰撞会擦出怎样的火花？
求解器，是工业软件的核心计算引擎，它在芯片设计、工业调度、智能制造等多个领域都有重要应用。比如，布尔可满足性问题（SAT，Satisfiability Problem）求解器就是电子设计自动化（EDA，Electronic Design Automation）不可或缺的计算引擎。而 EDA 软件则是芯片领域设计的至关重要的工具，也被称为芯片产业的“命门”，因此该领域的研究成果与中国解决芯片“卡脖子”问题直接相关。
图 | 蔡少伟（来源：蔡少伟）
中国科学院软件研究所研究员蔡少伟带领的团队长期研究约束求解器，近三年来该团队在结合大模型和约束求解的方向上持续耕耘，在arXiv上陆续公开了相关论文。蔡少伟认为，在大模型的加持下，求解器领域即将发生一次伟大的变革。求解器的研发周期和门槛将大大降低，算法思路也将由大模型得以扩展，这将让人们能够更快地研发更高性能的求解器。
据了解，该团队近几年的一个重要研究方向是如何利用大模型更快更好地完成求解器研发工作。在这一方向上，他们已经基于大模型研发了多个求解器，涵盖了布尔可满足性问题和伪布尔优化（PBO，Pseudo-Boolean Optimization）问题的求解器。其中，他们最重要成果便是基于大模型的 SAT 求解器。
该团队认为，基于一个基础求解器进行优化、而非完全从零开始是非常有益的，这样大模型可以充分利用人类长期经验建立起来的有效算法框架下进行算法设计。
近期，对于布尔可满足性问题，该团队通过大模型解决了求解器研发的三个关键挑战：LLM-友好的求解器开发、自动提示优化和高效搜索策略。
其中涉及到的关键技术包括：
第一项关键技术是模块化求解器设计：该团队基于以下三个原则——修改的函数简洁、代码中类变量共享信息、启发式探索中主动防错，设计了 LLM-友好的求解器，为后续大模型的自动优化算法提供了基础。
第二项关键技术是自动提示优化：该团队通过采用无监督方法增强了大模型输出的多样性，避免了人工设计限制。
第三项关键技术是预搜索策略：即结合候选解剪枝和进化细化，引导大模型自动地生成高性能求解器。
第四项关键技术是关键函数优化：通过大模型修改各个重要函数对代码，比如一些重要的启发式策略，以此不断地优化求解器。
（来源：http://arXiv.org/abs/2507.22876）
研究团队表示，其基于大模型研发的 SAT 求解器，在多个工业实例测试集上领先于人类研发的求解器。实验表明，利用大模型针对现存的工业级布尔可满足性问题求解器 MiniSAT 进行优化，可以使其平均求解速度提速 50%，并在多个工业实例集上超过目前人类设计的最先进求解器的性能。
蔡少伟还对 DeepTech 表示，布尔可满足性问题是非确定性多项式时间（NP，Nondeterministic Polynomial time）完全问题的典型代表，而此次成果也意味着诸多的复杂程序和专业软件都会因为大模型的参与进入一个快速发展期。其相信，大模型将使得求解器研发迈上一个新台阶，从而能够更好、更快地服务各种工业需求。
据了解，蔡少伟在 2020 年之前就开始研究求解器的自动化设计问题。2020 年，该团队曾和自动算法设计领域专家、荷兰莱顿大学教授霍尔格·胡斯（Holger Hoos）利用 AI 自动配置算法策略来提升布尔可满足性问题求解器的性能，相关论文发表于 2020 年的自然并行问题求解国际会议（PPSN，Parallel Problem Solving from Nature）上。
在 2022 年 GPT 出现之后，蔡少伟很快想到大模型对于数学建模和数学求解器的自动化将带来重大改革，于是便迅速启动了相关研究。恰逢复旦大学教授魏轲团队也在进行相关探索，于是双方一拍即合，立项合作研发基于大模型的求解器优化框架，并邀请了孙一文同学到中国科学院软件研究所实习。
但是，约束求解的工业实例较大，大模型无法直接读取解析，而求解器的更新迭代又比较慢，数据集也很少，所以很难按照传统思路来通过大量数据集训练得到合适的求解模型。为此，该团队转而寻找了一些更加轻量级的方式，比如多 Agent 框架等。
（来源：http://arXiv.org/pdf/2509.04007）
接着，该团队针对如下两个问题开展研究：一个是布尔可满足性问题，另一个是伪布尔优化问题。前者是最重要的非确定性多项式时间问题，后者是表达能力更丰富而形式简单的运筹优化问题。定下课题之后，他们设计并实现了基于大模型的自动优化框架，但是前期实验的结果不尽人意。相比于约束求解专家，大模型更类似于一个“博学者”，能力强但是不够专精，因此设计出的算法常常毫无道理、漏洞百出。
为此，他们开始集中于研究“如何让大模型生成的算法效果更好”这个问题。“这个阶段是最重要的、也是最艰难的，我们保存了大模型所生成的全部代码，分析了一些错误和不够好的结果，并探究了出现这类情况的原因，进而通过完善框架来解决这些问题。”该团队表示。
经过 2023 年一整年的奋斗，他们终于在 2024 年初发布了 AutoSAT，这是首个基于大模型研发的布尔可满足性问题求解器。AutoSAT 采用多智能体技术，以现有求解器作为骨架，该团队在其中留出了关键位置，以便让大模型去补上最合适的“拼图”，从而完成求解器的构造。
作为领域内的首次尝试，他们在一个包含几百行 C++ 代码的现存入门级布尔可满足性问题求解器 EasySAT 上进行了实验，结果发现 EasySAT 的性能得到了显著改善。在 1 个 AMD EPYC 7763 节点上进行算法演化，以及经过 60 轮的迭代演化之后，EasySAT 完全求解不了任何一个实例的问题类型上，而该团队研发的 AutoSAT 不仅比 EasySAT 更佳，甚至可以超过当时的全球前沿求解器 Kissat 的性能。
该团队回忆称：“2023 年，大模型的能力还没有现在这么强大，一个重要的局限就是处理长代码的能力不足。但是到了 2024 年，大模型能力有了一定提升，于是我们开始使用大模型修改更加复杂的布尔可满足性问题求解器。”
2025 年 7 月 30 日，对于他们来说是一个难忘的日子。这一天，他们成功研发了第二个基于大模型技术改进的布尔可满足性问题求解器——AutoModSAT，其核心思想是将复杂求解器改造得具备 LLM-友好的特征，并利用 prompt 自动优化方法来提升编写算法的多样性，以及通过预搜索策略来减少搜索空间。
他们还使用这一方法改进了工业界常用的一个著名的开源 SAT 求解器 MiniSAT，期间依旧是在 1 个 AMD EPYC 7763 节点上进行算法演化，经过 60 轮迭代演化之后，他们针对来自布尔可满足性问题比赛实例、电子设计自动化场景以及不同约束优化问题的数据集筛选了不同难度的数据，结果发现其所研发的 AutoModSAT 均能超过 Kissat 3.1.1 和 Cadical 2.0 等现存求解器，也能超过包含各种调参版本在内的多个 SOTA 求解器的表现。这表明大模型已经可以优化工业级别的求解器。
（来源：http://arXiv.org/pdf/2507.22876）
在本次研究伊始，他们能够确定的是：大模型一定能用在求解器研发上。但是，具体用在哪里？怎么应用？成本是否合理？这些问题都是未知的。于是，他们齐心协力进行探索，每周都开会分享自己通过调研学习到的新知识，最终才确定了合理的技术路线。“包括后面开发框架实验也是这样，大家总是一起想办法，一起验证 idea 是否有效，一起分析现有实验结果。”研究团队表示。其继续说道：“当时看起来很痛苦，毕竟这是世界上的新技术、新方法，就好像在黑暗里走迷宫，只能大家互相鼓励，一起摸索。”
最终，团队产出了大模型优化 PBO 求解器论文《AutoPBO: 基于大模型的局部搜索伪布尔优化求解器优化》（AutoPBO: LLM-powered Optimization for Local Search PBO Solvers）[1] 以及大模型优化 SAT 求解器论文《AutoSAT：基于大模型的 SAT 求解器优化》（AutoSAT: Automatically Optimize SAT Solvers via Large Language Models）[2] 和《复杂 SAT 求解器中基于大模型的启发式自动探索》（Automatically discovering heuristics in a complex SAT solver with large language models）[3]。团队成员李瑾媛、孙一文分别是第一作者，蔡少伟担任通讯作者，复旦大学魏轲老师为后两篇论文的共同通讯作者。
图 | 相关论文（来源：arXiv）
值得一提的是，基于大模型的 SAT 求解器逐渐引起了更多关注。2025 年国际 SAT 比赛的主赛道冠军由湖北工业大学罗茂教授等人和法国皮卡尔第大学李初民教授的合作团队联合获得。根据他们的介绍文档来看，其主要技术采用了蔡少伟团队在此方向的 AutoSAT 系列技术改进了前沿求解器 Kissat。2025 年 9 月，英伟达结合 AlphaEvolve 和蔡少伟团队 AutoModSAT 技术的优点（这也是该论文介绍的唯二两个相关工作），使用 Cursor 和 Claude 构建了大规模多智能体系统，利用了 800 个 AMD EPYC 7F72 计算节点批量快速测试了大模型生成的求解器代码，每轮迭代可以评估更多求解器版本，从而研发了求解器 SATLUTION，最终在 SAT Competition 2025 数据集上超过了 2025 年 SAT 冠军求解器。“这些都表明大模型在修改求解器方面已经建立起了可行的技术路径。”该团队表示。
据了解，该团队已有成员全职创办了一家名为晞德求索的公司，公司业务聚焦于求解器研发和数学技术服务，致力于更好地服务工业软件公司。目前，该公司正在不断完善求解器矩阵，并且研发的基于大模型的自动数学建模工具 SeedModeler 也在国际比赛获得佳绩，在 SAT 求解器和运筹优化求解器方面也已打造出商业化产品，并正在服务一些著名企业。
而在后续，蔡少伟团队会继续深化该研究，在更复杂的求解器上进行研究，并将提升资源的投入，通过使用更多的资源来在更复杂的智能体系统开展研究。另外，该团队也计划在更多约束求解问题上尝试这种基于大模型的自动化框架。“从目前经验来看，大模型应用在其它约束求解问题上也有较大的潜力。”该团队表示。
参考资料：
1.Jinyuan Li, Yi Chu, Yiwen Sun, Mengchuan Zou, Shaowei Cai."AutoPBO: LLM-powered Optimization for Local Search PBO Solvers."arXivpreprintarXiv:2509.04007 (2025).
2.Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, Shaowei Cai."Autosat: Automatically optimize sat solvers via large language models."arXivpreprintarXiv:2402.10705 (2024).
3.Yiwen Sun, Furong Ye, Zhihan Chen, Ke Wei, Shaowei Cai."Automatically discovering heuristics in a complex SAT solver with large language models."arXivpreprintarXiv:2507.22876 (2025).
4.Cunxi Yu, Rongjian Liang, Chia-Tung Ho, Haoxing Ren."Autonomous Code Evolution Meets NP-Completeness."arXivpreprintarXiv:2509.07367 (2025).
5.Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, & Xinyun Wu (2025). A Self-Optimizing Framework for SAT Solvers via Population Evolution and Large Language Model Collaboration. In Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions (pp. 15–17).
6.Chuan Luo, Holger H. Hoos, Shaowei Cai: PbO-CCSAT: Boosting Local Search for Satisfiability Using Programming by Optimisation. PPSN (1) 2020: 373-389
运营/排版：何晨龙