acp-summer-school-2026
Lazy clause generation and beyond
This material was used as part of the ACP Summer School 2026.
Lecturer
Dr Emir Demirović
Associate Professor, TU Delft
Personal Website
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 an introduction to those recent advancements. 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.
Learning Outcomes
After completing this part of the summer school, participants should be able to:
- Explain concept of explanations as propositional justifications of propagations.
- Checkers as procedures to verify explanations.
- Propagation and checker algorithms for linear inequalities and all-different.
- Understand conflict analysis and learning.
- Connect solver behaviour to its mathematical foundations.