Evaluating Nogood Management Heuristics in Constraint Programming Solvers

Abstract

Conflict analysis has become one of the key techniques behind the success of modern Constraint Programming (CP) solvers. In Lazy Clause Generation (LCG), conflicts are analysed to derive learned constraints, known as nogoods, which help the solver avoid revisiting infeasible regions of the search space. While learned nogoods can substantially improve search efficiency, maintaining large nogood databases introduces computational and memory overheads, making periodic removal of low-quality nogoods essential. Existing approaches largely rely on heuristics adopted from SAT solving, yet their comparative performance in the CP setting has not been systematically studied.

This thesis investigates the impact of nogood quality metrics and database reduction strategies on the performance of CP solvers. We analyse eight nogood quality metrics, including both established measures such as activity and Literal Block Distance (LBD), as well as new CP-specific metrics. We analyse their correlation with nogood usefulness, defined in terms of propagation behaviour across progressively stricter notions of utility. We find that all metrics can, to some extent, predict the usefulness of nogoods, and we identify four metrics for further study.

We then propose and evaluate a set of nogood management schemes that combine these metrics in different ways. Experiments across hundreds of optimisation and satisfaction instances from the MiniZinc Challenge show that a scheme retaining nogoods with either low LBD or high activity achieves the fewest conflicts and outperforms the default management strategy of the state-of-the-art solver Pumpkin. For anytime behaviour, incorporating the number of variables enables faster discovery of high-quality solutions. We further demonstrate that periodic database reductions are necessary, but that the choice of database size parameters involves a trade-off between finding solutions quickly and proving optimality. Finally, we find that differences in solver performance cannot be fully explained by schemes' ability to remove nogoods that cause few propagations and retain the active ones, suggesting avenues for future research.