The PhD student will be working in the Mathematical Insights into Algorithms for Optimization (MIAO) group headed by Jakob Nordstrom (www.jakobnordstrom.se), which is active at both the University of Copenhagen and Lund University on either side of the Oresund Bridge. We are closely affiliated with the Basic Algorithms Research Copenhagen (BARC) centre, and are part of a world-leading environment in algorithms and complexity theory encompassing also the IT University of Copenhagen and the Technical University of Denmark (DTU). We aim to attract top talent from around the world to an ambitious, creative, collaborative, and fun environment. Using the power of mathematics, we strive to create fundamental breakthroughs in algorithms and complexity theory. While the focus in on foundational research, we do have a track record of surprising algorithmic discoveries leading to major industrial applications.
The MIAO research group has a unique profile in that we are doing cutting-edge research both on the mathematical foundations of efficient computation and on state-of-the-art practical algorithms for real-world problems. This creates a very special environment, where we do not only conduct in-depth research on different theoretical and applied topics, but where different lines of research cross-fertilise each other and unexpected and exciting synergies often arise. Much of the activities of the group revolve around powerful algorithmic paradigms such as, e.g., Boolean satisfiability (SAT) solving, Groebner basis computations, integer linear programming, and constraint programming. This leads to classical questions in computational complexity theory—though often with new, fascinating twists—but also involves work on devising clever algorithms that can exploit the power of such paradigms in practice.
Quite recently, we have made research breakthroughs on how to verify the correctness of state-of-the-art algorithms for combinatorial optimization. Such algorithms are often highly complex, and even mature commercial solvers are known to sometimes produce wrong results. Our goal is to design a new generation of certifying combinatorial solvers with so-called proof logging, meaning that the solvers output not only a solution but also a machine-verifiable mathematical proof that is easy to check and provides 100% formal guarantees that the claimed solution is correct. This work has only started, but our tool VeriPB (gitlab.com/MIAOresearch/VeriPB) can already handle techniques that have long remained beyond the reach of other approaches, and we have recently received prestigious AAAI '22 distinguished paper and SAT '22 best paper awards for our work.
With this call, we are mainly looking for a mathematically gifted PhD student with excellent programming skills to continue our ground-breaking work on certifying algorithms, funded by the Wallenberg AI, Autonomous Systems and Software Program (WASP). There is some flexibility as to what kind of research PhD students in the group pursue, though, and all candidates are welcome, both those who want to go deep into either theory or practice and those who are inspired by the challenge of bridging the gap between the two.
Our PhD positions are four-year full-time employed positions, but they usually (though not necessarily) include 20% teaching, in which case they are prolonged for one more year. The starting date is negotiable but should ideally be around the turn of the year 2022-2023 or earlier. All positions in the research group are fully funded, employed positions (including travel money) that come with an internationally competitive salary.
The application deadline is September 15. Please see http://www.jakobnordstrom.se/openings/PhD-Lund-220915.html for the full announcement with more information and instructions for how to apply. Informal enquiries are welcome and may be sent to jakob.nordstrom@cs.lth.se.
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************