布尔可满足性（SAT问题）是芯片验证、网络安全和形式化证明检查等广泛计算任务的底层引擎。几十年来，人类专家不断改进求解该问题的算法，通过巧妙的变量选择、子句缩减和重启时机等启发式策略逐步提升性能。
7月17日发表在《自然·通讯》上的一项研究表明，大语言模型现在能够生成优于人类设计的SAT求解器启发式算法，在运行时上比基准求解器提升了40％，并在11个基准数据集中的8个上击败了最先进系统的最佳参数调整版本。
研究内容
由复旦大学柯伟和中国科学院蔡少伟领导的研究团队构建了一个名为AutoModSAT的框架。关键洞察在于，SAT求解器的代码库庞大且复杂，流行的Kissat求解器拥有25万个token。要求LLM直接修改这样的代码库是不现实的。相反，研究人员将CDCL（冲突驱动子句学习）求解器模块化，将重启时机、子句缩减、变量活动提升等恰好七个启发式函数暴露为一个清晰的搜索空间。
求解器模块化后，系统循环使用三个LLM智能体：编码器生成新的C++启发式代码，评估器过滤掉与现有启发式语义相同的代码，修复器修复编译错误。性能最佳的启发式在进化循环中得以保留。整个过程每个问题域使用50次LLM调用，并采用DeepSeek-V3，因其在低成本下具有竞争力的性能而被选中。
研究发现
在涵盖SAT竞赛问题、EDA（电子设计自动化）验证和组合谜题的11个基准数据集上，AutoModSAT生成的优化启发式算法在PAR-2评分（一种惩罚未求解实例的标准指标）上比基准模块化求解器平均提高了40％。
与经过参数调整的最先进求解器Kissat和CaDiCaL相比，AutoModSAT在11个数据集中的8个上获胜，平均加速约20％。在寄存器分配问题上，LLM发现的启发式在20个实例中解决了18个，而基准求解器解决的不到6个。在哈希表安全验证问题上（拥有1170万个变量和5360万个子句）AutoModSAT的PAR-2评分为3,302，而最佳竞争者为7,322。
LLM还发明了文献中未曾描述过的启发式算法。在重启策略方面，它生成了一种使用子句质量得分移动平均的动态方法，这是一种现有求解器中不存在的新方法。
重要意义
这与调整现有旋钮的自动超参数调优有本质区别。AutoModSAT生成新的算法代码，即人类专家未曾构想出的启发式算法。每次优化运行的总成本仅为几美元的API费用，使其适用于实际的工业部署。
模块化方法本身是本文最有力的论点：使求解器代码对LLM友好不是可选项，而是基础性要求。该方法可扩展至混合整数规划、约束满足和定理证明等其他复杂求解器。
局限性
基准求解器（ModSAT）比经过数十年优化的Kissat等最先进系统更为简单。部分改进反映了基准求解器的相对薄弱。该框架仅暴露七个启发式函数，无法触及在某些数据集上至关重要的顶层预处理参数。在Zamkeller数据集上，参数调整后的Kissat以四倍优势击败了AutoModSAT，因为差距存在于系统无法修改的组件中。
该论文发表于《自然·通讯》（DOI: 10.1038/s41467-026-74949-2），作者为Y. Sun、F. Ye、Z. Chen、K. Wei和S. Cai。
来源
1. Y. Sun, F. Ye, Z. Chen, K. Wei, S. Cai，”Discovering Heuristics in a Complex SAT Solver with Large Language Models,”《自然·通讯》(2026). DOI: 10.1038/s41467-026-74949-2
婷 翻译