华为云天筹AI求解器获SAT国际算法竞赛并行SAT组冠军

此次夺冠，不仅体现了联合团队在约束求解、并行计算和SAT核心算法领域的深厚技术积累，更验证了AI算法自动设计在复杂基础算法研发中的创新价值。通过将AI深入应用于算法生成、代码演化、性能评测和策略优化全过程，华为云天筹AI求解器推动求解器研发从依赖专家人工设计，向“经典算法与AI协同创新”演进，为高性能求解器研发探索出一条新的技术路径。

SAT（Satisfiability Problem，可满足性问题）是约束求解、理论计算机科学、形式化等多个领域中最为核心的问题之一，被誉为计算复杂性理论中的“珠穆朗玛峰”，是算法设计、启发式搜索和约束求解领域的试金石与基石难题。

从工业应用角度看，SAT求解器的价值远不止于理论层面，在硬件验证、软件测试、密码学分析、人工智能规划等领域已经成为不可或缺的核心工具。在硬件验证环节中，SAT求解器是EDA工具链中运行频率最高的核心引擎之一；在软件测试中，SAT求解器被用于路径可达性分析与测试用例自动生成。可以说，SAT求解器的性能已成为影响EDA、自动驾驶等诸多产业研发效率的关键因素之一。

SAT Competition是由业界顶级会议SAT Conference组织的国际赛事，至今已有二十余年历史，汇聚了全球优秀的科研机构和企业团队，以最先进的SAT求解器同台竞技。该赛事以其开源、严谨、可复现的评测体系著称，成功推动了SAT开源社区的蓬勃发展，获奖求解器往往成为学界与工业界的标准工具，许多国际顶级硬件公司、软件企业直接采用竞赛中表现优异的求解器投入生产环境，其冠军含金量远高于顶会论文。

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

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

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

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

本次获奖的背后，是华为云天筹AI求解器团队在传统约束求解算法、并行计算及AI算法自动设计领域深厚的技术积淀与持续的技术创新，核心技术组件包括：

在获奖求解器Kissat-MAB-HyPre-Evolve中，采用HyPre混合预处理与并行搜索隔离的两层架构，并行搜索采用Portfolio框架并跑多个AI演化的串行求解器，其中每一个都是以串行核心求解器为基础，基于OptvEvolve演化改进的AI求解器。

当下，AI已不再仅仅是求解器的辅助工具，更是算法创新的核心引擎。华为云天筹AI求解器推动AI与求解器研发交付全链路深度融合，将AI技术贯穿于自动建模、超参调优、算法设计的全环节，同步提升求解器易用性、研发迭代效率与求解运算性能，现已在复杂难例攻坚、重点项目落地、求解性能跃升、潜在缺陷识别等场景取得了显著成效。