分布式约束求解技术

1. 成果简介

在逻辑公式可满足性（SAT）领域，随着问题规模的不断扩大，传统串行求解器已难以满足工业级应用需求。为此，我们自主研发了支持云计算的分布式SAT求解器框架——PRS-distributed。该框架集成了多种先进求解器，采用多种预处理技术、分支顺序随机化以及子句共享机制，不仅有效降低问题规模和计算负担，还实现了不同线程或计算节点间的高效信息共享，大幅提升了大规模SAT问题的求解性能。PRS-distributed在2024年SAT竞赛的云计算赛道中荣获银牌。

在一阶逻辑可满足性（SMT）领域，我们创新性的首次提出基于变量级划分的动态分布式SMT求解框架AriParti，针对传统布尔级划分难以应对复杂理论内容的问题，通过增强约束传播算法与布尔传播协同，实现了对任意逻辑结构公式的高效划分和简化。实验结果表明，在52471个算术理论测试实例中，采用该技术后成功求解实例增加3495个，求解速度提升约30%，在6247个串行求解失败的实例中成功解决1211个，尤其在非线性理论问题上效果突出。AriParti在2024年SMT竞赛的云赛道获得“最大领先奖”和“最大贡献奖”，同时相关论文荣获CAV2024杰出论文奖。

在混合整数规划（MIP）领域，我们开发了分布式求解器PartiMIP。该系统基于子问题划分，通过关键变量评估和递归预处理，将大问题拆分为规模更小的子问题，并设计了动态调度机制以根据节点求解状态调整分支树，从而大幅提升求解效率。在SCIP和HiGHS的32核测试中，与基准求解器相比平均性能分别提升了15%和16.4%，优于现有并行技术。PartiMIP刷新了国际标准数据集MIPLIB中21个公开实例的已知最佳解纪录，并成功完备求解了1例此前未被其他求解器解决的open实例。

2. 技术创新点

在SAT领域，通过云计算框架PRS-distributed，采用预处理、随机化分支和子句共享机制，有效降低问题规模和计算负担，实现不同节点间高效协同。

在SMT领域，首创基于变量级划分的动态分布式求解框架AriParti，利用增强约束传播与布尔传播协同，高效划分和简化复杂公式。

在MIP领域，构建了基于子问题划分和关键变量评估的分布式求解器PartiMIP，通过递归预处理和动态调度机制，将大问题拆解为小规模子问题。

3. 技术成熟度

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

4. 可应用领域

该成果适用于电子设计自动化（EDA）、密码学、软件验证、操作系统内核及复杂系统安全分析等领域，同时在工业生产调度、资源分配优化、物流路径规划等规划问题中也表现卓越，为解决大规模复杂约束问题提供了有力支撑。

5. 联系人

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