A Theoretical Framework for Constraint Propagator Triggering

CSP instances are commonly solved by backtracking search combined with constraint propagation. During search, constraint solvers aim to remove any literals (variable-value pair) that can be shown not to be part of any solution. This literal removal, called propagation, is the beating heart of modern constraint solvers. A significant proportion of the runtime of propagating constraint solvers is spent running propagation algorithms. Therefore any mechanism for reducing how frequently propagators are called leads directly to significant performance improvements. One family of popular techniques is dynamic triggering — these techniques aim to avoid invoking a propagator when it would remove no literals. While this technique has been successful in practice, it has not yet been studied theoretically. This paper provides a theoretical framework for understanding when dynamic triggering will be successful. In particular, we prove when a literal deletion does not require a propagator to be executed. To achieve this, we describe supports: a support for a constraint is a set of literals whose presence in a search state ensures that propagating the constraint will not remove any literals. Therefore running the propagator when a literal outside the support is deleted is a waste of time. By characterising supports and giving a definition of dynamic and static supports for the CSP, we provide the framework for a proper analysis. We show how the number of triggers required for different constraints varies widely. For some constraints, dynamic triggering allows very small supports, for others the number of required supports is provably large.