文章摘要
可满足性（SAT）问题是计算复杂性领域标志性难题，SAT Competition是该领域顶级国际赛事。2026年该赛事首次设立并行AI赛道，要求AI调优求解器性能超越现有最优非AI求解器，标志赛事迈入经典算法与AI融合的新阶段。华为联合华中科技大学团队斩获该赛道SAT组冠军，本次夺冠依托的开源算法设计平台LLM4AD_Next已对外开放。

可满足性（SAT）问题被视作计算复杂性理论领域的标志性难题，如同学科领域的珠穆朗玛峰，其求解技术的突破往往能带动多个产业的升级。从硬件验证、软件测试到密码学分析与AI规划，SAT求解器早已成为自动驾驶、EDA芯片设计等产业研发中不可或缺的核心引擎。

SAT Competition作为约束求解与形式化领域的顶级国际赛事，由SAT Conference主办，至今已有二十余年历史。该赛事以开源严谨、可复现的评测体系闻名，汇聚全球顶尖科研机构与企业团队同台竞技，获奖的求解器往往会成为学界与工业界的标准工具，直接被国际头部企业投入生产环境，赛事冠军的含金量甚至远超多数顶会论文。

2026年的SAT Competition吸引了全球45支顶尖队伍参赛，本届赛事首次设立AI赛道，赛事规则明确要求，通过AI调优的求解器必须在性能上超越当前最优的非AI求解器，才能最终获奖。这一规则标志着SAT竞赛正式从人工算法设计阶段，迈入“经典算法与AI融合创新”的全新发展阶段，AI不再仅仅作为辅助优化工具，而是需要带来真实可量化的性能提升。

在本届赛事中，由华为诺亚方舟实验室、华为云天筹AI求解器团队与华中科技大学John Hopcroft计算中心组成的联合团队，最终斩获并行AI赛道SAT组冠军。

此次夺冠的核心技术依托，是华为云天筹决策智能引擎与AI算法自动设计技术。团队搭建了针对SAT求解器的专用算法自调优流水线，集成了专家知识注入、多智能体协同、经验高效沉淀、多维度多尺度算法评估等核心能力，通过分布式算力集群实现高速算法评测打分，打通了全代码仓的自动化算法设计链路。这意味着AI已经深度参与到求解器的算法生成、代码演化、性能评测与策略优化的全流程中，即便面对全新的未知数据集，也能实现稳定且可复现的求解性能提升。

本次夺冠所使用的算法自动设计能力，源自华为与香港城市大学张青富教授团队联合开发的开源算法设计平台LLM4AD_Next。该平台融合了算法自动设计领域的最新研究成果，覆盖四大核心能力模块。

自动算法构建：平台依托大模型驱动算法自主探索，仅需通过自然语言输入，即可完成算法构思、代码生成、迭代筛选与效果评估的全流程，无需依赖人工编写完整的算法逻辑。系统结合进化式搜索机制，持续生成候选方案并自动淘汰无效版本。在本次SAT竞赛中，这套能力被用于SAT求解器策略的自动演化，最终挖掘出了超越人工调优的优质求解方案。

独立记忆管理：平台搭载华为诺亚自研的记忆管理平台「MindMemOS」，能够留存任务灵感、项目场景先验知识以及跨任务通用算法范式，沉淀试错过程中的成功经验与失败教训，避免重复踩坑，让算法设计从“单次搜索”转向“持续积累”。例如在SAT求解器的迭代过程中，系统会记录不同实例集上调优策略的优劣表现，后续遇到同类问题时可以直接复用历史经验，大幅减少重复评测的开销。

Skill轻量化部署：平台将经过验证的算子、算法模块封装为可复用的技能单元，后续任务可以直接调用、重组这些组件，无需每轮从零开始构建全部代码。随着项目的持续迭代，技能库会不断沉淀扩充，大模型可以基于已有组件进行组合创新与二次优化，有效降低算法生成的复杂度，缩短算法开发周期，提升新任务下算法输出的质量与稳定性。目前该平台已支持10类自动算法设计方法的Skill化部署。

自动科研平台：在前面三项能力的基础上，平台打通了从问题定义、算法搜索、基准对比、结果归纳到论文撰写的完整科研链路。该能力基于开源自主科研智能体AutoResearchClaw的23阶段端到端科研流水线，并针对其在算法设计领域的短板进行了针对性改进：将LLM4AD_Next集成到AutoResearchClaw中，在代码定稿前，先让LLM4AD_Next尝试改进其中的核心算法，再使用原实验的评测方法进行逐一验证，只有性能确实更优的版本才会替换原算法，若没有提升则保留原有方案。

该平台面向高校学生、科研人员以及广大算法开发者，能够帮助更多人借助“让算法自我演化”的工具，更高效、更便捷地将想法转化为可验证的成果。目前该平台已开源开放，用户可以通过以下链接在线体验或下载使用。

以上内容不代表本平台立场，仅供读者参考