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

Albert Atserias (Universitat Politècnica de Catalunya).

Course Summary | About the lecturer | Location and schedule | Materials and problems

Course summary:

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.

About the lecturer:

Albert Atserias is an Associate Professor at Universitat Politenica de Catalunya (UPC), Barcelona. He received an engineering degree in computer science in 1997 from UPC, an M.Sc. in computer science from the University of California at Santa Cruz (UCSC) in 1999, a Ph.D. in computer science from UPC in 2002, and a Ph.D. in computer science from UCSC also in 2002. His research interests span computational complexity, combinatorics, and applications of logic to computer science. More specifically, he has contributed to propositional proof complexity, descriptive complexity, and finite model theory. His work is known for building bridges between the two traditional tracks of theoretical computer science (track A and track B). Among his best known achievements is the connection he established between the method of Ehrenfeucht-Fraisse games for finite model theory and the lower bound methods for propositional proof systems in proof complexity. In 2002 he received the Kleene Award for best student paper at the LICS conference for pioneering work in this area. More recent work of 2012 further connects Ehrenfeucht-Fraisse games and lift-and-project methods in mathematical programming, and their associated proof systems. Since June 2015 he is the principal investigator of a grant funded by the European Research Council (ERC) that develops this line of research.

Location and schedule:

MIMUW building, rooms 3160 and 2180.

Thursday, January 25 Room 3160
14:15 - 15:45 lecture
15:45 - 16:00coffee and cake
16:00 - 17:00 class
Friday, January 26 Room 2180
14:15 - 15:45 lecture
15:45 - 16:00 coffee and cake
16:00 - 17:00 class
Saturday, January 27 Room 2180
10:15 - 11:30 lecture
11:30 - 11:45 coffee and cake
11:45 - 13:00 class

Materials and problems
Bullet notes, including problems