Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs

Susanna F. de Rezende, Jakob Nordström, Kilian Risse, Dmitry Sokolov

TL;DR

The paper addresses the problem of proving exponential lower bounds on resolution proof length for pigeonhole and perfect matching formulas over sparse, highly unbalanced expander graphs. It develops and applies Razborov's pseudo-width method in conjunction with a graph-closure technique to preserve expansion under adversarial removals, enabling lower bounds in regimes between balanced expanders and dense graphs. The authors establish both average-case and explicit-graph lower bounds for onto-FPHP/PM and functional PHP across a range of left sizes $m$ and left degrees, including constant-degree and polylog-degree regimes, by transforming short proofs into low-width refutations and then proving width lower bounds via a lossy counting argument in a tensor-space. The results bridge existing gaps in graph PHP/PM lower bounds and demonstrate the versatility of the pseudo-width method, with potential applicability to other open problems in resolution and related proof systems.

Abstract

We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. We obtain our results by revisiting Razborov's pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs

TL;DR

The paper addresses the problem of proving exponential lower bounds on resolution proof length for pigeonhole and perfect matching formulas over sparse, highly unbalanced expander graphs. It develops and applies Razborov's pseudo-width method in conjunction with a graph-closure technique to preserve expansion under adversarial removals, enabling lower bounds in regimes between balanced expanders and dense graphs. The authors establish both average-case and explicit-graph lower bounds for onto-FPHP/PM and functional PHP across a range of left sizes and left degrees, including constant-degree and polylog-degree regimes, by transforming short proofs into low-width refutations and then proving width lower bounds via a lossy counting argument in a tensor-space. The results bridge existing gaps in graph PHP/PM lower bounds and demonstrate the versatility of the pseudo-width method, with potential applicability to other open problems in resolution and related proof systems.

Abstract

We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. We obtain our results by revisiting Razborov's pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.

Paper Structure

This paper contains 22 sections, 30 theorems, 39 equations, 2 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Previous Work
  3. Our Results
  4. Techniques
  5. Outline of This Paper
  6. Preliminaries
  7. Proof Complexity
  8. Concentration Inequalities
  9. Graph Theory
  10. Two Key Technical Tools
  11. Pigeon Filtering
  12. Graph Closure
  13. Lower Bounds for Weak Graph FPHP Formulas
  14. Formal Statements of Graph FPHP Formula Lower Bounds
  15. A Pseudo-Width Upper Bound for Graph FPHP Formulas with Extra Axioms
  16. ...and 7 more sections

Key Result

Theorem 1.1

Let $G$ be a randomly sampled bipartite graph with $n$ right vertices, $m = n^{\mathrm{o} ( \log n )}$ left vertices, and left degree $\Theta \bigl( \log^2 m \bigr)$. Then refuting the onto-FPHP formula (a.k.a. perfect matching formula) over $G$ in resolution requires length $\exp \bigl( \Omega \big

Figures (2)

  • Figure 4: Depiction of relations between $\mathsf{closure}_{{}}(C), \mathsf{closure}_{{}}(C_i), i = 1,2, \mathrm{dom} ( \varphi' )$ and $\mathcal{D}_{{}}$ in proof of Lemma \ref{['lem:fphp_span']}.
  • Figure 5: Depiction of relations between $V_{L}, V_{R}, V_{P}, V_{H}$ and the vertex sets in the proof of Lemma \ref{['lem:onto_span']}

Theorems & Definitions (37)

  • Theorem 1.1: Informal
  • Theorem 1.2: Informal
  • Theorem 1.3: Informal
  • Theorem 2.1
  • Lemma 2.2
  • Theorem 2.3: GUV09Unbalanced
  • corollary 2.4
  • Lemma 3.1: Filter lemma
  • definition 3.2: Closure
  • Lemma 3.3
  • ...and 27 more