Total Space in Resolution
Ilario Bonacina, Nicola Galesi, Neil Thapen · 2014
We show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables, and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the long-standing open problem of whether there are families of k-CNF formulas of polynomial size which require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.