Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR14-038 | 7th April 2014 15:30

Total space in resolution

RSS-Feed




Revision #1
Authors: Ilario Bonacina, Nicola Galesi, Neil Thapen
Accepted on: 7th April 2014 15:31
Downloads: 1317
Keywords: 


Abstract:

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.



Changes to previous version:

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


Paper:

TR14-038 | 24th March 2014 18:33

Total space in resolution





TR14-038
Authors: Ilario Bonacina, Nicola Galesi, Neil Thapen
Publication: 24th March 2014 19:40
Downloads: 2771
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint