Theoretical limits of 1UIP Learning
summary
Shows explicit CNF families with linear-length resolution proofs but that force CDCL with 1UIP (or any reasonable learning) to incur a quadratic blowup in proof length, so CDCL cannot always match resolution. Proofs rely on a fine-grained subsystem called merge resolution that models learning as input-resolution sequences, and the simulation requires assumptions: optimal branching, no clause deletion and frequent restarts; under those assumptions the best known simulation has polynomial overhead (cubic), and the separation gives a necessary linear-factor cost.
AI-written summary · about
chapters (9)
- 0:00Start
- 7:30CDCL equivalent to Resolution: Statement
- 12:43CDCL equivalent to Resolution: Simulation Derivation
- 15:18Assumptions: Branching
- 17:13Simulation Overhead
- 20:11Formalizing CDCL
- 22:21Merge Resolution
- 23:06Future: CDCL vs Resolution
- 24:36Future: SAT vs Proof Complexity
related talks
19mProof Automation for Linearizability in Separation Logic
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
24mBuilding Information Modeling Using Constraint Logic Programming (Extended Ab...
01h 05mVerifying Infinitely Many Programs at Once
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
15mIncremental Certified Programming
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)