Modern constraint programming solvers incorporate SAT-style learning, where the decisions that lead to a failure are recorded and used to reduce the search. While this can yield dramatic reductions in solving time, there are also cases where learning does not improve or even hinders performance. Unfortunately, the reasons for these differences in behaviour are not well understood in practice.

This talk describes some of the techniques we have used to cast some light on the practical behaviour of learning solvers, mainly by profiling their execution to measure the impact of the learnt clauses. I will show that analysing a solver’s execution in this way can be useful not only to better understand its behaviour — opening what is typically a black box — but also to infer modifications to the original constraint model that can improve the performance of both learning and non-learning solvers.