Photo: Maria Malmqvist |
|
News
- Our pseudo-Boolean proof checker VeriPB is now officially proposed as one of the proof checkers in the SAT Competition 2023.
- I am the main organizer of the extended reunion of the program Satisfiability: Theory, Practice, and Beyond running at the Simons Institute for the Theory of Computing at UC Berkeley from mid-March to mid-May.
- I am giving a plenary talk at the 2023 North American Annual Meeting of the Association for Symbolic Logic in March.
- I a co-organizing NordConsNet 2023, the annual workshop for the Nordic network for researchers and practitioners of constraint programming, in Odense, Denmark, on June 8-9.
- In December I gave a series of lectures on pseudo-Boolean solving and optimization at the Indian SAT+SMT Winter School at IIT Madras in Chennai.
-
In November I gave a video tutorial
Combinatorial solving with provably correct results
together with
Bart Bogaerts
and
Ciaran McCreesh.
Please check out the
video and/or the
slides!
(This is an updated version of the tutorial
Solving with
Provably Correct Results: Beyond Satisfiability, and Towards
Constraint Programming
that we gave in August at
CP '22
in Haifa.)
- Our paper Certified CNF Translations for Pseudo-Boolean Solving. by Stephan Gocht, Andy Oertel, and myself from the MIAO group joint with Ruben Martins received a SAT '22 best paper award.
- Our paper Certified Symmetry and Dominance Breaking for Combinatorial Optimisation by Stephan Gocht and myself from the MIAO group joint with Bart Bogaerts and Ciaran McCreesh received a AAAI '22 distinguished paper award.
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 May 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? Understanding 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 solved 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.
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. Recently, 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 best commercial tools sometimes produce wrong answers, but there has been no really principled way of addressing this problem. We are working on changing this. See the presentation of my research group for a slightly more detailed description.
Some links
- 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 (and webpages for the no longer active Theory reading group and the Complexity meetings that I organized while at KTH)
- Teaching
- Biographic sketch
- Résumé/industrial CV in PDF or HTML (last updated January 8, 2020) and academic CV in PDF (last updated August 25, 2022)