基于近期文字极性分配的学习子句评估算法  

A learnt clause evaluation algorithm based on recent literal polarity assignment

作　　者：冯心妍 吴贯锋 张丁荣 王恪铭[2,4] FENG Xin-yan;WU Guan-feng;ZHANG Ding-rong;WANG Ke-ming(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756;National-Local Joint Engineering Laboratory of System Creditability Automatic Verification,Southwest Jiaotong University,Chengdu 611756;School of Mathematics,Southwest Jiaotong University,Chengdu 611756;School of Computer and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China)

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

出　　处：《计算机工程与科学》2023年第11期1941-1948,共8页Computer Engineering & Science

基　　金：国家自然科学基金(62106206)。

摘　　要：为了维护学习子句数据库的大小,并以合理的成本执行单元传播,在SAT求解器求解过程中需要对学习子句进行评估,从而删除对求解过程无用的子句。因此,需要对学习子句数据库进行动态管理,包含对学习子句的分析和删除等,并提出新的评估子句有用性的方法,从而保留对求解最有促进作用的学习子句,以提高求解效能。从捕获学习子句近期的极性分配出发,结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省,来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准,针对其在子句评估环节的算法进行改进测试。实验结果表明,这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率,有效改善了原有求解器在一些问题上求解耗时过长的问题,并在先进求解器的水平上多求解了2个合取范式CNF文件,单个文件的平均求解时间缩短了13~34 s。In order to maintain the size of the learned clause database and perform unit propagation with reasonable cost during the SAT solver s solving process,it is necessary to evaluate the learnt clauses and remove those that are not useful to the solving process.Therefore,it is necessary to propose a new method for evaluating clause usefulness,including the analysis and deletion of learned clauses,for dynamic management strategies of the learned clause database,thereby retaining the clauses that are most effective for solving and improving solving efficiency.This paper starts by capturing the recent polarity assignments of learnt clauses,combined with a heuristic based on literal polarity commonly used in the backtracking process of modern solvers-progress saving,to infer the relevance of a given learnt clause to the remaining search steps.Based on the two state-of-the-art Conflict Driven Clause Learning(CDCL)solvers,Glucose and MapleLCMDistChronoBT,their clause evaluation algorithms are improved and tested.The experimental results show that this clause evaluation strategy based on the recent literal polarity assignment can generally improve the solving efficiency of CDCL serial and parallel solvers,and effectively reducing the excessive time consumption of original solvers on some problems.Besides,2 more Conjunctive Normal Form(CNF)files are solved at the level of advanced solvers,and the average solve time of a single file is decreased by 13~34 seconds.

关 键 词：SAT问题 子句评估策略 CDCL 学习子句 

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