Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR10-068 | 15th April 2010 19:53

Breaking local symmetries can dramatically reduce the length of propositional refutations


Authors: Shir Ben-Israel, Eli Ben-Sasson, David Karger
Publication: 15th April 2010 19:53
Downloads: 3601


This paper shows that the use of ``local symmetry breaking'' can dramatically reduce the length of propositional refutations. For each of the three propositional proof systems known as (i) treelike resolution, (ii) resolution, and (iii) k-DNF resolution, we describe families of unsatisfiable formulas in conjunctive normal form (CNF) that are ``hard-to-refute'', i.e., require exponentially long refutations, but when a polynomial-time procedure for detecting and adding clauses arising from ``local'' symmetries --- that permute only a constant number of variables --- is applied to a formula in this family, it is transformed into an ``easy-to-refute'' CNF whose refutation length is polynomially bounded.

One of the most successful paradigms for solving instances of the satisfiability problem is the branch-and-bound strategy set forth by Davis, Putnam, Loveland and Logemann (DPLL). The three proof systems we discuss in this paper correspond respectively to (i) ``standard'' DPLL, (ii) DPLL augmented with clause learning, and (iii) multi-valued logic DPLL. Viewed with this correspondence in mind, our results suggest that the running time of SAT solvers from the above mentioned family of algorithms can be dramatically reduced when making use of information about the symmetries of a formula. This is true even when restricting our attention to the set of efficiently detectable symmetries that involve only a constant number of variables.

ISSN 1433-8092 | Imprint