Jakob Nordström / Open positions

Open Positions

The MIAO research group is active at both the University of Copenhagen and Lund University, and all members have offices in both Copenhagen and Lund.

Please feel free to drop me a line if you have any questions about any of the openings advertised (or not advertised) on this webpage.

Note, however, that we cannot accept applications via e-mail — we can only hire for currently open positions as advertised in official announcements, and all applications must be made via the official recruitment systems (as per instructions in the announcements).

Faculty Positions

We currently have no openings in theoretical computer science at the Department of Computer Science at the University of Copenhagen, but expect to hire in TCS going forward. Please do not hesitate to contact me and/or Mikkel Thorup if you are interested in learning more about opportunities to join one of the most exciting and dynamic TCS environments in Europe!

We currently have no open faculty positions in algorithms or complexity theory at the Department of Computer Science at Lund University, but this webpage will be updated as we publish new openings.

Postdoctoral Positions

We will be advertising openings again in the autumn of 2022, both in theoretical computer science and in combinatorial optimization, with an intended starting date in the autumn of 2023. More detailed information will be posted as soon as it is available. The official job advertisement will be posted Real Soon Now™ — hopefully before the end of November.

All postdoc positions in my research group are fully funded, employed positions (including travel money) that come with an internationally competitive salary.

If you instead want to start collecting grants to list on your CV, you can also try to apply for an postdoctoral fellowship within the EU Marie Skłodowska-Curie actions program to come and do a postdoc with me. The next call is expected to open in April 2023 and have a deadline in August-September 2023. I would particularly welcome applications from strong candidates who want to work in computational complexity theory, SAT solving, integer linear programming, constraint programming, or some mix of these areas.

Another opportunity is to apply for a postdoc position within the framwork of the postdoc fellowship program of the Danish Data Science Academy. The deadline is March 19, 2023.

Please feel free to contact me if you want to discuss this.

PhD Positions

I am looking for a PhD student in theoretical computer science and/or combinatorial optimization at Lund University. The application deadline is January 12, 2023. The starting date is flexible, but should ideally be during the first half of 2023, or at the latest in August/September 2023.

We will advertise PhD openings in Copenhagen in the late autumn or winter of 2022 with an intended starting date in the autumn of 2023. The webpage will be updated as soon as we know more about this. The official job advertisement will be posted Real Soon Now™ — hopefully before the end of November. Just for your information, future announcements are likely to be fairly similar to our latest call in Copenhagen (but note that it is no longer possible to apply for these particular positions—the webpages are being kept for archival purposes only).

In Copenhagen, it is also possible to apply for a PhD position within the framwork of the PhD fellowship program of the Danish Data Science Academy. The deadline is March 19, 2023.

All our PhD positions are fully funded, employed positions (including travel money) that come with an internationally very competitive salary.

Thesis Projects

I would be interested in supervising students for thesis work on topics as briefly outlined below. Please note that the descriptions are in no way intended to be exhaustive. You can send me an e-mail to get more detailed information with an up-to-date list of more concrete proposals. (Note, however, that these projects are intended for students who are geographically close and can work on their thesis in the Copenhagen-Lund area. There is no dedicated funding available to support foreign students to come to Denmark or Sweden.)

These projects are intended to give students a feel for what research in computer science is like, while at the same time focusing on concrete problems of both theoretical and practical importance. Apart from the thesis work itself, the intention is that the results of successful thesis projects should also be exciting enough to be published as (parts of) papers in leading scientific conferences and/or journals in the field (within the framework of the research outlined here).

Formula Hardness and SAT Solving

Given a formula in propositional logic, is it possible to set its variables in such a way that the formula is satisfied? This simple looking problem has been on centre stage in theoretical computer science ever since the field got started some 40 years ago, and has been named as one of the Millennium Prize Problems comprising some of the major challenges for all of mathematics in the 21st century. Today, students of computer science worldwide learn in their introductory algorithms and complexity courses that this so-called SAT problem is what is known as NP-complete, and therefore is very, very hard in practice.

Interestingly, practioners take a somewhat different view. During the last 20 years, SAT has developed from a problem of mainly theoretical interest into a practical approach for solving a wide range of applied problems. Enormous progress in performance has led to satisfiability algorithms, so-called SAT solvers, becoming a standard tool for solving real-world problems with millions of variables in the context of, for example, hardware and software verification, electronic design automation, artificial intelligence, operations research, and bioinformatics. The theory of NP-completeness did not quite go away, however — for all these SAT solvers there are also known examples of tiny formulas with just a couple of hundred variables that make them fail miserably.

How can modern SAT solvers be so good in practice? How can one know for a particular formula whether it will be hard or easy? Can we extend SAT solvers with new methods of reasoning to make them potentially even more powerful than the best solvers today? These are the kind of questions we want to study in these Master's thesis projects, using a mix of theoretical research and practical experiments.

Solving 0-1 Integer Linear Programs

A 0-1 integer linear program (ILP) is a collection of linear constraints

a1 x1 + a2 x2 + … + an xn ≥ A

where all ai and A are integers and the variables xi can only take values 0 or 1. Such 0-1 ILPs can be used to model a vast range of problems in computer hardware construction and verification, software analysis, scheduling, logistics, disaster management, bioinformatics, artificial intelligence, et cetera.

Most of these problems are known to be computationally very, very challenging from a theoretical point of view — it is widely believed that it is impossible to design general-purpose algorithms that will always run fast and produce correct solutions — but in practice there are very efficient combinatorial optimization solvers that try to exploit the structure of concrete problems to find shortcuts, and use an array of sophisticated heuristics to do so. For most of these heuristics there is an almost complete lack of rigorous scientific understanding of when and why they work well or fail, however.

Another intriguing fact is that recent research on combining methods from Boolean satisfiability (SAT) solving, pseudo-Boolean solving, and mixed-integer linear programming (MIP) has shown that adding together solving techniques from these different areas can lead to major improvements in performance.

A project in this area could involve:

  • Reading up on the literature on SAT solving and pseudo-Boolean solving, focusing on conflict-driven search.
  • Identifying one or a couple of aspects of combinatorial solvers to investigate further, such as, for instance, (a) how to vary the methods for learning constraints during so-called conflict analysis, (b) how to assess the quality of the linear constraints learned (when prioritizing which ones to keep or throw away), (c) how to choose variables for branching, (d) how to perform restarts during search, (e) how to integrate different MIP solving techniques such as linear programming relaxations, et cetera.
  • Implementing some different heuristics for the aspect(s) identified, and run experiments on benchmark 0-1 ILPs to see how solver performance is affected (which can be measured in terms of running time, search quality, memory usage, and possibly also other parameters).
  • For the benchmarks emanating from research papers in computational complexity theory, possibly compare the practical performance with the known theoretical properties of these benchmarks to see if and how they match up.
Published by: Jakob Nordström <jn~at-sign~di~dot~ku~dot~dk>
Updated 2022-11-22