基于演绎长度的学习子句删除策略  

Learned clauses reduction strategy based on length of deduction

作　　者：常文静 徐扬[3,2] 吴贯锋 CHANG Wenjing;XU Yang;WU Guanfeng(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610036,China;School of Mathematics,Southwest Jiaotong University,Chengdu 610036,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610036,China)

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

出　　处：《计算机工程与应用》2018年第16期30-36,共7页Computer Engineering and Applications

基　　金：国家自然科学基金(No.61673320);中央高校基本科研业务费专项资金(No.2682018ZT10)

摘　　要：学习子句删除策略是CDCL-SAT求解器中的一个重要内容,可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的,极大地影响求解效率。基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程,基于此,提出一种基于演绎长度的学习子句评估方法,并与现有的基于文字块距离的评估方法结合,根据排序子句的基准不同,形成两种不同的结合算法。采用国际SAT竞赛的基准实例,与目前主流的求解器进行了实验对比分析。结果表明,所提的结合算法能更好地评估学习子句的有用性,较基于文字块距离策略的求解个数提高了4.1%,说明所提策略具有一定的优势。Learned clauses database reduction heuristics are one of the most important components of a Conflict Driven Clause Learning（CDCL）SAT solver,which are used to avoid memory consumption and sustain unit propagation speed.The learned clause to be removed is different based on different evaluation criteria,which is measuring the usefulness of learned clause.A CDCL based SAT solver can be formulated as a resolution proof system with a learned clause deletion strategy.On this basic,a learned clauses reduction strategy based on length of resolution is proposed,and combined with Literals Blocks Distance（LBD）evaluation criteria.According to the basis of sorting clauses,two different combination algorithms are formed.Based on international SAT competition instances,this paper analyzes the experimental comparison with the current mainstream solver.Experimental results indicate that compared with the LBD-based criteria method,the number of the proposed combined method is increased by 4.1%.The proposed strategy can preferably estimate the usefulness of learned clauses and efficiently improve the performance of solving instances.

关 键 词：可满足性问题 冲突驱动子句学习 学习子句删除 演绎长度 

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