Lazy ad hoc Explanations for the Sum Constraint

Hybridization of CP and SAT combines the strengths of both paradigms, Constraint Programming (CP) and the Boolean satisfiability problem (SAT). This hybridization allows for the use of dedicated CP propagators paired with the powerful clause learning mechanism of SAT. In contrast to lazy clause generation, solvers based on lazy explanations extract a SAT explanation after each conflict and in particular after those detected by a CP propagator. In this article, we rely on a constraint-wise generic explanation algorithm to build new ad hoc explanation and reason extracting algorithms for the Sum constraint and some of its variants. Time complexity concerns fueled the elaboration of a relaxed version of our ad hoc algorithms, where the loss of a reasonable amount of clause accuracy yields better results. Finally, we conduct an empirical study on XCSP3 instances, where the efficiency of our ad hoc algorithms in reducing the size of generated clauses is clearly visible.