Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
(2020) 35th Computational Complexity Conference, CCC 2020 In Leibniz International Proceedings in Informatics, LIPIcs 169.- 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)
- author
- de Rezende, Susanna F.
LU
; Nordström, Jakob LU ; Risse, Kilian and Sokolov, Dmitry LU
- organization
- publishing date
- 2020-07-01
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Perfect matching, Proof complexity, Resolution, Sparse graphs, Weak pigeonhole principle
- host publication
- CCC '20: Proceedings of the 35th Computational Complexity Conference 2020
- series title
- Leibniz International Proceedings in Informatics, LIPIcs
- editor
- Saraf, Shubhangi
- volume
- 169
- article number
- 28
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 35th Computational Complexity Conference, CCC 2020
- conference location
- Virtual, Online, Germany
- conference dates
- 2020-07-28 - 2020-07-31
- external identifiers
-
- scopus:85089398484
- ISSN
- 1868-8969
- ISBN
- 9783959771566
- DOI
- 10.4230/LIPIcs.CCC.2020.28
- language
- English
- LU publication?
- yes
- id
- 1529fede-06f1-4730-ac52-e0a29cd502f2
- date added to LUP
- 2020-12-18 22:14:03
- date last changed
- 2022-04-19 02:56:18
@inproceedings{1529fede-06f1-4730-ac52-e0a29cd502f2, 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}}, booktitle = {{CCC '20: Proceedings of the 35th Computational Complexity Conference 2020}}, editor = {{Saraf, Shubhangi}}, isbn = {{9783959771566}}, issn = {{1868-8969}}, keywords = {{Perfect matching; Proof complexity; Resolution; Sparse graphs; Weak pigeonhole principle}}, language = {{eng}}, month = {{07}}, publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}}, series = {{Leibniz International Proceedings in Informatics, LIPIcs}}, title = {{Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs}}, url = {{http://dx.doi.org/10.4230/LIPIcs.CCC.2020.28}}, doi = {{10.4230/LIPIcs.CCC.2020.28}}, volume = {{169}}, year = {{2020}}, }