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

0531886 - MÚ 2021 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
de Rezende, Susanna F. - Nordstöm, J. - Risse, K. - Sokolov, D.
Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs.
35th Computational Complexity Conference (CCC 2020). Dagstuhl: Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2020 - (Shubhangi, S.), č. článku 28. Leibniz International Proceedings in Informatics, 169. ISBN 978-3-95977-156-6. ISSN 1868-8969.
[35th Computational Complexity Conference (CCC 2020). Saarbrücken (DE), 28.07.2020-31.07.2020]
Institucionální podpora: RVO:67985840
Klíčová slova: proof complexity * resolution * weak pigeonhole principle * perfect matching * sparse graphs
Obor OECD: Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
https://doi.org/10.4230/LIPIcs.CCC.2020.28

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.
Trvalý link: http://hdl.handle.net/11104/0310520