Showing 2025Show all
3 papers · 1 filter
cs.CC2025
On bounded depth proofs for Tseitin formulas on the grid; revisited
Johan HÃ¥stad, Kilian Risse
We study Frege proofs using depth- Boolean formulas for the Tseitin contradiction on grids. We prove that if each line in the proof is of size then the number o…
cs.CC2025
Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
Susanna F. de Rezende, Jakob Nordström, Kilian Risse +1
We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, th…
cs.CC2025
Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
Jonas Conneryd, Susanna F. de Rezende, Jakob Nordström +2
We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse ErdÅs-Rény…