2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02)
Using Problem Symmetry in Search Based Satisfiability Algorithms
Paris, France
March 04-March 08
ISBN: 0-7695-1471-5
We introduce the notion of problem symmetry in search-based SAT algorithms. We develop a theory of essential points to formally characterize the potential search-space pruning that can be realized by exploiting problem symmetry. We unify several search-pruning techniques used in modern SAT solvers under a single framework, by showing them to be special cases of the general theory of essential points. We also propose a new pruning rule exploiting problem symmetry. Preliminary experimental results validate the efficacy of this rule in providing additional search-space pruning beyond the pruning realized by techniques implemented in leading-edge SAT solvers.
Citation:
E. Goldberg, M. Prasad, R. Brayton, "Using Problem Symmetry in Search Based Satisfiability Algorithms," date, pp.0134, 2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02), 2002