Exponential separations using guarded extension variables
summary
Proves exponential separations between redundancy-based CNF proof systems by embedding short extended‑resolution (ER) proofs into guarded formulas so only some systems can exploit the added extension variables. Uses guarded extension variables and syntactic criteria like blocked clauses to force some systems to see no shortcut while others simulate ER; constructions start from an ER proof of size m and add m new xi (or xi↔yi) clauses as guards. Results give many new separations (some conditional on ER vs SBC minus), modular upper bounds and matching lower bounds.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:36Resolution
- 2:14Proof in Resolution
- 5:47Motivation
- 7:24Example
- 8:49Redundancy
- 9:28Block Clause
- 12:01Inference Rules
- 13:05Different Proof Systems
- 14:33Results
- 16:26Guarded extension variables
- 18:34Summary
- 20:33Proof
- 22:18Takehome messages
related talks
31mNew Unconditional Lower Bounds for Algorithms and Enumeration Problems
33mLower Bounds for Subexponential Parameterized Complexity of Minimum Fill-in and Related Problems
27mOn the Subexponential Time Complexity of the CSP
A Formal Disproof of Hirsch Conjecture
01h 02mFine-Grained Counting Complexity I
01h 31mCircuits of Bounded Depth
30mLower Bound Results for Hard Problems Related to Finite Automata
33mSub-exponential Approximation Schemes for CSPs: from Dense to Almost Sparse