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

计算机工程与科学 ›› 2023, Vol. 45 ›› Issue (11): 1941-1948.

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

冯心妍1,2,吴贯锋2,3,张丁荣1,2,王恪铭2,4

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

收稿日期:2022-08-01 修回日期:2022-09-23 接受日期:2023-11-25 出版日期:2023-11-25 发布日期:2023-11-16
基金资助:
国家自然科学基金(62106206)

A learnt clause evaluation algorithm based on recent literal polarity assignment

FENG Xin-yan1,2,WU Guan-feng2,3,ZHANG Ding-rong1,2,WANG Ke-ming2,4

(1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756;
2.National-Local Joint Engineering Laboratory of System Creditability Automatic Verification,
Southwest Jiaotong University,Chengdu 611756;
3.School of Mathematics,Southwest Jiaotong University,Chengdu 611756;
4.School of Computer and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China)

Received:2022-08-01 Revised:2022-09-23 Accepted:2023-11-25 Online:2023-11-25 Published:2023-11-16

摘要/Abstract

摘要： 为了维护学习子句数据库的大小，并以合理的成本执行单元传播，在SAT求解器求解过程中需要对学习子句进行评估，从而删除对求解过程无用的子句。因此，需要对学习子句数据库进行动态管理，包含对学习子句的分析和删除等，并提出新的评估子句有用性的方法，从而保留对求解最有促进作用的学习子句，以提高求解效能。从捕获学习子句近期的极性分配出发，结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省，来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准，针对其在子句评估环节的算法进行改进测试。实验结果表明，这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率，有效改善了原有求解器在一些问题上求解耗时过长的问题，并在先进求解器的水平上多求解了2个合取范式CNF文件，单个文件的平均求解时间缩短了13~34 s。

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

Abstract: 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.

Key words: SAT problem, clause evaluation strategy, conflict driven clause learning(CDCL), learnt clause

冯心妍, 吴贯锋, 张丁荣, 王恪铭, . 基于近期文字极性分配的学习子句评估算法[J]. 计算机工程与科学, 2023, 45(11): 1941-1948.

FENG Xin-yan, WU Guan-feng, ZHANG Ding-rong, WANG Ke-ming, . A learnt clause evaluation algorithm based on recent literal polarity assignment[J]. Computer Engineering & Science, 2023, 45(11): 1941-1948.