晞德求索×中科院软件所斩获SMT-COMP 2025多个冠军

团队合作研发的BV-Parti (STP-Parti-Bitwuzla) 求解器创新性地提出了常数位与可行区间深度结合的推理方法、变量级划分、动态分布式等关键技术。在本届竞赛中，BV-Parti求解器表现优异：较之亚军求解器，整体上多求解近 30%个问题实例，在可满足性（SAT Performance）实例中，提升超过 60%。

此前，晞德求索与中科院软件所团队联合研发的Z3++求解器获得SMT-COMP 2022模型验证赛道最大贡献奖和最大领先奖、2022年国际联合逻辑奥林匹克大会中线性算术理论和非线性算术理论赛道第一。该求解器主要对算数理论进行了深入优化，在软件验证领域有更优秀的求解表现。