Certifying Combinatorial Solving Using Cutting Planes with Strengthening Rules
summary
Claims that cutting planes with redundance-based strengthening plus explicit witnesses lets off‑the‑shelf solvers emit compact, machine‑checkable proofs for many combinatorial problems beyond SAT. Uses 0/1 integer linear inequalities, extension variables and a new dominance rule to certify parity, cardinality and graph‑problem reasoning; implements proof logging and verification and reports order‑of‑magnitude faster checking than prior encodings. Works empirically on many benchmarks but leaves symmetric‑learning and some end‑to‑end translations to be formally verified.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 2:30The Problem
- 3:40Formal Verification
- 4:57Preflogging
- 14:22Does this exist
- 20:44Outline
- 21:31Subproblem
- 21:52Conflict Driven Close Learning
- 26:58Proof Vlogging
- 29:15Redundancy Rules
- 36:08Pseudo Boolean Inequalities
- 39:23Extension Variables
- 40:59Parity Reasoning
- 44:52Symmetries
- 47:10Optimization Problems
- 49:06Proof System
- 55:27Deleting
- 57:09Wrapup
related talks
18mOn the Verification of a Subgraph Construction Algorithm
01h 17mInapproximability of Constraint Satisfaction Problems III
01h 30mInapproximability of Constraint Satisfaction Problems II
01h 25mInapproximability of Constraint Satisfaction Problems IV
56mApproximate Counting II
01h 08mThe Simple, Little and Slow Things Count: On Parameterized Counting Complexity
01h 01mThe Gospel According to TCS
58mDichotomy Theorems for Counting Problems II