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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

2 Citations (Scopus)
41 Downloads (Pure)

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.

Original languageEnglish
Title of host publication35th Computational Complexity Conference, CCC 2020
EditorsShubhangi Saraf
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date1 Jul 2020
Pages1-24
Article number28
ISBN (Electronic)9783959771566
DOIs
Publication statusPublished - 1 Jul 2020
Event35th Computational Complexity Conference, CCC 2020 - Virtual, Online, Germany
Duration: 28 Jul 202031 Jul 2020

Conference

Conference35th Computational Complexity Conference, CCC 2020
Country/TerritoryGermany
CityVirtual, Online
Period28/07/202031/07/2020
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume169
ISSN1868-8969

Keywords

  • Perfect matching
  • Proof complexity
  • Resolution
  • Sparse graphs
  • Weak pigeonhole principle

Cite this