Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Space in Proof Complexity
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-1487-445X
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 [en]
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: urn:nbn:se:kth:diva-206571ISBN: 978-91-7729-422-1 (print)OAI: oai:DiVA.org:kth-206571DiVA: diva2:1094244
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
List of papers
1. Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)
Open this publication in new window or tab >>Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)
Show others...
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
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 7965 LNCS
Keyword
Extended abstracts, Lower bounds, Pigeonhole principle, Polynomial calculus, Proof complexity, Proof system, Short cycle, Space complexity
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-134074 (URN)10.1007/978-3-642-39206-1_37 (DOI)2-s2.0-84880288724 (Scopus ID)978-364239205-4 (ISBN)
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
2. How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
Open this publication in new window or tab >>How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
2016 (English)In: 2016 IEEE 57th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society, 2016, Vol. 2016, 295-304 p.Conference paper, Published paper (Refereed)
Abstract [en]

We obtain the first true size-space trade-offs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constant-size coefficients, and the lower bounds apply to length and formula space (i.e., number of inequalities in memory) even for derivations with exponentially large coefficients. These are also the first trade-offs to hold uniformly for resolution, polynomial calculus and cutting planes, thus capturing the main methods of reasoning used in current state-of-the-art SAT solvers. We prove our results by a reduction to communication lower bounds in a round-efficient version of the real communication model of [Krajicek ' 98], drawing on and extending techniques in [Raz and McKenzie ' 99] and [Goos et al. '15]. The communication lower bounds are in turn established by a reduction to trade-offs between cost and number of rounds in the game of [Dymond and Tompa '85] played on directed acyclic graphs. As a by-product of the techniques developed to show these proof complexity trade-off results, we also obtain an exponential separation between monotone-AC(i-1) and monotone-AC(i), improving exponentially over the superpolynomial separation in [Raz and McKenzie ' 99]. That is, we give an explicit Boolean function that can be computed by monotone Boolean circuits of depth log(i) n and polynomial size, but for which circuits of depth O (log(i-1) n) require exponential size.

Place, publisher, year, edition, pages
IEEE Computer Society, 2016
Series
Annual IEEE Symposium on Foundations of Computer Science, ISSN 0272-5428 ; 2016
Keyword
proof complexity, communication complexity, circuit complexity, cutting planes, trade-offs, pebble games
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-200426 (URN)10.1109/FOCS.2016.40 (DOI)000391198500032 ()2-s2.0-85009372730 (Scopus ID)978-1-5090-3933-3 (ISBN)
Conference
57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016, New Brunswick, United States, 9 October 2016 through 11 October 2016
Note

QC 20170130

Available from: 2017-01-30 Created: 2017-01-27 Last updated: 2017-05-09Bibliographically approved
3. Cumulative Space in Black-White Pebbling and Resolution
Open this publication in new window or tab >>Cumulative Space in Black-White Pebbling and Resolution
2017 (English)Conference paper, Published paper (Refereed)
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-206582 (URN)
Conference
8th Innovations in Theoretical Computer Science (ITCS) conference, Berkeley, January 9-11, 2017
Note

QC 20170509

Available from: 2017-05-05 Created: 2017-05-05 Last updated: 2017-05-09Bibliographically approved
4. Trade-offs between time and memory in a tighter model of CDCL SAT solvers
Open this publication in new window or tab >>Trade-offs between time and memory in a tighter model of CDCL SAT solvers
Show others...
2016 (English)In: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Springer, 2016, 160-176 p.Conference paper, Published paper (Refereed)
Abstract [en]

A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that cap- tures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL with- out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.

Place, publisher, year, edition, pages
Springer, 2016
Keyword
Commerce, Formal logic, Clause learning, Fine grained, Learning schemes, Lower bounds, Memory usage, Resolution proofs, SAT solvers, Upper Bound, Economic and social effects
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-195488 (URN)10.1007/978-3-319-40970-2_11 (DOI)000387430600011 ()2-s2.0-84977484096 (Scopus ID)9783319409696 (ISBN)
Conference
5 July 2016 through 8 July 2016
Note

QC 20161118

Available from: 2016-11-18 Created: 2016-11-03 Last updated: 2017-05-09Bibliographically approved
5. Hardness of Approximation in PSPACE and Separation Results for Pebble Games
Open this publication in new window or tab >>Hardness of Approximation in PSPACE and Separation Results for Pebble Games
2015 (English)In: Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS, Institute of Electrical and Electronics Engineers (IEEE), 2015, 466-485 p.Conference paper, Published paper (Refereed)
Abstract [en]

We consider the pebble game on DAGs with bounded fan-in introduced in [Paterson and Hewitt '70] and the reversible version of this game in [Bennett '89], and study the question of how hard it is to decide exactly or approximately the number of pebbles needed for a given DAG in these games. We prove that the problem of deciding whether s pebbles suffice to reversibly pebble a DAG G is PSPACE-complete, as was previously shown for the standard pebble game in [Gilbert, Lengauer and Tarjan '80]. Via two different graph product constructions we then strengthen these results to establish that both standard and reversible pebbling space are PSPACE-hard to approximate to within any additive constant. To the best of our knowledge, these are the first hardness of approximation results for pebble games in an unrestricted setting (even for polynomial time). Also, since [Chan '13] proved that reversible pebbling is equivalent to the games in [Dymond and Tompa '85] and [Raz and McKenzie '99], our results apply to the Dymond - Tompa and Raz - McKenzie games as well, and from the same paper it follows that resolution depth is PSPACE-hard to determine up to any additive constant. We also obtain a multiplicative logarithmic separation between reversible and standard pebbling space. This improves on the additive logarithmic separation previously known and could plausibly be tight, although we are not able to prove this. We leave as an interesting open problem whether our additive hardness of approximation result could be strengthened to a multiplicative bound if the computational resources are decreased from polynomial space to the more common setting of polynomial time. © 2015 IEEE.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2015
Keyword
Dymond-Tompa game, pebbling, PSPACE-complete, PSPACE-hardness of approximation, Raz-Mc Kenzie game, resolution depth, reversible pebbling, separation
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:kth:diva-186800 (URN)10.1109/FOCS.2015.36 (DOI)000379204700027 ()2-s2.0-84960371365 (Scopus ID)9781467381918 (ISBN)
Conference
56th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2015, 17 October 2015 through 20 October 2015
Note

QC 20160516

Available from: 2016-05-16 Created: 2016-05-13 Last updated: 2017-05-09Bibliographically approved

Open Access in DiVA

fulltext(1865 kB)62 downloads
File information
File name FULLTEXT01.pdfFile size 1865 kBChecksum SHA-512
a8c1221e0e26596ab2c2f9e6b7573ad37bd44a0c23264cf4ebca40cf592300e062e669e0a730217245dd9f8ac9a080406801d0527112778ad4e8b405fd949fe9
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Vinyals, Marc
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 62 downloads
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

Total: 287 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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