The Proof Complexity of Integer Programming
summary
Introduces Stabbing Planes as a proof system modeling branch-and-cut and proves a constructive translation that, when each query has bounded-coefficient, converts a size-S stabbing‑planes refutation into a quasi-polynomial simulation by Cutting Planes with a diameter-dependent blowup. Key tools are Schrijver’s face‑lifting lemma, Nisan–Wigderson style variable compression and pebbling/Tseitin hardness; surprising facts: Tseitin admits quasi‑poly stabbing‑planes proofs but only quasi‑poly Cutting Planes simulations under coefficient bounds, yielding new lower bounds and depth tradeoffs.
AI-written summary · about
chapters (10)
- 0:00Intro
- 2:17Integer Programming in Practice
- 8:41Analyzing Modern IP Algorithms
- 17:13Cutting Planes vs. Stabbing Planes
- 28:31Proof Idea: Stabbing Planes* → Cutting Planes
- 30:46Step 1. Facelike Stabbing Planes = Cutting Planes
- 34:31Step 2. Stabbing Planes* = Facelike Stabbing Planes
- 37:34Depth Blow-Up
- 39:49Supercritical Size-Depth Tradeoffs
- 49:56Open Problems
related talks
40mUtilizing Structure in Combinatorial Solving and Reasoning
18mOn the Verification of a Subgraph Construction Algorithm
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
01h 05mVerifying Infinitely Many Programs at Once
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
59mExact Performance Verification of First‑Order Methods in Parametric Convex Optimization