Using Problem Symmetry in Search Based Satisfiability Algorithms

We introduce the notion of problem symmetry in search-basedSAT algorithms. We develop a theory of essentialpoints to formally characterize the potential search-spacepruning that can be realized by exploiting problem symmetry.We unify several search-pruning techniques used inmodern SAT solvers under a single framework, by showingthem to be special cases of the general theory of essentialpoints. We also propose a new pruning rule exploitingproblem symmetry. Preliminary experimental results validatethe efficacy of this rule in providing additional search-spacepruning beyond the pruning realized by techniquesimplemented in leading-edge SAT solvers.