|M.Sc Thesis||Department of Computer Science|
|Supervisor:||Assoc. Prof. Ben Sasson Eliyahu|
|Full Thesis text|
This thesis shows that the use of "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 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 thesis correspond respectively to (i) "standard" DPLL, (ii) DPLL augmented with clause learning, and (iii) multi-valued logic DPLL. That is: A running of the algorithm on an unsatisfiable formula F is corresponded with a refutation of F in the proof system.
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 set of efficiently detectable symmetries that involve only a constant number of variables.