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