TOTAL SPACE IN RESOLUTION
2016 (English)In: SIAM journal on computing (Print), ISSN 0097-5397, E-ISSN 1095-7111, Vol. 45, no 5, 1894-1909 p.Article in journal (Refereed) Published
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 open problem of whether there are families of k-CNF formulas of polynomial size that 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.
Place, publisher, year, edition, pages
IEEE Computer Society , 2016. Vol. 45, no 5, 1894-1909 p.
total space, resolution, random CNFs, proof complexity
IdentifiersURN: urn:nbn:se:kth:diva-197847DOI: 10.1137/15M1023269ISI: 000387321500007ScopusID: 2-s2.0-84920019506OAI: oai:DiVA.org:kth-197847DiVA: diva2:1059477
QC 201612222016-12-222016-12-082016-12-22Bibliographically approved