The Width Method for Resolution and SumsofSquares 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 practicallyused SATsolvers are "resolutionbased" in the sense that their underlying inference system is Resolution. In particular, when the SATsolvers 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 wellunderstood 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 SATsolver 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 widthmethod of BenSasson 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 SheraliAdams and SumsofSquares, 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 EhrenfeuchtFraisse 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 EhrenfeuchtFraisse games and liftandproject 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.



Materials and problems
Bullet notes, including problems