Revision #1 Authors: Ilario Bonacina, Nicola Galesi, Neil Thapen

Accepted on: 7th April 2014 15:31

Downloads: 1123

Keywords:

We show $\Omega(n^2)$ 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 size $O(n)$ requiring total space $\Omega(n^2)$ in resolution, and gives the first truly quadratic lower bounds on total space. 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.

Some stylistic changes in Section "1. Introduction". All the other sections are exactly the same as in the previous version.

TR14-038 Authors: Ilario Bonacina, Nicola Galesi, Neil Thapen

Publication: 24th March 2014 19:40

Downloads: 2171

Keywords:

We show $\Omega(n^2)$ 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 size $O(n)$ requiring total space $\Omega(n^2)$ in resolution, and gives the first truly quadratic lower bounds on total space. 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.