I have moved to the Department of Computer Science (DIKU) at the University of Copenhagen and also have a parttime affiliation with the Department of Computer Science at Lund University. For now, my webpages still reside at KTH, and are being updated here, but this should change during 2020.
This also means that all openings mentioned below are either in Copenhagen or in Lund. The research group is active at both universities, and all members have offices in both Copenhagen and Lund.Open Positions
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 email—we can only hire for currently open positions as advertised in official announcements, and all applications must be made via the official recruitment system (as per instructions in the announcements).
Postdoc PositionsI need to hire postdocs in theoretical computer science. The application deadline is July 6, 2020. I then expect to advertise openings again in late 2020 or early 2021, both in theoretical computer science and in combinatorial optimization, with an intended starting date in the autumn of 2021. For the record, here is my latest announcements for a postdoc in SAT solving or combinatorial optimization more broadly — future announcements for applied postdocs are likely to look somewhat similar. Also, I am always interested in getting in contact with interesting candidates — and such contacts can result in positions opening earlier.
All postdoc positions in my research group are fully funded positions (including travel money) 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 Individual Fellowship within the EU Marie SkłodowskaCurie actions program to come and do a postdoc with me. There is currently an open call that closes September 9, 2020. 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. Please feel free to contact me if you want to discuss this.
PhD PositionsI am looking for PhD students in theoretical computer science and for a PhD student in SAT solving or combinatorial optimization more broadly. The application deadline is July 6, 2020. All PhD positions in my research group are fully funded positions with an internationally very competitive salary. I expect to advertise openings again in late 2020 or early 2021 with an intended starting date in the autumn of 2021. Future announcements are likely to be similar in spirit to those for the currently open positions. Also, I am always interested in getting in contact with interesting candidates — and such contacts can result in positions opening earlier.
Thesis ProjectsI would be interested in supervising students for thesis work on topics as briefly outlined below (but please note that the descriptions are in no way intended to be exhaustive). Please do not hesitate to send me an email to get more detailed information. (Note, however, that these projects are intended for students who are geographically close and can work on their thesis in the CopenhagenLund 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 SolvingGiven 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 socalled SAT problem is what is known as NPcomplete, 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, socalled SAT solvers, becoming a standard tool for solving realworld 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 NPcompleteness 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 01 Integer Linear ProgramsA 01 integer linear program (ILP) is a collection of linear constraints a_{1} x_{1} + a_{2} x_{2} + … + a_{n} x_{n} ≥ A where all a_{i} and A are integers and the variables x_{i} can only take values 0 or 1. Such 01 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 generalpurpose 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, pseudoBoolean solving, and mixedinteger 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:
