Proof Logging for Constraint Programming
summary
A pseudo-Boolean proof system, VeriPB, records backtracking search by emitting negations of decision sequences as RUP steps and extends with cutting-planes to certify propagators; it uses reverse unit propagation as a compact rule and on‑the‑fly direct and bitwise (2's complement) encodings plus reified auxiliaries to represent multi‑valued CP variables. The all‑different propagator is certified by extracting a hull violator, summing at‑most‑one and at‑least‑one constraints via cutting planes to derive a contradiction (five‑variable example generalizes), and a Glasgow prototype implements these proofs for core CP constraints and integration with existing VeriPB tooling.
AI-written summary · about
chapters (8)
- 0:00Introduction to proof logging
- 2:00Proof logging for CP solvers
- 4:07Encoding strategies
- 6:11Integrating encodings and constraints
- 9:31Maintaining proof invariants
- 12:16Proof logging for propagators
- 18:08Open challenges and future work
- 25:09Q&A session
related talks
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
01h 09mProofs - Practice 1
19mAutomated Verification of Fundamental Algebraic Laws
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
41mLiving inside a Theorem Proving Universe
01h 13mA Zero-Knowledge PCP Theorem
30mRelatively Complete Verification of Probabilistic Programs
17mIntroduction of PROLEG (PROlog-based LEGal reasoning support system)