2025
Certifying Bounds Propagation for Integer Multiplication Constraints
AAAI 2025technical
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 ca…