Learnt clause deletion based on clause deepness

摘要

Learnt clause deletion is a key component of SAT (Satisfiability Problem) solvers. First, this paper introduces clause activity based deletion and LBD (Literal Blocks Distance) based deletion respectively. Then, the deepness of learnt clauses is defined, and a new clause deletion method based on deepness of learnt clauses is proposed to accelerate the BCP (Boolean Constraint Propagation) procedure. Last, experimental results show that deepness based clause deletion method can improve the efficiency of solvers Minisat and Glucose.