ERC-Funded PostDoc in Combinatorial Search & Optimization (Certifying Algorithms / Proof Logging)

The Faculty of Sciences and Bioengineering Sciences, Department Computer Science, is looking for a postdoctoral researcher. 

More concretely your work package contains: 

We are looking for an excellent researcher to strengthen Bart Bogaerts' research group on Knowledge Representation and Combinatorial Optimization. This research group is part of the Artificial Intelligence Lab, the oldest AI Lab on the European mainland, situated in Brussels, the heart of Europe. 

We are particularly looking for someone who can strenghten the recently-launched research line on proof logging (also known as certifying algorithms) for combinatorial optimization. In this line of research, the goal is to develop methods and algorthims that can guarantee with 100% certainty that the answers produced by a combinatorial optimizer are correct.
Recent breakthroughs in this direction have resulted in a distinguished paper award at AAAI 2022 [1] as well as a series of tutorials at major conferences (CP, IJCAI). A (short) online version of this tutorial can be found online [2]. 

The next iteration of the tutorial will be delivered at AAAI 2024 in Vancouver. 

You are expected to have experience with combinatorial optimization algorithms (e.g., SAT solving, constraint solving, MaxSAT, SAT modulo theories, Answer Set Programming, (Mixed) Integer Programming, ...) and are expected to contribute to go beyond the state-of-the-art of proof logging. In particular, we are interested in investigating how proof logging can be brought to the world of high-level modelling languages, rather than low-level solver languages. More info can be found in the abstract below. 

We offer a fully-funded postdoc position, initially for 12 months, but renewable and with expected duration of two or three years. The position comes with a competitive salary (academic salaries in Belgium are very competitive), as well as with travel budget. This is a pure research position, but it also comes with the possibility to participate in advanced teaching (while this is encouraged, it is not mandatory). 

The starting date is flexible; but preferrably around the summer of 2024. 

[1] https://www.bartbogaerts.eu/articles/2023/005-JAIR-CertifiedDominance/CertifiedSymmetryAndDominanceBreakingForCombinatorialOptimisation_JournalExtension.pdf
[2] https://www.youtube.com/watch?v=s_5BIi4I22w  

Project abstract:

The field of combinatorial optimization is concerned with developing generic tools that take a declarative problem description and automatically compute an optimal solution to it. Often, users specify their problem in a high-level, human-understandable formal language. This specification is first translated into a low-level specification a solver understands and subsequently solved. Thanks to tremendous progress in solving technology, we can now solve a wide variety of NP-hard (or worse) problems in practice. Moreover, these tools are increasingly used in real-life applications, including high-value and life-affecting decisions. Therefore, it is of utmost importance that they be completely reliable. The central objective of this proposal is to develop methodologies and tools with which we can guarantee with 100% certainty that the right problem has been solved correctly.

To achieve this ambitious objective, we will build on recent breakthroughs in proof logging, where solvers do not just output an answer, but also a proof (or certificate) of correctness. However, a major limitation of current techniques is that correctness is not proven relative to the human-understandable specification written by the user, but relative to the low-level translation that the solver receives, meaning that there is no guarantee that the solver is solving the original problem. In this project, we will investigate end-to end guarantees of correctness. When successful, this will have a major impact on the way combinatorial optimization software is developed, evaluated, and used: the proofs produced will enable (1) debugging, since proofs contain detailed information about where bugs occurred, (2) auditability, since proofs can be stored and checked by an independent third party, and even (3) rigorous evaluation of algorithmic improvements.

For this function, our Brussels Humanities, Sciences & Engineering Campus (Elsene) will serve as your home base.