Jakob Nordström

Picture of Jakob Nordstrom
Photo: Kennet Rouna
E-mail: jn at-sign di dot ku dot dk or
jakob dot nordstrom at-sign cs dot lth dot se
Cellular: +46 (0)70 742 21 98 / +45 28 78 38 11
Address in Copenhagen: Datalogisk Institut, Københavns Universitet (DIKU)
Algorithms & Complexity Section
Universitetsparken 1, office 3-1-09
2100 Copenhagen, DENMARK
Address in Lund: Institutionen för datavetenskap
Lunds universitet
Ole Römers väg 3, office 2130a
221 00 Lund, SWEDEN

News

  • A big welcome to our new PhD student Rui Ji!
  • In March 2024 I organized the workshop Proof Complexity and Beyond at Mathematisches Forschungsinstitut Oberwolfach together with Albert Atserias, Meena Mahajan, and Alexander Razborov.
  • At the constraint programming conference CP '23 in August 2023, former MIAO PhD student Stephan Gocht received the ACP Doctoral Research Award from the Association for Constraint Programming for his work on proof logging. Not only that, but our close collaborator Ciaran McCreesh received the ACP Early Career Researcher Award, among other things for our joint work on proof logging, and Ciaran and his PhD student Matthew McIlree got the CP 2023 best paper award for their work on proof logging for constraint programming solvers using VeriPB. So, all in all, a pretty good week for certifying combinatorial solvers… Big congrats to Stephan, Ciaran, and Matthew!
  • At the AI conference IJCAI '23 in August 2023, I gave a tutorial Combinatorial Solving with Provably Correct Results on VeriPB proof logging joint with Bart Bogaerts and Ciaran McCreesh. (See the VeriPB YouTube tutorial from the autumn of 2022 with accompanying slides for an earlier version.)
  • The SAT solver with VeriPB proof logging, BreakID-kissat-low, that we submitted to the SAT Competition 2023 was the most successful solver in the competition, and would have won 1st prize had the competition rules been like in previous years. With VeriPB proof logging we can support advanced SAT solving techniques that have previously been out of reach for the standard SAT proof logging format, thus increasing the power of the solver exponentially. However, our proof checking is still not as fast as in the highly optimized checkers for the standard format that have been used for the last decade, and some of our proofs were not verified within the required time limits. Therefore, we instead had to to content ourselves with receiving an honorary 1st prize. We know how to make our toolchain for formal verification of proofs more efficient, though, and are working on it for next year—and it is already clear what is the future of efficient, powerful, fully general SAT proof logging…

Academic affiliation and background

I am a professor at the Department of Computer Science at the University of Copenhagen, Denmark, and also have a part-time affiliation with the the Department of Computer Science at Lund University.

Prior to moving to Copenhagen and Lund, I worked at KTH Royal Institute of Technology as an assistant professor and then associate professor during the years 2011-2019. During 2008-2010 I was a postdoc at the Computer Science and Artificial Intelligence Laboratory at the Massachusetts Institute of Technology hosted by Madhu Sudan. Before that I was a PhD student of Johan Håstad in the Theory Group at KTH. where I defended my PhD thesis in 2008. Please see my biographic sketch for more information.

About my research

Computers are everywhere today—at work, in our cars, in our living rooms, and even in our pockets—and have changed the world beyond our wildest imagination. Yet these marvellous devices are, at the core, amazingly simple and stupid: all they can do is to mechanically shuffle around zeros and ones. What is the true potential of such automated computational devices? And what are the limits of what can be done by mindless calculations? Finding answers to this kind of questions is ultimately what my research is about.

Computational complexity theory gives these deep and fascinating philosophical questions a crisp mathematical meaning. A computational problem is any task that is in principle amenable to being solved by a computer—i.e., it can be worked out by mechanical application of mathematical steps. By constructing general, abstract models of computers we can study how to design efficient methods, or algorithms, for solving different tasks, but also prove mathematical theorems showing that some computational problems just cannot be solved efficiently for inherent reasons (meaning that is impossible to design algorithms for them that are as efficient as we would like).

I am particularly interested in understanding combinatorial optimization problems, which are of fundamental mathematical importance but also have wide-ranging applications in industry. My goal is, one the one hand, to prove formally that many such problems are beyond the reach of current algorithmic techniques, but also, on the other hand, to develop new algorithms that have the potential to go significantly beyond the current state of the art. Recently, I have also been doing research on how complexity theory can be harnessed to produce certificates that algorithms are actually computing correct results. It is an open secret in combinatorial optimization that even the best commercial tools sometimes produce wrong answers, but there has been no really principled way of addressing this problem. We are working on changing this. See the presentation of my research group for more information.

Some links

Published by: Jakob Nordström <jn~at-sign~di~dot~ku~dot~dk>
Updated 2024-04-05