NFA vs DFA Representations for the Regular Constraint in Lazy Clause Generation: A Comparative Evaluation

Abstract

The regular constraint enforces that a sequence of variables forms a word accepted by
a finite automaton, and is widely used in constraint programming (CP) for rostering,
timetabling, and puzzle solving. While non-deterministic finite automata (NFAs) offer
more compact representations than deterministic finite automata (DFAs), their relative performance within Lazy Clause Generation (LCG) remains underexplored. We
adapt existing NFA and DFA-based LCG propagators, using a decomposition-based
propagator as a baseline, and evaluate all three under identical solver conditions across
instances stratified by DFA-to-NFA state blowup. At low blowup, NFA and DFA
solve times are closely matched. At medium blowup, NFA remains faster by a factor of approximately three, and at high blowup it is approximately 22× faster than
DFA, with DFA never clearly preferable. Although both compute the same filtering
under generalised arc consistency, they can justify prunings differently, and thus are
not guaranteed to explore identical search trees. Despite this potential for divergence,
clause metrics are identical between NFA and DFA across every blowup bin, a result
that may generalise more broadly but warrants further investigation. We also show
that the currently used greedy explanations are close to optimal, within one percent
of the exact minimum overall and within a few percent for any individual problem
type measured. We thus provide the first direct evidence that NFA’s compactness
advantage carries over to propagation performance under LCG, establishing it as the
default representation for the regular constraint in CP with LCG.