This talk will survey research on analyzing the power and limitations of conflict-driven clause learning (CDCL) using tools from proof complexity. We will present som of the major results, but will also highlight many of the open problems that remain. Time permitting, we will also discuss how CDCL can be combined with algebraic or geometric (pseudo-Boolean) techniques and what proof complexity can say about such extensions.

Biographic Sketch for Jakob Nordström:

Jakob Nordström received his Master of Science in Computer Science and Mathematics at Stockholm University in 2001, and his PhD in Computer Science at KTH Royal Institute of Technology in 2008. During the academic years 2008-09 and 2009-10, he was a postdoctoral researcher at the Massachusetts Institute of Technology (MIT). Since 2011 he is working at the School of Computer Science and Communication at KTH Royal Institute of Technology, where he became an Associate Professor and received his Docent degree (habilitation) in 2015.

In 2006 he received the best student paper award at 38th ACM Symposium on Theory of Computing (STOC '06), and his PhD thesis received the Ackermann Award 2009 for "outstanding dissertations in Logic in Computer Science" from the European Association for Computer Science Logic. His research is funded by a Junior Researcher Position (2010) and a Breakthrough Research Grant (2012) from the Swedish Research Council as well as by a Starting Independent Researcher Grant from the European Research Council (2011).

In 1997-1998, Jakob Nordström served as a military interpreter at the Swedish Armed Forces Language Institute (Försvarets tolkskola), graduating as the best student of the 1998 class. In parallel with his studies and later his research, he has worked as a Russian interpreter, engaged among others for His Majesty the King of Sweden and the Swedish Prime Minister. He also has a Diploma in Choir Conducting with extended Music Theory from the Tallinn Music Upper Secondary School, Estonia. During the period 1994-1999, he was the artistic director of Collegium Vocale Stockholm, a vocal ensemble performing mainly Renaissance and Baroque music.