约束求解的混合算法

1. 成果简介

约束求解器在工业基础软件中有重要的应用价值。如EDA领域中常用可满足性问题（SAT）求解器、软件验证领域常用可满足性模理论（SMT）求解器、规划调度领域常用混合整数规划（MIP）求解器。

SAT等判定问题的常用求解技术可以分为系统搜索和局部搜索两类，有一定互补性。早在1997年Selman等人于AAAI就提出了混合技术的命题逻辑挑战，但一直未能得到很好的处理。课题组创新性的提出了两者的深度混合技术，即以系统搜索算法CDCL为主体，局部搜索为辅进行搜索空的采样。CDCL会为局部搜索提供高质量初始解、局部搜索会反过来改善CDCL的搜索启发式。凭借该技术，Relaxed求解器取得了国际SAT比赛主赛道冠军、并获得国内首个SAT会议“最佳论文奖”。相关技术已被《Handbook of SAT》收录，且被目前领域最顶级SAT求解器kissat集成为一标准技术。

SMT作为SAT的一阶逻辑拓展问题，其求解技术可以视为SAT求解技术的拓展。课题组将混合SAT求解器的成功经验推广至整数算术背景理论的SMT问题（SMT-IA）上，设计了Hybrid-SMT求解器。Hybrid-SMT求解器研制了一种双层混合机制，外层为重量级局部搜索与系统搜索算法CDCL(T)的简单策略组合，内层为轻量级局部搜索与CDCL(T)的深度混合和信息交互技术。相关技术被集成与课题组z3++求解器，相关技术获得FLoC奥林匹克竞赛模型验证总比分最大领先奖与最大贡献奖，并发表与ICSE 2024。

工业应用中的整数规划问题常同时包含整数和实数约束，MIP是该类优化求解器的代表。此外，业内普遍采用基于分支限界（BnB）的系统搜索技术，但该技术难以满足计算负荷较大的领域的快速求解需求。为此，团队独立研制了局部搜索算法Local-MIP，并针对目标函数和约束的性质，分别设计了高效的算子与得分函数，来削减解空间，提升求解能力与效率。该技术获国内首个CP会议最佳论文奖，求解器刷新了国际标准数据集MIPLIP的10个公开实例的世界记录。

2. 技术创新点

SAT求解器Relaxed：系统搜索算法CDCL与局部搜索的深度混合机制，及信息交互利用策略。

SMT求解器Hybrid-SMT：系统搜索算法CDCL(T)与局部搜索的双层混合机制，及深度信息交互策略。

MIP求解器Local-MIP：深度剖析目标函数与复杂约束的内在联系，通过设计新型算子和得分函数，提出首个高效的自研局部搜索算法。

3. 技术成熟度

该成果当前处于产品化阶段（市场应用）。

4. 可应用领域

该成果可应用于电子设计自动化（包括逻辑综合、等价性验证、测试向量生成、布局布线等领域）、模型检查、软件形式化验证、调度排版、模型计数、神经网络验证、自动定理证明等领域。

5. 联系人

蔡少伟，caisw@ios.ac.cn，18515285536