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

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

Key words: satisfiability problem, conflict driven clause learning, learned clauses reduction, length of deduction