近期，约束求解与形式化领域的国际顶级赛事 SAT Competition 2026 落下帷幕。由华为诺亚方舟实验室、华为云天筹 AI 求解器团队和华中科技大学 John Hopcroft 计算中心所组成的联合团队，获得并行 AI 赛道 SAT 组冠军
SAT 问题被誉为计算复杂性理论中的 “珠穆朗玛峰”，从硬件验证、软件测试到密码学分析与 AI 规划，SAT 求解器已成为自动驾驶、EDA 芯片设计等产业研发中不可或缺的核心引擎。而 SAT Competition 正是这一领域最具权威性的国际顶级赛事，由 SAT Conference 组织，至今已有二十多年历史。SAT Competition 以开源、严谨、可复现的评测体系著称，汇聚全球顶尖科研机构与企业团队同台竞技，获奖求解器往往成为学界与工业界的标准工具，被国际顶级公司直接采用投入生产环境，赛事冠军含金量远超顶会论文。
2026 年的 SAT Competition 共吸引全球 45 支顶尖队伍参赛，并首次设立 AI 赛道，要求 AI 调优的求解器必须在性能上超越最优非 AI 求解器方可获奖 —— 这意味着 AI 不能仅作为辅助优化，而必须带来真实、可量化、可验证的算法性能提升，标志着 SAT 竞赛从人工算法设计迈入 “经典算法 + AI 融合创新” 的新阶段。
此次夺冠，依托于华为云天筹决策智能引擎AI 算法自动设计技术，搭建了 SAT 求解器专用的算法自调优流水线，集成了专家知识注入、多智能体协同、经验高效沉淀、多维度多尺度算法评估等核心能力，依托分布式算力集群实现高速算法评测打分，打通了全代码仓自动化算法设计链路。这意味着 AI 已不再仅仅是参数推荐或辅助开发工具，而是深入参与求解器的算法生成、代码演化、性能评测与策略优化全过程，针对各类全新未见数据集，均可实现稳定、可复现的求解性能提升。而支撑这次夺冠的算法自动设计能力，使用了华为和城大张青富教授团队联合开发的开源算法设计平台 LLM4AD_Next。该平台融合算法自动设计方向的最新成果，覆盖自动算法构建、独立记忆管理、Skill 轻量化部署和自动科研平台等核心能力。
自动算法构建：平台依托大模型驱动算法自主探索，通过自然语言输入，可完成算法构思、代码生成、迭代筛选与效果评估，无需依赖人工编写完整算法逻辑。系统结合进化式搜索，不断生成候选方案，自动淘汰无效版本。本次 SAT 竞赛中，这套能力就用于 SAT 求解器策略的自动演化，挖掘出超越人工调优的求解方案。
独立记忆管理：平台搭载华为诺亚自研的记忆管理平台「MindMemOS」，能够留存任务灵感、项目场景先验以及跨任务通用算法范式，沉淀试错过程中的成功经验与失败教训，避免重复踩坑，让算法设计从 “单次搜索” 走向 “持续积累”。比如在 SAT 求解器迭代过程中，系统记录不同实例集上调优策略的优劣，后续遇到同类问题可直接复用历史经验，减少重复评测开销。
Skill 轻量化部署：平台将经过验证的算子、算法模块封装为可复用技能单元，后续任务可直接调用、重组组件，不必每轮从零构建全部代码。随着项目持续迭代，技能库会不断沉淀扩充，大模型可基于已有组件做组合创新与二次优化，有效降低算法生成的复杂度，缩短算法开发周期，提升新任务下算法输出的质量与稳定性。目前已支持 10 类自动算法设计方法的 Skill 化部署。
自动科研平台：在前述能力基础上，平台打通了从问题定义、算法搜索、基准对比、结果归纳和论文撰写的完整科研链路。该能力基于开源自主科研智能体 AutoResearchClaw 的 23 阶段端到端科研流水线，并针对其在算法设计的短板做了针对性改进 —— 将 LLM4AD Next 集成到 AutoResearchClaw，在代码定稿前，先让 LLM4AD_Next 尝试改进其中的核心算法，再用原实验的评测方法逐一验证。只有成绩确实更好的版本，才会替换原算法，没有变好就保持原样。
该平台面向高校学生、科研人员以及广大算法开发者，可以让更多人都能借助这套 “让算法自我演化” 的工具，更好、更快、更容易地把想法变成可验证的结果。目前该平台已开源开放，可通过以下链接在线体验和下载尝试。
- 在线体验: https://llm4ad-next.cn
- GitHub 链接: https://github.com/Optima-CityU/LLM4AD_Next