[Proof Complexity] Resolution lower bounds for weak graph PHP formulas

[Jakob Nordström]

Dear colleagues,

This is just to let you know that our manuscript

"Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs"

has now appeared as ECCC report https://eccc.weizmann.ac.il/report/2019/174/ .

You find the abstract below. Any comments or questions are warmly welcome!

Best regards,
Jakob Nordström


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.

Joint work with Susanna F. de Rezende, Kilian Risse, and Dmitry Sokolov.


Jakob Nordström, Associate Professor
University of Copenhagen and KTH Royal Institute of Technology
Phone: +46 70 742 21 98
http://www.csc.kth.se/~jakobn/