今天有不同的朋友都发给我一个新闻，英伟达团队用大模型技术，结合了2024年SAT比赛多个求解器的代码并进行改进，在800个AMD EPYC 7F72 计算节点上进行70轮迭代演化之后，最终得到一个性能更佳的SAT求解器SATLUTION [1]。该求解器在2024年SAT比赛的数据集上进行训练，在2025年SAT比赛的数据集上进行测试，性能超过了2025年SAT比赛主赛道冠军，时间性能领先约16%。这是大模型修改复杂程序的一次成功尝试。

布尔可满足性问题（SAT），是第一个被证明为NP完全的问题，被认为是NP完全问题的代表性问题。SAT求解器的方向至少可以追溯到1960年的DP算法，是很多聪明的脑袋付出了长期努力的方向，也不乏有国际学术大咖的参与。大模型改进SAT求解器达到世界前沿这件事情，体现了现在的大模型已经在复杂程序编写方面具备了相当的能力。

大模型辅助研发SAT求解器这个方向，研究工作很少。第一个工作是我们软件所团队和复旦大学魏轲老师和孙一文同学以及第四范式公司的朋友合作研发的AutoSAT（2024 年 2 月）[2]，首次成功将大模型用于SAT求解器研发。AutoSAT采用多智能体技术，以现有求解器作为骨架，在其中留出关键位置，让大模型去补上最合适的“拼图”，从而完成求解器的构造。作为首个尝试，该工作在一个几百行C++代码的一个入门级SAT求解器EasySAT上进行了实验，显著改进了EasySAT的性能。在1个AMD EPYC 7763 节点上进行算法演化，在60轮迭代演化之后，AutoSAT甚至可以在其baseline求解器EasySAT完全求解不了任何一个实例的问题类型上，超过当时的世界前沿求解器Kissat的性能。

2025.7.31，我们软件所和复旦大学联合团队在AutoSAT的基础上，研发了第二个基于大模型技术改进的SAT求解器AutoModSAT，被英伟达这篇论文[1]介绍为此方向的基础性工作，核心想法在于改造复杂求解器为LLM-friendly，并利用prompt自动优化方法提升编写算法的多样性，以及预搜索策略减少搜索空间。我们应用该方法改进了一个著名的工业级SAT求解器MiniSAT，在60轮迭代演化之后（仍然是在1个AMD EPYC 7763 节点上进行算法演化），对于来自SAT比赛实例、EDA场景、以及不同约束优化问题的数据集上（筛选了不同难度的数据），均超过多个sota求解器（包括Kissat 3.1.1、Cadical 2.0 及各种调参版本）。[3]

2025年的国际SAT比赛上，湖北工业大学罗茂老师等人和法国皮卡尔第大学李初民老师的合作团队获得主赛道冠军， 并且在满足性分赛道中，该求解器平均求解时间较第二名缩短48.8%。在他们的技术文档中介绍该求解器主要用到了AutoSAT系列技术改进了前沿求解器Kissat，并优化了多智能体框架。[4]

2025.9.9，英伟达团队结合了AlphaEvolve和AutoSAT系列技术的优点，使用Cursor和Claude构建了大规模多智能体系统，利用了800个AMD EPYC 7F72 计算节点（800个计算节点！），批量快速测试LLM生成的求解器代码，每轮迭代可以评估更多求解器版本，从而研发了求解器SATLUTION，最终在SAT Competition 2025数据集上超过了2025年SAT冠军求解器，于是看到了媒体的“亮眼标题”报道。[1]

对于这样的结果，我一点都不感到意外，甚至是意料之中。我相信，在大模型的加持下，求解器领域即将发生一次伟大的变革。求解器的研发周期和门槛将大大降低，算法思路也将由大模型得以扩展，这将使得我们可以更快地研发更高性能的求解器。SAT问题作为NP完全问题的典型代表，这也意味着有诸多的复杂程序和专业软件都会因为大模型的参与进入一个快速发展期。

参考文献
1. Yu, C., Liang, R., Ho, T., & Ren H. (2025) Autonomous Code Evolution Meets NP-Completeness. arXiv preprint arXiv:2509.07367
2. Sun, Y., Ye, F., Zhang, X., Huang, S., Zhang, B., Wei, K., & Cai, S. (2024). AutoSAT: Automatically Optimize SAT Solvers via Large Language Models. arXiv preprint arXiv:2402.10705.
3. Sun, Y., Ye, F., Chen, Z., Wei, K., & Cai, S. (2025). Automatically Discovering Heuristics in a Complex SAT Solver with Large Language Models. arXiv preprint arXiv:2507.22876.
4. Ding, H., Luo, M., Li, C.-M., Li, S., Chen, R., Xiong, C., & Wu, X. (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).

#SATLUTION#