Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs

De Rezende, Susanna F. LU orcid ; Nordström, Jakob LU ; Risse, Kilian and Sokolov, Dmitry LU (2025) In TheoretiCS 4.
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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; ; and
organization
publishing date
type
Contribution to journal
publication status
published
subject
keywords
Computational Complexity, Pigeonhole principle, Proof complexity, Resolution
in
TheoretiCS
volume
4
article number
9
pages
46 pages
publisher
TheoretiCS Foundation
external identifiers
  • scopus:105031163879
ISSN
2751-4838
DOI
10.46298/theoretics.25.9
language
English
LU publication?
yes
id
3dcc0de3-c036-4bf1-96fa-a74725f6313c
date added to LUP
2026-03-11 11:26:46
date last changed
2026-04-02 09:08:02
@article{3dcc0de3-c036-4bf1-96fa-a74725f6313c,
  abstract     = {{<p>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.</p>}},
  author       = {{De Rezende, Susanna F. and Nordström, Jakob and Risse, Kilian and Sokolov, Dmitry}},
  issn         = {{2751-4838}},
  keywords     = {{Computational Complexity; Pigeonhole principle; Proof complexity; Resolution}},
  language     = {{eng}},
  publisher    = {{TheoretiCS Foundation}},
  series       = {{TheoretiCS}},
  title        = {{Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs}},
  url          = {{http://dx.doi.org/10.46298/theoretics.25.9}},
  doi          = {{10.46298/theoretics.25.9}},
  volume       = {{4}},
  year         = {{2025}},
}