Reference: Zeng, H.; McIlraith, S. The Role of Redundant Clauses in Solving Satisfiability Problems (extended abstract), CP-2005 (the Eleventh International Conference on Principles and Practice of Constraint Programming), October 1-5, 2005, Barcelona, Spain. 2005.
Abstract: In this paper, we introduce the notion of redundant clauses to characterize the structure of SAT instances. We identify several interesting features of redundant clauses that provide compelling evidence of the correlation between the percentage of redundant clauses and the hardness of instances. We propose a definition of weighted clause-to-variable ratio (WCV), which substantially improves the classic clause-to-variable (m/n) ratio in predicting search cost and explaining phase phenomenon.
Notes:
Full paper available as pdf.