基于大模型的求解器研发框架

1. 成果简介

基于大模型的求解器研发框架AutoSAT和AutoPBO旨在通过大语言模型自动优化求解器代码，减少人工设计和调参成本的同时提升求解器性能。

AutoSAT首先将基于大模型的算法设计带入求解器领域，实现对SAT求解器的优化，通过将CDCL求解器拆分为9个关键启发式函数，使用大语言模型进行优化；结合贪心爬山法（GHC）和（1+1）进化算法（1+1 EA），引导LLMs生成更优的启发式方法，平衡探索与开发效率。同时通过多个agent的定义、目标明确、代码上下文嵌入等策略，确保LLMs生成高质量且可执行的代码。AutoSAT基于经典CDCL求解器进行优化，用几百行代码达到非常优越的性能，在多个数据集上超过SAT求解器Kissat，实现用非常少的代码量达到近乎最优的性能。

AutoPBO基于大语言模型提升伪布尔优化（PBO）求解器的性能。其核心机制是通过模块化设计的PBO求解器系统，将求解器的关键启发式函数（如重启、计算分数、计算子句权重等）独立定义，构建一个细粒度的搜索空间，使用大语言模型进行优化。AutoPBO系统接收求解器作为输入，并提取其中的已模块化的关键启发式函数。接着，系统利用精心设计的提示模板，指导LLM生成新的启发式函数。生成的代码会被自动集成到求解器中，并运行一系列测试来评估其性能。通过选择更新优化结果，迭代生成更好的启发式函数，结合进入求解器。

2. 技术创新点

（1）提出对复杂求解器的优化标准。针对大语言模型的特点，对求解器进行适当改写；

（2）提出多函数同步优化策略，将求解器拆分为多个关键启发式函数，并结合进化算法理论，合理设置调用LLMs的迭代次数，平衡探索与开发效率；

（3）构建高效自动化求解器优化框架。将求解器修改与计算解耦，实现并行修改、运行和反馈，进行高效的算法自动设计。

3. 技术成熟度

该成果当前处于小试阶段（实验室验证）。

4. 可应用领域

AutoSAT可用于工业SAT实例求解、EDA等价性验证等场景。AutoPBO可用于伪布尔优化场景的各领域，如物流与供应链、生产调度、电子设计自动化等。

5. 联系人

蔡少伟，caisw@ios.ac.cn，18515285536