【CNMO 科技消息】近日，约束求解与形式化领域的国际顶级赛事 SAT Competition 2026（可满足性问题国际算法竞赛）落下帷幕。由华为云天筹 AI 求解器团队、华中科技大学 John Hopcroft 计算中心、华为诺亚方舟实验室所组成的联合团队，获得并行 AI 赛道 SAT 组冠军。

华为

据 CNMO 科技了解，本届赛事吸引了来自全球顶尖高校和机构的 45 支队伍参赛，其一大亮点是首次设立 AI 赛道，鼓励参赛团队利用 AI 技术对求解器进行智能化调优。

按照赛事规则，基于 AI 调优的求解器只有在性能上超过最优的非 AI 求解器才能获得奖项。这意味着，AI 不能仅作为参数推荐或辅助开发工具，而必须带来真实、可量化、可验证的算法性能提升。AI 赛道的设立意味着赛事从传统的纯算法设计竞赛，迈入了经典算法 +AI 融合创新的新阶段。

本届赛事的数据集包含软硬件验证、EDA、密码学分析、组合优化等应用领域的 400 个高难度问题。天筹 AI 求解器团队研发的求解器 Kissat-MAB-HyPre-Evolve 凭借在复杂问题求解能力、并行搜索效率和算法鲁棒性等方面的综合优势，获并行 AI 赛道 SAT 组冠军。

这一结果表明，AI 已经能够突破传统辅助调优的边界，深入参与求解器算法和代码设计，并在全新、未见的数据集上形成稳定、可复现的性能增益。