Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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.
Series
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
Identifiers
URN: urn:nbn:se:kth:diva-134074DOI: 10.1007/978-3-642-39206-1_37Scopus ID: 2-s2.0-84880288724ISBN: 978-364239205-4 (print)OAI: oai:DiVA.org:kth-134074DiVA: diva2:664987
Conference
40th International Colloquium on Automata, Languages, and Programming, ICALP 2013; Riga; Latvia; 8 July 2013 through 12 July 2013
Note

QC 20131118

Available from: 2013-11-18 Created: 2013-11-15 Last updated: 2017-05-09Bibliographically approved
In thesis
1. On Complexity Measures in Polynomial Calculus
Open this publication in new window or tab >>On Complexity Measures in Polynomial Calculus
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Proof complexity is the study of different resources that a proof needs in different proof systems for propositional logic. This line of inquiry relates to the fundamental questions in theoretical computer science, as lower bounds on proof size for an arbitrary proof system would separate P from NP.

We study two simple proof systems: resolution and polynomial calculus. In resolution we reason using clauses, while in polynomial calculus we use polynomials. We study three measures of complexity of proofs: size, space, and width/degree. Size is the number of clauses or monomials that appear in a resolution or polynomial calculus proof, respectively. Space is the maximum number of clauses/monomials we need to keep at each time step of the proof. Width/degree is the size of the largest clause/monomial in a proof.

Width is a lower bound for space in resolution. The original proof of this claim used finite model theory. In this thesis we give a different, more direct proof of the space-width relation. We can ask whether a similar relation holds between space and degree in polynomial calculus. We make some progress on this front by showing that when a formula F requires resolution width w then the XORified version of F requires polynomial calculus space Ω(w). We also show that space lower bounds do not imply degree lower bounds in polynomial calculus.

Width/degree and size are also related, as strong lower bounds for width/degree imply strong lower bounds for size. Currently, proving width lower bounds has a well-developed machinery behind it. However, the degree measure is much less well-understood. We provide a unified framework for almost all previous degree lower bounds. We also prove some new degree and size lower bounds. In addition, we explore the relation between theory and practice by running experiments on some current state-of-the-art SAT solvers.

Place, publisher, year, edition, pages
Stockholm, Sweden: KTH Royal Institute of Technology, 2016. 180 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:02
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-197278 (URN)978-91-7729-226-5 (ISBN)
Public defence
2017-01-20, D2, Lindstedtsvägen 5, Stockholm, 14:00 (English)
Opponent
Supervisors
Projects
Understanding the Hardness of Theorem Proving
Funder
EU, FP7, Seventh Framework Programme, 279611
Note

QC 20161206

Available from: 2016-12-06 Created: 2016-11-30 Last updated: 2016-12-26Bibliographically approved
2. Space in Proof Complexity
Open this publication in new window or tab >>Space in Proof Complexity
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

ropositional proof complexity is the study of the resources that are needed to prove formulas in propositional logic. In this thesis we are concerned with the size and space of proofs, and in particular with the latter.

Different approaches to reasoning are captured by corresponding proof systems. The simplest and most well studied proof system is resolution, and we try to get our understanding of other proof systems closer to that of resolution.

In resolution we can prove a space lower bound just by showing that any proof must have a large clause. We prove a similar relation between resolution width and polynomial calculus space that lets us derive space lower bounds, and we use it to separate degree and space.

For cutting planes we show length-space trade-offs. This is, there are formulas that have a proof in small space and a proof in small length, but there is no proof that can optimize both measures at the same time.

We introduce a new measure of space, cumulative space, that accounts for the space used throughout a proof rather than only its maximum. This is exploratory work, but we can also prove new results for the usual space measure.

We define a new proof system that aims to capture the power of current SAT solvers, and we show a landscape of length-space trade-offs comparable to those in resolution.

To prove these results we build and use tools from other areas of computational complexity. One area is pebble games, very simple computational models that are useful for modelling space. In addition to results with applications to proof complexity, we show that pebble game cost is PSPACE-hard to approximate.

Another area is communication complexity, the study of the amount of communication that is needed to solve a problem when its description is shared by multiple parties. We prove a simulation theorem that relates the query complexity of a function with the communication complexity of a composed function.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2017. 318 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:15
Keyword
proof complexity, resolution, polynomial calculus, cutting planes, space complexity, computational complexity, pebble games, communication complexity, CDCL
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-206571 (URN)978-91-7729-422-1 (ISBN)
Public defence
2017-06-09, E2, Lindstedtsvägen, 3, Stockholm, 14:00 (English)
Opponent
Supervisors
Funder
EU, FP7, Seventh Framework Programme, 279611
Note

QC 20170509

Available from: 2017-05-10 Created: 2017-05-09 Last updated: 2017-05-10Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Lauria, MassimoNordström, JakobVinyals, Marc

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 145 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf