SMT 求解器 Xolver 在 SMT-COMP 2026 荣获两项冠军
获奖
近日，2026 年度国际 SMT 求解器竞赛（SMT-COMP 2026）公布结果。由 SQuARE 组贾富琦主要研发的 SMT 独立求解器 Xolver 荣获“单查询赛道最大贡献——不可满足性”（Single Query Track Largest Contribution—UNSAT Performance Winner）和“非线性整数实数算术”（QF_NIRA Winner）两项冠军，马菲菲研究员和张健研究员担任指导教师。
Xolver 采用“研究人员主导、AI 编码智能体协同”的研发模式：研究人员负责总体架构、算法设计、任务组织和测试验证，Claude、ChatGPT、Kimi 等 AI 编码智能体协同完成主要代码实现。为保障求解结果的可靠性，Xolver 会使用原始公式回验可满足结果，并对部分不可满足性推理进行一致性检查。Xolver 的前端基于团队此前研发的 SOMTParser，负责 SMT-LIB 解析、类型检查和表达式管理等基础功能。
SMT 求解器是形式化验证的基础引擎，广泛应用于计算机基础软硬件的测试、分析与验证。SMT-COMP 是国际权威的 SMT 求解器竞赛，通过统一基准评测求解器在不同逻辑理论上的能力和效率。本届竞赛汇集了 Z3、cvc5、Bitwuzla、Yices2、OpenSMT 等主流求解器，参赛团队来自微软研究院、斯坦福大学、爱荷华大学和 SRI International 等高校与科研机构。