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

摘要： 学习子句删除策略是CDCL-SAT求解器中的一个重要内容，可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的，极大地影响求解效率。基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程，基于此，提出一种基于演绎长度的学习子句评估方法，并与现有的基于文字块距离的评估方法结合，根据排序子句的基准不同，形成两种不同的结合算法。采用国际SAT竞赛的基准实例，与目前主流的求解器进行了实验对比分析。结果表明，所提的结合算法能更好地评估学习子句的有用性，较基于文字块距离策略的求解个数提高了4.1%，说明所提策略具有一定的优势。

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