This thesis introduces Lazy Linear Generation (LLG), a novel conflict analysis and learning framework for Constraint Programming (CP) that incorporates cutting planes reasoning. By leveraging cutting planes, our approach learns potentially stronger linear constraints than traditi
...
This thesis introduces Lazy Linear Generation (LLG), a novel conflict analysis and learning framework for Constraint Programming (CP) that incorporates cutting planes reasoning. By leveraging cutting planes, our approach learns potentially stronger linear constraints than traditional clausal learning, allowing for more pruning of the search space while benefiting from strong CP propagation.
LLG generates linear explanations for both propagations and conflicts, which are then used in linear inequality-based conflict analysis. When cutting planes reasoning fails to derive a linear constraint, we employ Lazy Clause Generation (LCG) as a fallback mechanism. We present linear explanations for various arithmetic constraints, including less-than-or-equal, not-equal, absolute value, maximum, integer multiplication, truncating division, element, and reified constraints. Additionally, we introduce techniques for dynamically generating auxiliary Boolean variables to encode conditions within linear explanations.
We evaluate an LLG prototype on 952 benchmark instances, demonstrating a median conflict reduction of 10%, increasing to 60% for the 25th percentile. Our results confirm that linear inequalities enable stronger reasoning than clauses and show that integrating CP propagators with linear conflict analysis outperforms employing a fully linear model. Furthermore, we show that a clausal fallback mechanism is crucial when linear analysis fails.
While further research and engineering efforts are required for full integration into CP solvers, our findings underscore the potential of linear learning in CP, paving the way for more effective conflict analysis and solving.
