In Search of the Hard Instances
summary
Partial survey that ties concrete lower/upper bounds, sum-of-squares algebraic proofs, and proof-search hardness to practical SAT behavior. Shows the pigeonhole principle needs exponential resolution size but has constant-degree SOS refutations; identifies regimes where random k‑clique and q‑coloring formulas are provably hard for tree‑like or general resolution yet easy for SDP/SOS certificates like the Lovász theta. Raises open problems: produce explicit worst‑case graphs, explain the combinatorial property behind random‑graph lower bounds, and match SOS/SDP power without heavy semidefinite solvers (testable on planted vs random graphs around degree ~15 for 3‑coloring).
AI-written summary · about
chapters (6)
- 0:00Workshop introduction
- 8:46Motivation for hard instances
- 19:08Proof systems in SAT
- 35:35Hard instances for clique
- 1:03:43Approximate graph coloring
- 1:14:03Q&A
related talks
40mUtilizing Structure in Combinatorial Solving and Reasoning
24mA New Conjecture on Hardness of Low-Degree 2-CSP’s with...
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
18mOn the Verification of a Subgraph Construction Algorithm
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
58mA New Perspective on Commutativity in Verification
52mNumbers, Logic, and Decidability for Cyber-Physical Systems