Constraint Solving

Covers state-of-the-art algorithms used in practice to solve combinatorial optimisation problems, focusing on (Max)SAT and (lazy clause generation) constraint programming. The course offers an in-depth view of the algorithms including advanced techniques (e.g., propagator design, conflict analysis, decomposition approaches), alongside techniques that can certify the correctness of the output of the algorithms beyond reasonable doubt. The assignments include a notable programming component with Rust as the programming language. After the course, students will have a principled understanding of the algorithms and will be able to use that knowledge to design their own tailored approaches to solve combinatorial optimisation problems.