Abstract: The technique of clause set simplification is a crucial part in the process of propositional logic SAT solving.The clause elimination methods corresponding to the redundancy property can accurately identify and delete redundant clauses.Either in the pre-processing stage or in the process of SAT solving,the embedded clause elimination methods in the SAT solver accelerate the solving efficiency of the solver. A large number of efficient clause elimination methods are extended based on the redundancy properties of blocked clauses and implication module resolution clauses.In order to check whether clause C is redundant,we need only to consider whether clause C satisfies the redundancy conditions.The proposed L-type redundancy is an extension of the blocked redundancy property,subsumption redundancy property and implication module resolution redundancy. It extends the judgement condition of redundant clause from the resolution of single literal to the combination of the set of literals.According to the properties of L-type redundancy,this paper analyzes the properties of L-type redundancy clause,and applies comparison analy-sis on the efficiency of L-type redundancy clauses and other existed redundant clauses,so as to illustrate the efficiency of L-type redundancy clauses.

Key words: Propositional logic, Clause elimination method, L-type redundancy property