Change search
ReferencesLink to record
Permanent link

Direct link
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
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
Abstract [en]

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.
Keyword [en]
total space, resolution, random CNFs, proof complexity
National Category
Computer Systems
URN: urn:nbn:se:kth:diva-197847DOI: 10.1137/15M1023269ISI: 000387321500007ScopusID: 2-s2.0-84920019506OAI: diva2:1059477

QC 20161222

Available from: 2016-12-22 Created: 2016-12-08 Last updated: 2016-12-22Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Bonacina, Ilario
By organisation
Theoretical Computer Science, TCS
In the same journal
SIAM journal on computing (Print)
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 8 hits
ReferencesLink to record
Permanent link

Direct link