Proof Logging for the Circuit Constraint

Proof logging in constraint programming is an approach to certifying a conclusion reached by a solver. To allow for this, different propagators must be augmented to produce justifications for any inferences they make, so that an independent proof checker can certify correctness. The Circuit constraint is used to enforce a Hamiltonian cycle on a set of vertices, e.g. for vehicle routing. Maintaining consistency for the Circuit constraint is hard, so various ad-hoc propagation techniques have been devised and implemented in solvers. We show that standard Circuit constraint inference rules can be efficiently justified within a pseudo-Boolean proof system, either by using a simple sequence of cutting planes steps or through a conditional counting argument.