AllDifferent Inside Circuit: An Experimental Evaluation of Propagation Strength and Explanation Quality in Lazy Clause Generation

Abstract

Embedding AllDifferent within Circuit is standard practice for routing problems in Constraint Programming, but in a Lazy Clause Generation (LCG) solver this creates a tension: stronger propagators prune more but produce larger, more situation-specific explanations, yielding learned clauses that generalise poorly. AllDifferent and Circuit have only ever been studied separately, under incomparable conditions, leaving practitioners without an evidence-based choice of AllDifferent propagator inside Circuit in LCG. We close this gap with a systematic experimental evaluation of four propagator variants of increasing strength: a decomposed baseline, a matching-based conflict detector, a full GAC propagator, and a circuit-aware extension of GAC, implemented in the Pumpkin LCG solver and tested on structured geographic and unstructured random-graph benchmarks under fixed and activity-based search. Full GAC (V2) is the strongest choice overall, cutting runtime by up to two orders of magnitude by eliminating conflicting branches before the solver enters them; the theoretically stronger circuit-aware variant fails to improve on it because its extra pruning condition rarely fires in practice. V2's runtime advantage holds even where explanation quality favours weaker propagators, but narrows sharply on unstructured graphs as its clause reusability degrades, showing that propagation strength alone cannot predict LCG performance. We recommend full GAC as the default AllDifferent propagator for Circuit in LCG solvers.