From Propagation to Proof Systems
This course is offered at the European Summer School of Artificial Intelligence (ESSAI 2026).
The webpage is still under construction. For now, its main purpose is to give prospective attendees an impression of the course and help them decide whether it is a good fit for their interests and background.
Lecturer
Dr Emir Demirović
Associate Professor, TU Delft
Personal Website
At a Glance
- Prerequisites: None
- Topics: Search, Propagation, Conflict Analysis, Certificates
- Format: Interactive lectures + dedicated textbook
- Takeaway: Understand how modern constraint solvers work internally
Overview
Constraint programming has undergone significant development over the past two decades. Techniques such as conflict analysis, nogood learning, lazy clause generation, certification, and proof systems have become fundamental components of many modern solvers. Beyond their practical impact, these developments have also provided new ways of understanding solver behaviour.
This course presents a unified introduction to modern constraint programming. Through interactive lectures and the accompanying textbook, the course serves both as an introduction to constraint programming and as a gateway to modern solver technology. Attendees learn how solvers operate, but also acquire the conceptual foundation needed to understand recent research papers and ongoing developments.
A central theme of the school is that modern constraint solvers can be understood not merely as search procedures, but as systems that progressively construct proofs of feasibility, infeasibility, and optimality.
Who is this course for?
The course is intended for students, practitioners, and researchers interested in understanding how constraint programming solvers work.
No prior knowledge of constraint programming is assumed. The course introduces the fundamental concepts from first principles while also covering modern solver techniques and recent developments from the research literature. It is designed to be accessible to newcomers while remaining relevant to participants interested in state-of-the-art methods and current research.
Teaching Philosophy
Concepts are introduced through examples and visual explanations. The emphasis is on developing algorithmic intuition and understanding how modern solvers reason. See draft slides as an example.
The lectures are designed with interactivity in mind, with an emphasis on discussion, active participation, and understanding.
The course follows the same philosophy as the accompanying textbook. Given the limited time available, the lectures focus on the central ideas and techniques, while the textbook develops the material in greater depth, provides the formal treatment, and discusses additional topics that cannot be covered during the lectures.
Each lecture follows approximately the same structure:
- 15 minutes: discussion and revision of previous material,
- 30 minutes: Part I,
- 15 minutes: break,
- 30 minutes: Part II.
Topics
The course has four main parts:
- Foundations of Constraint Programming;
- Propagation algorithms;
- Conflict Analysis and Learning;
- Certificates and Proof Systems.
We conclude with a discussion of current research directions and open problems.
Learning Outcomes
After completing the summer school, participants should be able to:
- Explain how modern constraint solvers operate internally.
- Design propagators and their explanations.
- Understand conflict analysis and learning.
- Connect solver behaviour to its mathematical foundations.
- Read and evaluate contemporary research papers in constraint solving.