近日，中国科学院软件研究所基础软件与系统重点实验室（计算机科学国家重点实验室）的论文Distributed　SMT　Arithmetic　Theories　Solving　Based　on　Dynamic　Variable－level　Partitioning在形式化验证领域国际旗舰会议Computer　Aided　Verification（CAV　2024）上荣获杰出论文奖（CAV　Distinguished　Paper　Award），这也是中国学者在形式化验证领域首次获得该荣誉。论文第一作者为博士生赵梦宇，通讯作者为蔡少伟研究员。

CAV杰出论文获奖证书

可满足性模理论（SMT）是形式化方法与自动推理的一个重要研究方向，主要研究在特定理论下（如等式理论和无解释函数、位向量、线性和非线性算术）的一阶逻辑公式可满足性的判定方法。目前，大多数相关工作集中在如何改进串行SMT求解器中的求解技术和启发式方法。随着工业样例难度和规模的增长，串行SMT求解已逐渐无法满足业界的需求。现有的SMT划分策略也主要遵循SAT的布尔级划分方法，对于具有简单布尔结构的公式，现有的划分策略无法产生足够的子问题，严重限制了分布式SMT求解器性能。

论文首次提出了一种基于变量级划分的动态并行框架，可以有效地对任何逻辑结构的问题进行划分。针对算术理论，通过增强约束传播算法，将其集成到变量级划分策略中，显著提升了公式简化和解空间削减能力，从而大大提升了求解能力与效率。

变量级划分技术示例图

研究团队将该方法应用于目前国际最先进的求解器CVC5、OpenSMT2和Z3。与基准求解器相比，仅使用8核的并行求解，平均成功求解实例增加了3495个（算术理论相关测试基准集共有52471个实例），求解速度提高约30％。此外，在任意串行求解器都无法解决的6247个实例中，通过我们的分布式方法，成功地解决了1211个。该方法相较于CVC5和OpenSMT2团队开发的前沿并行求解技术也有着显著提升，尤其在非线性理论上的表现尤为突出。

对比基求解器的实验结果

对比前沿并行求解技术的实验结果

该研究不仅为分而治之的并行划分方法提供了新的方向，也为其他SMT理论的变量级划分提供了探索空间。

工具链接：

并行版本：https://github.com/shaowei-cai-group/AriParti

分布式版本：https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2024