The role of redundant clauses in solving satisfiability problems

Abstract

In our work, we investigate the role of redundant clauses in characterizing and solving hard SAT problems. Informally, a redundant clause is one that may be removed from the CNF representation of a SAT instance without altering the satisfying assignments of that instance. Correspondingly, a set of prime clauses is a set of clauses that preserves all the but that contains no redundant clauses. 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 the phase transition. WCV is based on a linear combination of the number of prime clauses (NPC) and the number of redundant clauses (NRC). We compare WCV to a number of existing parameters including backbone size and backbone fragility, the constrainedness measure, and the m /n ratio; we posit a variety of advantages to WCV over other measures. We believe that full utilization of redundant knowledge to solve random and real-world SAT problems can significantly improve the performance of SAT solvers, in terms of the scale of the problems that can be dealt with as well as the speed with which these problems are solved. © Springer-Verlag Berlin Heidelberg 2005.