Zoom seminar Thu Oct 30 at 13:15 CET: Proof complexity as a computational lens

[Jakob Nordström]

Dear colleagues,

With apologies for the short notice (and also for any multiple copies), this is just to announce a seminar this Thursday October 30 at 13:15 CET titled "Proof complexity as a computational lens" and given by yours truly. You find the abstract at the bottom of this message. This will be a video seminar at https://lu-se.zoom.us/j/61925271827 (unless you happen to be in Lund).

This is expected to be a ca-2-hour tutorial-style seminar, which will double as the first introductory lecture of a seminar course with the same name that will be given in Copenhagen and Lund during the winter of 2025/26. The course will focus on the part of proof complexity that can also be used to analyze SAT solvers, Gröbner basis algorithms, 0-1 linear programming solvers, and other combinatorial solving algorithms. More about the course can be found at https://jakobnordstrom.se/teaching/proofcplx25/ , but please feel free to reach out if you are interested in information about, e.g., how to follow lectures remotely.

Please feel free to share this information with colleagues who you think might be interested. As usual, we are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend. More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ .

Best regards,
Jakob Nordström

**********

Thursday Oct 30 at 13:15 (note the time!) in seminar room E:2116, Ole Römers väg 3, Lund University, and on Zoom
Proof complexity as a computational lens
(Jakob Nordström, University of Copenhagen and Lund University)

This seminar will give an overview of proof complexity with a focus on "algorithmically relevant" proof systems that, besides offering interesting objects for mathematical study, can also be used to analyze real-world combinatorial solving algorithms. We will talk about proof systems [and corresponding algorithms] such as resolution [DPLL and conflict-driven clause learning SAT solving], Nullstellensatz and polynomial calculus [linear algebra and Gröbner basis computations], and cutting planes [pseudo-Boolean solving and 0-1 integer linear programming]. Time permitting, we will also discuss briefly proof systems such as Sherali-Adams and sum of squares [linear programming and semidefinite programming hierarchies], stabbing planes [0-1 ILP], and extended resolution [SAT pre- and inprocessing].

Speaker bio: Jakob Nordström is a professor at the University of Copenhagen, Denmark, with a side affiliation at Lund University on the Swedish side on the Oresund Bridge. He started his research career in computational complexity theory, but these days his activities also include (in addition to frequent, long train commutes) work on how to leverage complexity theory to build more efficient combinatorial solvers and how to develop proof logging methods for applications such as SAT solving, SAT-based optimization, graph solving, constraint programming, and integer linear programming using the VeriPB tool.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se