近期，约束求解与形式化领域的国际顶级赛事 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 特别