ECCC-Report TR14-038https://eccc.weizmann.ac.il/report/2014/038Comments and Revisions published for TR14-038en-usMon, 07 Apr 2014 15:31:04 +0300
Revision 1
| Total space in resolution |
Ilario Bonacina,
Nicola Galesi,
Neil Thapen
https://eccc.weizmann.ac.il/report/2014/038#revision1We 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.Mon, 07 Apr 2014 15:31:04 +0300https://eccc.weizmann.ac.il/report/2014/038#revision1
Paper TR14-038
| Total space in resolution |
Ilario Bonacina,
Nicola Galesi,
Neil Thapen
https://eccc.weizmann.ac.il/report/2014/038We 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.Mon, 24 Mar 2014 19:40:33 +0200https://eccc.weizmann.ac.il/report/2014/038