Certifying Bounds Propagation for Integer Multiplication Constraints

摘要

A constraint programming (CP) solver that implements proof logging will output a machine-checkable certificate of correctness alongside any result it obtains. This is useful for trusting claims of unsatisfiability or optimality, as well as for debugging and auditing solver implementations. Proofs can be constructed by having the solver log justifications for each inference it makes, and previous work has shown that many standard CP reasoning techniques can be efficiently justified using a pseudo-Boolean (PB) proof format. This paper extends PB justifications to propagators enforcing bounds consistency on multiplication and division constraints. We show that even though the proof system and checker operate only on linear inequalities over 0-1 variables, non-linear reasoning over bounded domains can be efficiently expressed as a sequence of PB proof steps. Additionally, we demonstrate that bespoke proof logging for bounds-consistency algorithms offers a clear advantage over constructing justifications by brute force.