Postdoc in Combinatorial Search & Optimization (SAT / CP / SMT / MIP) KU Leuven in Canada

Postdoc in Combinatorial Search & Optimization (SAT / CP / SMT / MIP) at KU Leuven, Belgium, in the research group of Prof. dr. Bart Bogaerts within the Knowledge Representation and Combinatorial Optimization group of the Declarative Languages and Artificial Intelligence (DTAI) section, Department of Computer Science.

The position focuses on research in combinatorial optimization and declarative problem solving, with an emphasis on building reliable tools that translate high-level problem descriptions into solver-ready formulations and then compute optimal solutions correctly. The project highlights recent advances in proof logging and machine-verifiable certificates, aiming for end-to-end correctness guarantees relative to the original user specification, not just the translated model. A second major theme is explainability: developing human-understandable explanations for why a solution is optimal, why no solution exists, or why a problem has a unique solution.

This is a strong fit for researchers interested in SAT solving, constraint programming, MaxSAT, SMT, Answer Set Programming, mixed integer programming, and related areas of combinatorial search and optimization. The advertised work also connects to auditability, debugging, rigorous evaluation of algorithms, and trustworthy AI-style decision support in high-impact applications.

The role is a fully funded postdoc position with an expected duration of 2 years (negotiable) and includes sufficient travel budget. Applicants must hold a PhD in computer science or a closely related field before the start date and have strong expertise in combinatorial optimization algorithms. Proficiency in English is required.

Application deadline: 2026-10-30.

How to apply: submit your application through the KU Leuven job portal using the provided application link. For questions, contact Prof. dr. Bart Bogaerts at [email protected].