|
Photo: Kennet Rouna |
|
News
- I am looking for a PhD student who will help us go even further beyond the state of the art in provably correct computation with certifying algorithms (as per this tutorial) or possibly in combinatorial solving and optimization (as explained in this series of tutorials.) This is a pretty unique opportunity if you have a strong background in both mathematics and programming and wish to combine the two. The application deadline is January 17, 2025.
- The Department of Computer Science at Lund University invites applications for a tenure-track assistant professorship in the foundations of computer science with a focus on logic and automated reasoning. The application deadline is January 8, 2025.
- We have now published videos and slides from the 1st International Workshop on Solving Linear Optimization Problems for Pseudo-Booleans and Yonder (SLOPPY '24) held at Lund University in November 2024 as well as from the 1st International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '24) held at the University of Copenhagen in May 2024.
-
Great news from the
International Conference on
Theory and Applications of Satisfiability Testing
in August 2024!
- For the second year, VeriPB was used as one of the proof checkers in the SAT Competition, allowing solvers to use the full range of advanced solving techniques. We showed that just taking a previously existing SAT solver and doing nothing more than adding this proof logging support was enough to get a silver medal in the competition.
- VeriPB was also used in the Pseudo-Boolean Competition, where our solver RoundingSat was one of the contestants. In the optimization track, 9 out of the 12 best solvers were based on the RoundingSat code base, and the original RoundingSat solver was the best one for both decision and optimization problems when certificates of correctness were required.
- Former MIAO group PhD student Stephan Gocht was a runner-up for the SAT Association Fahiem Bacchus PhD Award in Satisfiability.
- And as another sign of the impact of our research, the SAT best paper was dedicated to a theoretical analysis of the proof system developed for VeriPB, while the best student paper investigated ways of improving RoundingSat.
See the article at the Wallenberg AI, Autonomous Systems and Software Program webpages for a bit more details.
- In March 2024 I organized the workshop Proof Complexity and Beyond at Mathematisches Forschungsinstitut Oberwolfach together with Albert Atserias, Meena Mahajan, and Alexander Razborov.
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. In the last few years, 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 most mature optimization tools in academica and industry sometimes produce wrong answers, but there has been no really principled way of addressing this problem. Our work has started to change this state of affairs. See the presentation of my research group for more information.
Some links
- Mathematical Insights into Algorithms for Optimization (MIAO) research group
- Open positions
- Publications
- Software
- Slides (and sometimes video) for some presentations
- MIAO seminars with some recordings posted on the MIAO Research YouTube channel youtube.com/@MIAOresearch
- Teaching
- Biographic sketch
- Curriculum Vitae: long version and short version (last updated October 1, 2024)