一种基于搜索路径识别的CDCL命题逻辑求解器延迟重启算法  

Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver

作　　者：陈青山 徐扬 吴贯锋 何星星 

机构地区：[1]西南交通大学信息科学与技术学院,成都611756 [2]系统可信性自动验证国家地方联合工程实验室,成都610031

出　　处：《计算机科学》2017年第11期279-283,共5页Computer Science

基　　金：国家自然科学基金项目(61673320;11526171;61305074);中央高校基本科研业务费项目(2682017ZT12)资助

摘　　要：适当的重启有助于求解器跳出局部最优,但频繁重启会严重降低效率。为解决CDCL求解器重启触发条件随意性大的问题,提出一种基于搜索路径识别的延迟重启算法。该算法使用Luby序列触发延时重启判断,将当前搜索路径和已搜索路径转换为向量空间模型,通过计算向量空间相似度来判断当前搜索过程是否会进入重复搜索空间。若向量空间相似度达到设定阈值,则触发重启,否则延迟重启。采用SAT国际竞赛的实例,与两个主流的求解器进行了对比实验。结果表明,所提算法能够有效规避重复搜索空间问题,并显著提高求解效率。An appropriate restart is helpful for a solver to jump out of the local optimization,but more frequent restarts will significantly reduce the efficiency.To address the arbitrariness of triggering conditions for the restart of CDCL solver,the delaying restart algorithm based on path identification was proposed in this paper.Specifically,the Luby sequence is utilized to trigger the delaying restart decision,which converts current path and the searched paths to vector space models（VSMs）such that the similarity of VSMs is calculated to judge whether the current search process will get into the repetitive search space.Once the underlying similarity reaches a given threshold,the restart is triggered,otherwise it will be delayed.SAT international testing example and two state-of-the-art solvers were adopted for comparison purpose.The experimental results show that the proposed algorithm can not only effectively avoid the repetitive search space,but also obviously improve the solving efficiency.

关 键 词：SAT问题 命题逻辑 重启 路径识别 向量空间模型 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]