Explanation-Based Propagators for the Table Constraint
Comparing Eager vs. Lazy Explanations in Lazy Clause Generation Solvers
M. Aišparas (TU Delft - Electrical Engineering, Mathematics and Computer Science)
E. Demirović – Mentor (TU Delft - Algorithmics)
Maarten Flippo – Mentor (TU Delft - Algorithmics)
Benedikt 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
The table constraint is a fundamental component of constraint programming (CP), used to explicitly define valid value combinations for variables. In modern Lazy Clause Generation (LCG) solvers, constraints rely on explanations to justify value removals and enable efficient conflict analysis through nogood generation. However, table constraints have primarily been implemented using direct SAT encodings, such as the state-of-the-art Bacchus method, rather than explanation-based approaches. This paper introduces two types of explanation-based propagators for table constraints: eager explanations, generated during propagation, and lazy explanations, which adapt explanations to specific conflicts for more general nogoods. Experiments on MiniZinc benchmarks show that Optimized (Lazy) explanations reduce conflicts by an average of 23% across all problems and up to 64% for specific instances compared to the Bacchus encoding, while also reducing learned clause length by 46%. Although the current implementations incur a runtime penalty of up to 2x, these findings highlight the potential of explanation-based propagators to improve conflict resolution and search efficiency with further optimizations.