Change search
ReferencesLink to record
Permanent link

Direct link
Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0003-4003-3168
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
Show others and affiliations
2013 (English)In: Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part I, Springer, 2013, no PART 1, 437-448 p.Conference paper (Refereed)
Abstract [en]

During the last decade, an active line of research in proof complexity has been into the space complexity of proofs and how space is related to other measures. By now these aspects of resolution are fairly well understood, but many open problems remain for the related but stronger polynomial calculus (PC/PCR) proof system. For instance, the space complexity of many standard "benchmark formulas" is still open, as well as the relation of space to size and degree in PC/PCR. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PCR space, providing some circumstantial evidence that degree might be a lower bound for space. More importantly, this immediately yields formulas that are very hard for space but very easy for size, exhibiting a size-space separation similar to what is known for resolution. Using related ideas, we show that if a graph has good expansion and in addition its edge set can be partitioned into short cycles, then the Tseitin formula over this graph requires large PCR space. In particular, Tseitin formulas over random 4-regular graphs almost surely require space at least Ω(√n). Our proofs use techniques recently introduced in [Bonacina-Galesi '13]. Our final contribution, however, is to show that these techniques provably cannot yield non-constant space lower bounds for the functional pigeonhole principle, delineating the limitations of this framework and suggesting that we are still far from characterizing PC/PCR space.

Place, publisher, year, edition, pages
Springer, 2013. no PART 1, 437-448 p.
, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 7965 LNCS
Keyword [en]
Extended abstracts, Lower bounds, Pigeonhole principle, Polynomial calculus, Proof complexity, Proof system, Short cycle, Space complexity
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-134074DOI: 10.1007/978-3-642-39206-1_37ScopusID: 2-s2.0-84880288724ISBN: 978-364239205-4OAI: diva2:664987
40th International Colloquium on Automata, Languages, and Programming, ICALP 2013; Riga; Latvia; 8 July 2013 through 12 July 2013

QC 20131118

Available from: 2013-11-18 Created: 2013-11-15 Last updated: 2016-04-19Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Lauria, MassimoMikša, MladenNordström, JakobVinyals, Marc
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 22 hits
ReferencesLink to record
Permanent link

Direct link