Talk by Jakob Nordström

On Tuesday 4 September 2018, Associate Professor Jakob Nordström from KTH Royal Institute of Technology in Stockholm, Sweden, will give a talk at DIKU.


Divide and Conquer: Towards Faster Conflict-Driven Pseudo-Boolean Solving


Although Boolean satisfiability (SAT) is an NP-complete problem, and is hence expected to require exponential time in the worst case, the last 20 years have witnessed dramatic improvements in applied SAT solvers. Today solvers based on conflict-driven clause learning (CDCL) are routinely used to solve instances with millions of variables in a wide range of application areas.

One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean reasoning (a.k.a. 0-1 integer linear programming), but so far the promise of exponential gains in performance has mostly failed to materialize --- the increased theoretical strength seems hard to harness algorithmically, and most often CDCL-based methods are still superior.

In this talk, we will discuss conflict-driven search and how to generalize it to pseudo-Boolean linear constraints. We will survey the "classic" method in [Chai and Kuehlmann '05], and then describe a new, different approach from [Elffers and Nordström '18]. We will also try to highlight some of the obstacles that remain along the path to truly efficient pseudo-Boolean solvers.

The talk will be self-contained, so no prior knowledge of applied SAT solving is assumed.


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 Electrical Enginering and Computer Science (previously 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 mainly funded by a Breakthrough Research Grant (2012) and a Consolidator Grant (2016) from the Swedish Research Council, a Starting Independent Researcher Grant from the European Research Council (2011), and (joint with Johan Håstad and Per Austrin) a Research Project with High Scientific Potential Grant from the Knut and Alice Wallenberg Foundation (2016).