期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2010
卷号：2010
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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.
