近日，第20届国际可满足性模理论求解竞赛（SMT-COMP 2025）正式公布竞赛结果。由北京航空航天大学软件学院罗川副教授团队研发的Z3-Noodler-Mocha求解器在字符串及其混合理论分组（QF_Strings Division）中斩获冠军，并在所有评价指标上均位列第一。这是国际可满足性模理论求解竞赛自创办以来，首次全部由中国成员组成的团队在字符串及其混合理论分组（QF_Strings Division）夺冠，标志着我国在该研究领域取得重大突破。

可满足性模理论（Satisfiability Modulo Theories，简称SMT）作为计算机科学领域的核心基础问题，致力于解决一阶逻辑公式在特定理论背景下的可满足性问题。其理论价值和应用前景受到学界高度认可，图灵奖得主Edmund Clarke教授曾指出，SMT能够有效表达形式化验证中的各类场景。在实际应用中，亚马逊云服务每日需调用高达十亿次SMT求解器以确保为用户提供可靠服务，提升SMT求解器的效率能够带来更高的系统可用性和稳健性。

国际SMT求解竞赛（SMT-COMP）是该领域极具影响力的年度赛事，迄今已成功举办20届。本届竞赛吸引了来自斯坦福大学、剑桥大学、国际斯坦福研究院等全球顶尖高校和研究机构的顶尖团队参与角逐。

北航软件学院团队研发的Z3-Noodler-Mocha求解器创新性地提出了字符串结构识别、正则约束提取和自动机合并等关键技术。在本届竞赛中，Z3-Noodler-Mocha求解器表现优异：较之亚军求解器多求解475个问题实例；更令人瞩目的是，其在24秒时限内求解的问题数量显著超过亚军求解器在1200秒时限内的求解数量。这一突破性成果充分展现了北航软件学院在该领域的技术实力。

本团队主要成员包括北航软件学院副教授兼团队负责人罗川老师，以及崔绍锞、杨振炜两位优秀学生。其中，崔绍锞同学是北航软件学院2024级博士研究生，具备坚实的理论基础和出色的创新能力，为团队在本届竞赛中的突破性表现做出了重要贡献；杨振炜同学于北航软件学院本科毕业，已被北航软件学院录取为2025级硕士研究生，积极参与求解器研发，在相关算法设计与实现方面展现了扎实的能力。值得一提的是，两位学生均多次获得国际大学生程序设计竞赛（ICPC）亚洲区域赛金奖，并代表北航参加了ICPC全球总决赛。

除获得分组冠军外，北航软件学院团队还获得了一项"最大贡献奖"（Largest Contribution），进一步印证了其研究工作的创新价值。这一成就不仅彰显了北航软件学院在国际学术舞台上的影响力，更为我国基础软件研究领域的发展注入了新的动力。

关于国际SMT求解竞赛：SMT-COMP始于2005年，是SMT研究领域的权威赛事，旨在推动SMT求解技术的创新与优化。竞赛结果被视为衡量该领域研究进展的重要参考。

相关链接：

-Z3-Noodler-Mocha求解器的下载地址：https://zenodo.org/records/15766150

图1：Z3-Noodler-Mocha求解器的作者列表

图2：SMT-COMP 2025竞赛官方网站发布的QF_Strings Division获奖结果