This paper2 details the stages of building a substantial, carefully specified, fully tested and fully operational university and school timetabling system. This is reported as a case study in applying Constraint Satisfaction techniques. The emphasis is on the software engineering aspects of the problem. That is, Constraint Satisfaction problems are expressed in a language more familiar to the formal software engineering community. Moreover, this language is used to formulate domain constraints and heuristic information. In addition to that, the user's needs are looked at more closely. For instance, the system supplies indications useful for relaxing or reformulating the constraints of the problem when a solution satisfying these constraints is impossible to produce. This has a value in bringing Constraint Satisfaction one-step closer to formal specification, program verification and transformation.
Abdulwahed M. Abbas, Edward P. K. Tsang