Articulation-Based Propagation for the Circuit Constraint

Abstract

Constraint Programming (CP) solvers rely on propagation algorithms to reduce the search space of combinatorial problems. For graph constraints such as the circuit constraint, infeasibility often depends on global connectivity properties that are difficult to capture using local propagation alone. In this paper, we investigate articulation-based graph reasoning for the circuit constraint in a Lazy Clause Generation (LCG) solver. We introduce propagation techniques based on articulation points and strong articulation points, using connectivity bottlenecks and strongly connected component structure to detect infeasible states and derive additional pruning. We further describe explanation-generation methods that allow these propagations to participate in clause learning within the LCG framework. To evaluate the practical usefulness of this reasoning, we implement the proposed propagators in an LCG solver and compare them against a baseline cycle-prevention propagator on graph instances with varying sizes and densities. The experiments show that articulation-based reasoning substantially reduces search effort and often improves runtime performance on sparse and moderately dense benchmark instances. These results demonstrate that global connectivity reasoning can provide practical benefits beyond traditional cycle-prevention propagation in modern LCG solvers.