[Proof Complexity] Seminar Mon May 30 at 14:00 CET with Marc Vinyals: CDCL versus resolution

[Jakob Nordström]

Dear all,

On Monday May 30 at 14:00 CET we are having a seminar with Marc Vinyals titled "CDCL versus resolution". You find the abstract at the bottom of this message.

We will run this as a hybrid seminar at Lund University. Local participants are welcome to seminar room E:2116 at Ole Römers väg 3. Other participants are 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://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 video 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

**********

Monday May 30 at 14:00 in seminar room E:2116, Ole Römers väg 3, Lund University, and on Zoom
CDCL versus resolution
(Marc Vinyals)

The effectiveness of the CDCL algorithm, the one most used to solve SAT in practice, is complicated to understand, and so far one of the most successful tools for that has been proof complexity. CDCL is easily seen to be limited by the resolution proof system, and furthermore it has been shown to be equivalent to resolution, in the sense that CDCL can reproduce a given resolution proof with only polynomial overhead.

But the question of the power of CDCL with respect to resolution is far from closed. To begin with, the previous equivalence is subject to some assumptions, only some of which are reasonable in practice. In addition, in a world where algorithms are expected to run in linear time, a polynomial overhead is too coarse a measure.

In this talk we will discuss what breaks when we try to make the assumptions more realistic, and how much of an overhead CDCL needs in order to simulate resolution.


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