Photo: Kennet Rouna |
|
News
- In August, I will be lecturing on proof logging for automated reasoning and combinatorial solving with VeriPB at the ACP Summer School 2026 in Changchun, China.
-
Great news from the competitive events affiliated with the
SAT 2026 conference
at the
Federated Logic Conference (FLoC '26)
in Lisbon, Portugal!
- Our proof checker VeriPB was used as one of the checkers in the SAT Competition verifying machine-generated proofs that solvers had computed correct answers, allowing solvers to use the full range of advanced SAT solving techniques. VeriPB is also the only proof checker that is advanced enough to check proofs for the solvers in the Pseudo-Boolean Competition.
- In the SAT Competition 2026, we showed that just taking a previously existing SAT solver and doing nothing more than adding symmetry breaking with VeriPB proof logging support was enough to finish 3rd in the main track of the competition (and also in the subcategory for unsatisfiable instances).
- Somewhat intriguingly, the best solver in the subcategory of satisfiable instances in the SAT Competition main track, which was AI-generated, also used the VeriPB proof format to produce proofs (to be able to capture the high-level reasoning required for some crafted combinatorial problem instances).
- In the Pseudo-Boolean Competition 2026, the main non-certified tracks do not (yet) require proof logging. Still, our pseudo-Boolean solver RoundingSat had a good showing even when competing with solvers that do not have to produce proofs and therefore can (and typically do) use floating-point-based reasoning that can introduce errors. The best versions of RoundingSat placed 3rd in the decision track and 12th in the optimization track. As in previous years many of the other best solvers also made heavy use of the RoundingSat code base (five out of ten solvers in the top-10 list for the optimization track). In the certified tracks, RoundingSat had a very dominant performance, and different versions of the solver was awarded 1st, 2nd, and 3rd place in both the decision track and the optimization track.
- In July, I ran the 3rd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '26) together with Ciaran McCreesh. This workshop was organized as part of the workshop program at the Federated Logic Conference (FLoC '26).
- Congratulations to my PhD student Andy Oertel, who successfully defended his PhD thesis Certifying Combinatorial Optimization: A Unified Approach Using Pseudo-Boolean Reasoning in May!
- During the winter 2025/26 I taught the course Proof Complexity as a Computational Lens in Copenhagen and Lund together with Kilian Risse. More information, as well as links to video recordings and lecture notes, can be found on the course webpage.
- In January this year I organized the workshop Theory and Practice of SAT and Combinatorial Solving at the Banff International Research Station (BIRS) together with Olaf Beyersdorff, Daniela Kaufmann, and Ciaran McCreesh. You can watch video recordings of most talks on the BIRS workshop webpages.
Academic affiliation and background
I am a full 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, on 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 February 8, 2026)