The Width Method for Resolution and Sums-of-Squares Proofs

Resolution is a proof system for propositional logic of great practical use. Indeed, virtually all practically-used SAT-solvers are "resolution-based" in the sense that their underlying inference system is Resolution. In particular, when the SAT-solvers halt and state that a given formula is unsatisfiable, their trace produces a Resolution refutation. At the same time Resolution is very well studied from the proof complexity point of view. It is relatively well-understood what it is that makes a given CNF formula have short or long minimal Resolution refutations. This understanding could in principle be used to predict the (bad) performance of a SAT-solver on a given instance without actually running it, which could be particularly useful when the running time is predicted as astronomically big (e.g. 10^100 ms). In the first part of this course I plan to overview the width-method of Ben-Sasson and Wigderson to determine whether a given CNF formula does not have short Resolution refutations. As an application we will show that several explicitly given families of unsatisfiable CNF formulas of practical significance require exponentially long Resolution refutations. In the second part of the course I will motivate and discuss the applicability of the method to two provably stronger proof systems called Sherali-Adams and Sums-of-Squares, respectively.

More info at this link.