Time: Wednesday, 22 February 2017, 3:00pm
Venue: SIC 305, C Block, 03rd Floor, Dept. of CSE, Kanwal Rekhi (KReSIT) Bldg.
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, e.g., geometric (pseudo-Boolean) techniques and what proof complexity can say about such extensions.
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).