Jakob Nordström
Photo: Kennet Rouna

Email: 
jn atsign di dot ku dot dk or 

jakob dot nordstrom atsign cs dot lth dot se 


Cellular:

+46 (0)70 742 21 98



Address in Copenhagen:

Datalogisk Institut, Københavns Universitet (DIKU)
Algorithms & Complexity Section
Universitetsparken 1, office 3109
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

At
the constraint programming conference
CP '23 in August, 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, 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, BreakIDkissatlow,
that we submitted to the
SAT Competition 2023
was the most successful solver in the competition, and would have won 1st prize
with last year's competition rules.
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…

Our pseudoBoolean proof checker
VeriPB
was used as
one of the official proof checkers
in the
SAT Competition 2023.

In December 2022 I gave a series of
lectures on pseudoBoolean solving and optimization
at the
Indian SAT+SMT Winter School
at IIT Madras in Chennai.
The video recordings have now been posted of
part 1,
part 2,
part 3,
and
part 4
of the tutorial, as well as of the
demo session.

Our paper
Certified
CNF Translations for PseudoBoolean Solving.
by
Stephan Gocht,
Andy Oertel, and myself from the MIAO group
joint with
Ruben Martins
received a
SAT '22
best paper award.

Our paper
Certified
Symmetry and Dominance Breaking for Combinatorial Optimisation
by
Stephan Gocht
and myself from the MIAO group
joint with
Bart Bogaerts
and
Ciaran McCreesh
received a
AAAI '22
distinguished paper award.
Academic affiliation and background
I am a professor at the
Department of Computer Science
at the
University of Copenhagen,
Denmark,
and also have a parttime 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 20112019.
During 20082010
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 May 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? Understanding
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 solved
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.
I am particularly interested in understanding combinatorial
optimization problems, which are of fundamental mathematical
importance but also have wideranging 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
