Gecode: Guido Tack 'Constraint Propagation - Models, Techniques, Implementation'
Guido Tack is one of the Gecode team. His doctoral dissertation Constraint Propagation - Models, Techniques, Implementation (2009, as PDF) discuss constraint propagation in general, and give many examples of how propagation works in Gecode.
Abstract:
This dissertation presents the design of a propagation-based constraint solver. The design is based on models that span several levels of abstraction, ranging from a mathematical foundation, to a high-level implementation architecture, to concrete data structures and algorithms. This principled design approach results in a well-understood, correct, modular, and efficient implementation.The core of the developed architecture is the propagation kernel. It provides the propagation infrastructure and is thus crucial for correctness and efficiency of the solver. Based on a mathematical model as well as a careful design of the employed algorithms and data structures, the presented architecture results in an efficient and domain-independent kernel. Constraints are realized by propagators, and implementing a propagator is a challenging, error-prone, and time-consuming task. A practically useful solver must however provide a comprehensive propagator library. This dissertation introduces two techniques for automatically deriving correct and efficient propagators. Views generalize variables and are used to derive propagators from existing propagators. For constraints over set variables, propagators are derived from formal constraint specifications.
The presented techniques are the basis of Gecode, a production-quality, highly efficient, and widely deployed constraint solver. Gecode is the empirical evidence for success and relevance of the principled design approach of this dissertation.
Some comments
My interest right now is to step up from "just modeling" with decompositions to understand more about (and hopefully also write) "real" propagators, such as global constraints. Programming propagators is not possible in the MiniZinc language, the system I've used most the last year. Both Comet and Gecode has support for this, as well as the Java based systems Choco and JaCoP. Until now, I've only used Gecode's examples as a inspiration of and comparison to my own models, but I plan to start modeling in Gecode as well.
In view of this, Constraint Propagation - Models, Techniques, Implementation is a perfect book, explaning what propagations are and how they are implemented in Gecode. It is therefore great for understanding how Gecode works. It is also a modern introduction of the state-of-art techniques and implementation of propagators, which is one of the most important part in constraint programming.
Although quite theoretical in part (it is a dissertation in computer science after all), the book has a nice pedagogic pace and explains all core concepts very well, often with examples. Also, the proofs - there are lot of them - are often explained in "normal prose" before or after the proof, which makes it easy to follow the reasoning. (I didn't follow all the proofs, meaning that for some proofs I either didn't understand them or just glanced them through.)
It was very interesting to read the reasons, supported with benchmarks, behind some of the design decisions that was made in Gecode.
I enjoyed the "Related work" part at the end of a chapter or section, which related the discussed concepts to former research. Also, I liked that the Bibliography shows to what page a specific work is refered in the book.
I happened to read Modeling with Gecode just before Constraint Propagation - Models, Techniques, Implementation, and that was a good thing: Modeling with Gecode shows how to model in Gecode so the core concepts are laid out for the dissertation. (The Documentation page shows that a document "Programming with Gecode" is under preparation, which I look forward to read.)
Last, thanks to Mikael Zayenz Lagerkvist for recommending the book.