Debugging unsatisfiable constraint models

The first constraint model that you write for a new problem is often unsatisfiable, and constraint modelling tools offer little support for debugging. Existing algorithms for computing Minimal Unsatisfiable Subsets (MUSes) can help explain to a user which sets of constraints are causing unsatisfiability. However, these algorithms are usually not aimed at high-level, structured constraint models, and tend to not scale well for them. Furthermore, when used naively, they enumerate sets of solver-level variables and constraints, which may have been introduced by modelling language compilers and are therefore often far removed from the user model. This paper presents an approach for using high-level model structure to, at the same time, speed up computation of MUSes for constraint models, present meaningful diagnoses to users, and enable users to identify different sources of unsatisfiability in different instances of a model. We discuss the implementation of the approach for the MiniZinc modelling language, and evaluate its effectiveness.