Solving Cumulative with Extended Resolution in LCG Solvers
Nothing is as important as proper explanations
M.A.A. Kienhuis (TU Delft - Electrical Engineering, Mathematics and Computer Science)
E. Demirović – Mentor (TU Delft - Algorithmics)
I.C.W.M. Marijnissen – Mentor (TU Delft - Algorithmics)
B.P. Ahrens – Graduation committee member (TU Delft - Programming Languages)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Lazy Clause Generation (LCG) Solving is a state-of-the-art technique for solving finite domain problems. The combination of powerful Constraint Programming (CP) propagators and Conflict Driven Clause Learning (CDCL) from the SAT domain enables both powerful inferences and learning from conflicts. Most research has focused on strengthening propagator explanations but has limited itself to remain within the standard LCG protocol, which only uses basic assignment and bound literals.
This thesis will focus on structurally extending this CDCL resolution protocol with new literals. We investigate the addition of two different literals to this protocol: a partial sum inequality literal and a precedence literal specifically for the cumulative constraint.
We verify previous work on the inequality literal, expand the test suite, and take a dive into metrics specifically related to extended resolution. We propose the novel idea of the cumulative literal, assessing its performance. We evaluate these extensions against both a baseline solver without protocol extensions and against each other across a range of hyper-parameters and search strategies.
Our results show that extending the protocol is not a guarantee for performance, the linear inequality extension remains powerful in some scenarios but fails to improve on a series of benchmarks whilst the cumulative literal shows no improvement at all. Moreover, we find that structurally based extended resolution introduces overlap between the literals in a nogood which negatively affects nogood quality.
These findings showcase that the research is far from done. A powerful technique exists but future research should consider additional infrastructure to make sure these techniques flourish at their fullest potential.