Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs. / de Rezende, Susanna F.; Nordström, Jakob; Risse, Kilian; Sokolov, Dmitry.
35th Computational Complexity Conference, CCC 2020. ed. / Shubhangi Saraf. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. p. 1-24 28 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 169).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
AU - de Rezende, Susanna F.
AU - Nordström, Jakob
AU - Risse, Kilian
AU - Sokolov, Dmitry
PY - 2020/7/1
Y1 - 2020/7/1
N2 - 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.
AB - 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.
KW - Perfect matching
KW - Proof complexity
KW - Resolution
KW - Sparse graphs
KW - Weak pigeonhole principle
UR - http://www.scopus.com/inward/record.url?scp=85089398484&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CCC.2020.28
DO - 10.4230/LIPIcs.CCC.2020.28
M3 - Article in proceedings
AN - SCOPUS:85089398484
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 1
EP - 24
BT - 35th Computational Complexity Conference, CCC 2020
A2 - Saraf, Shubhangi
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
T2 - 35th Computational Complexity Conference, CCC 2020
Y2 - 28 July 2020 through 31 July 2020
ER -
ID: 251867082