近期，arXiv上陸續出現了大模型自動優化約束求解器的論文，一個是當下熱門的 AI 方向，一個是比較傳統的算法研究方向，它們的碰撞會擦出怎樣的火花？

求解器，是工業軟件的核心計算引擎，它在芯片設計、工業調度、智能制造等多個領域都有重要應用。比如，布爾可滿足性問題（SAT，Satisfiability Problem）求解器就是電子設計自動化（EDA，Electronic Design Automation）不可或缺的計算引擎。而 EDA 軟件則是芯片領域設計的至關重要的工具，也被稱為芯片產業的“命門”，因此該領域的研究成果與中國解決芯片“卡脖子”問題直接相關。

圖 | 蔡少偉（來源：蔡少偉）

中國科學院軟件研究所研究員蔡少偉帶領的團隊長期研究約束求解器，近三年來該團隊在結合大模型和約束求解的方向上持續耕耘，在arXiv上陸續公開了相關論文。蔡少偉認為，在大模型的加持下，求解器領域即將發生一次偉大的變革。求解器的研發周期和門檻將大大降低，算法思路也將由大模型得以擴展，這將讓人們能夠更快地研發更高性能的求解器。

據了解，該團隊近幾年的一個重要研究方向是如何利用大模型更快更好地完成求解器研發工作。在這一方向上，他們已經基于大模型研發了多個求解器，涵蓋了布爾可滿足性問題和偽布爾優化（PBO，Pseudo-Boolean Optimization）問題的求解器。其中，他們最重要成果便是基于大模型的 SAT 求解器。

該團隊認為，基于一個基礎求解器進行優化、而非完全從零開始是非常有益的，這樣大模型可以充分利用人類長期經驗建立起來的有效算法框架下進行算法設計。

近期，對于布爾可滿足性問題，該團隊通過大模型解決了求解器研發的三個關鍵挑戰：LLM-友好的求解器開發、自動提示優化和高效搜索策略。

其中涉及到的關鍵技術包括：

第一項關鍵技術是模塊化求解器設計：該團隊基于以下三個原則——修改的函數簡潔、代碼中類變量共享信息、啟發式探索中主動防錯，設計了 LLM-友好的求解器，為后續大模型的自動優化算法提供了基礎。

第二項關鍵技術是自動提示優化：該團隊通過采用無監督方法增強了大模型輸出的多樣性，避免了人工設計限制。

第三項關鍵技術是預搜索策略：即結合候選解剪枝和進化細化，引導大模型自動地生成高性能求解器。

第四項關鍵技術是關鍵函數優化：通過大模型修改各個重要函數對代碼，比如一些重要的啟發式策略，以此不斷地優化求解器。

（來源：https://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 框架等。

（來源：https://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 求解器的表現。這表明大模型已經可以優化工業級別的求解器。

（來源：https://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

運營/排版：何晨龍