Abstract: The effectiveness of the CDCL algorithm for SAT is complicated to understand, and so far one of the most successful tools for its analysis has been proof complexity. CDCL is easily seen to be limited by the resolution proof system, and furthermore it was 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 assumptions, only some of which are reasonable. In addition, in a setting where algorithms are expected to run in near-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.
Bio: Marc Vinyals is a researcher in theoretical computer science, currently visiting Memorial University of Newfoundland. His research interests include several areas of computational complexity, and in particular proof complexity, and the theory of satisfiability solving. Previously he was a graduate student at the KTH Royal Institute of Technology, supervised by Jakob Nordstrom, a postdoc at the Tata Institute of Fundamental Research and the Technion, hosted by Arkadev Chattopadhyay and Yuval Filmus respectively, and a docent (assistant/associate professor) at Saint Petersburg State University.
The CICS Theory Seminar is free and open to the public. If you are interested in giving a talk, please email Cameron Musco or Rik Sengupta. Note that in addition to being a public lecture series, this is also a one-credit graduate seminar (CompSci 891M) that can be taken repeatedly for credit.