[Proof Complexity] MIAO seminar Thu Apr 25 at 16:00 CEST with Mathias Fleury: Verifying a SAT solver from ground up

[Jakob Nordström]

Dear all,

On Thursday April 25 at 16:00 CEST (note the time!) we will have the opportunity to enjoy a seminar with Mathias Fleury from Albert-Ludwigs-Universität Freiburg, who will give a talk titled "Verifying a SAT solver from ground up". You find the abstract at the bottom of this message.

We will run this as a hybrid seminar at Lund University. Local participants are warmly welcome to seminar room E:1426 at Ole Römers väg 3. Other participants are equally warmly welcome to join virtually 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://youtube.com/@MIAOresearch 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 a self-contained 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 https://jakobnordstrom.se/miao-seminars/. In particular, note that this week we also have a seminar on Tuesday April 23 with Daniel Neuen titled "Compressing CFI graphs and lower bounds for Weisfeiler-Leman refinements" and another seminar on Friday April 26 with Markus Hecher titled "A crash course in answer-set programming". 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

**********

Thursday Apr 25 at 16:00 CEST (note the time!) in seminar room E:1426, Ole Römers väg 3, Lund University, and on Zoom
Verifying a SAT solver from ground up
(Mathias Fleury, Albert-Ludwigs-Universität Freiburg)

In this seminar, I will present my verified SAT solver, IsaSAT, starting from an abstract CDCL calculus, through a more pragmatic version PCDCL, down to reasonably efficient code using a refinement chain. In the first part of the presentation, I will present the general approach and the second part, I will show more details how the refinement is done and what are the critical parts where performance is lost.


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