一种基于DR算法的构造子句预处理策略  

A preprocessing strategy for constructing clauses based on DR algorithm

作　　者：刘沛瑶 宋振明[2] 张世杰 LIU Pei-yao;SONG Zhen-ming;ZHANG Shi-jie(School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China;National Local Joint Engineering Laboratory of System Credibility Automatic Verification,Southwest Jiaotong University,Chengdu 610031,China)

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

出　　处：《信息技术》2019年第5期10-14,共5页Information Technology

基　　金：国家自然科学基金资助项目(61673320)

摘　　要：DR算法是一种完备的归结算法,但在归结过程中会产生大量的新子句,增加了求解时间,所以提高DR算法效率就成了一个问题。文中提出一种基于DR算法的预处理策略CC(Clauses Conduction),通过缩减子句集的规模,得到一个子子句集,再在其上运行DR算法,使得求解时间减少。这种策略虽不完备,但可以大幅度缩减运行时间。The DR algorithm is a complete resolution algorithm,but a large number of new clauses are generated in the resolution process,which increases the solution time. Therefore,improving the efficiency of the DR algorithm becomes a problem. In this paper,a preprocessing strategy CC( clauses conduction)based on DR algorithm is proposed. By reducing the scale of the clause sets,a sub-clause set is obtained,and then the DR algorithm is run on it to reduce the solution time. Although this strategy is not complete,it can greatly reduce the running time.

关 键 词：SAT问题 DR算法 归结算法 

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