基于回跳层数的SAT求解器学习子句删除策略  

Back-jump levels based learnt clauses deletion strategy for SAT solver

作　　者：沈雪 陈树伟 徐扬[1,3] 吴贯锋 Shen Xue;Chen Shuwei;Xu Yang;Wu Guanfeng(School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China;School of Information&Technology,Southwest Jiaotong University,Chengdu 610031,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610031,China)

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

出　　处：《计算机应用研究》2020年第11期3316-3320,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(61673320);中央高校基本科研业务费专项资金资助项目(2682018ZT10,2682018CX59)。

摘　　要：目前学习子句删除策略广泛采用的是基于LBD的评估方式,LBD评估方式在每次执行删除时都会删除前一半LBD值大的学习子句,这种方式对LBD值大的学习子句的删除过于激进。针对此问题,提出了一种利用冲突回跳层数(back-jump levels)的评估方式来保留LBD值较大的有用学习子句。以CDCL(conflict driven clause learning)完备算法为框架,在子句删除环节形成了BJL删除算法。通过测试2017年SAT国际竞赛例,对新改进的版本与原版求解器进行了对比实验。实验表明,所提策略可显著提高求解器的求解性能和求解效率。At present,the widely used method for learnt clauses deletion strategy is based on the LBD evaluation method,which deletes the learnt clauses with the first half of the LBD value in each deletion operation.For the large LBD value,this method is too aggressive.To solve this problem,this paper proposed an evaluation method that used back-jump levels to preserve the relevant learnt clauses with large LBD value.Based on the CDCL complete algorithm,it formed the BJL deletion algorithm in the learnt clauses deletion stage.It conducted a comparative experiment on the newly improved version and the original version by testing the 2017 SAT international competition.Experiments show that the proposed strategy can significantly improve the solver’s performance and efficiency.

关 键 词：可满足性问题 冲突驱动子句学习 LBD 回跳层数 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]