[Proof Complexity] MIAO seminar Friday Sep 30 at 14:00 CET with Albert Atserias: Towards an algorithmic theory of proof complexity

[Jakob Nordström]

Dear all,

Next Friday September 30 at 14:00 Albert Atserias from Universitat Politècnica de Catalunya will give a talk titled "Towards an algorithmic theory of proof complexity". You find the abstract at the bottom of this message.

This will be a video seminar at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming MIAO seminars can be found at http://www.jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

Friday Sep 30 at 14:00 on Zoom
Towards an algorithmic theory of proof complexity
(Albert Atserias, Universitat Politècnica de Catalunya)

A possibly unexpected by-product of the mathematical study of the lengths of proofs, as is done in the field of propositional proof complexity, is, I claim, that it may lead to new algorithmic insights. To explain this, I will first recall the origins of proof complexity as a field. Then I will explain why our current understanding of certain proof systems could lead to new algorithms. The key to this is that, for several proof systems of practical use, the class of tautologies with low-complexity proofs comes with a tight semantic characterization. Concretely, the characterization states that a tautology fails to have a low-complexity proof precisely when it is locally satisfiable, in a precise technical sense of the term. One immediate derivative of this is that, for those proof systems that admit such semantic characterizations, the statement that a formula has a low-complexity proofs has: (1) low-complexity certificates when true, and (2) low-complexity refutations when false. We illustrate the point by discussing the recently discovered subexponential-time algorithm that distinguishes the graphs that are 3-colorable from those that are not even n^eps-colorable in time exp(n^{1-2eps}), which beats all previously known approaches.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se