软件所分布式smt求解器研究工作获cav杰出论文奖
文章来源： | 发布时间：2024-07-25 | 【】 【】
近日，中国科学院软件研究所基础软件与系统重点实验室（计算机科学国家重点实验室）的论文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理论的变量级划分提供了探索空间。
工具链接：
并行版本：
分布式版本：
