Please wait ... |

Link to record
http://kth.diva-portal.org/smash/person.jsf?pid=authority-person:32201 $(function(){PrimeFaces.cw("InputTextarea","widget_formSmash_upper_j_idt122_recordDirectLink",{id:"formSmash:upper:j_idt122:recordDirectLink",widgetVar:"widget_formSmash_upper_j_idt122_recordDirectLink",autoResize:true});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt122_j_idt124",{id:"formSmash:upper:j_idt122:j_idt124",widgetVar:"widget_formSmash_upper_j_idt122_j_idt124",target:"formSmash:upper:j_idt122:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Permanent link

Direct link

Vinyals, Marcorcid.org/0000-0002-1487-445X

Open this publication in new window or tab >>Cumulative Space in Black-White Pebbling and Resolution### Alwen, Joël

### de Rezende, Susanna F.

### Nordström, Jakob

### Vinyals, Marc

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_some",{id:"formSmash:j_idt184:0:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_otherAuthors",{id:"formSmash:j_idt184:0:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_otherAuthors",multiple:true}); 2017 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2017Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017
##### Keywords

Clause Space, Cumulative Space, Parallel Resolution, Pebble Game, Pebbling, Proof Complexity, Resolution, Space, Commerce, Optical resolving power, Economic and social effects
##### National Category

Computer Sciences
##### Identifiers

urn:nbn:se:kth:diva-206582 (URN)10.4230/LIPIcs.ITCS.2017.38 (DOI)2-s2.0-85034241142 (Scopus ID)9783959770293 (ISBN)
##### Conference

8th Innovations in Theoretical Computer Science Conference (ITCS 2017), January 9-11, 2017, Berkeley, CA, USA
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_j_idt359",{id:"formSmash:j_idt184:0:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_j_idt365",{id:"formSmash:j_idt184:0:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_j_idt371",{id:"formSmash:j_idt184:0:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_j_idt371",multiple:true});
#####

##### Note

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko 2015] as a tool for obtaining results in cryptography. We consider instead the nondeterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10-15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström 2008, 2011], we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.

QC 20170509

Available from: 2017-05-05 Created: 2017-05-05 Last updated: 2019-05-29Bibliographically approvedOpen this publication in new window or tab >>Trade-offs between time and memory in a tighter model of CDCL SAT solvers### Elffers, Jan

### Johannsen, J.

### Lauria, M.

### Magnard, T.

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_some",{id:"formSmash:j_idt184:1:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_some",multiple:true}); ### Nordström, Jakob

### Vinyals, Marc

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_otherAuthors",{id:"formSmash:j_idt184:1:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_otherAuthors",multiple:true}); Show others...PrimeFaces.cw("SelectBooleanButton","widget_formSmash_j_idt184_1_j_idt188_j_idt202",{id:"formSmash:j_idt184:1:j_idt188:j_idt202",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt202",onLabel:"Hide others...",offLabel:"Show others..."}); 2016 (English)In: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Springer, 2016, p. 160-176Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Springer, 2016
##### Keywords

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 Sciences
##### 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
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_j_idt359",{id:"formSmash:j_idt184:1:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_j_idt365",{id:"formSmash:j_idt184:1:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_j_idt371",{id:"formSmash:j_idt184:1:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt371",multiple:true});
#####

##### Note

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

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.

QC 20161118

Available from: 2016-11-18 Created: 2016-11-03 Last updated: 2018-01-13Bibliographically approvedOpen this publication in new window or tab >>Hardness of Approximation in PSPACE and Separation Results for Pebble Games### Chan, S. M.

### Lauria, Massimo

### Nordstrom, Jakob

### Vinyals, Marc

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_some",{id:"formSmash:j_idt184:2:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_otherAuthors",{id:"formSmash:j_idt184:2:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_otherAuthors",multiple:true}); 2015 (English)In: Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS, Institute of Electrical and Electronics Engineers (IEEE), 2015, p. 466-485Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Institute of Electrical and Electronics Engineers (IEEE), 2015
##### Keywords

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
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_j_idt359",{id:"formSmash:j_idt184:2:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_j_idt365",{id:"formSmash:j_idt184:2:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_j_idt371",{id:"formSmash:j_idt184:2:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_j_idt371",multiple:true});
#####

##### Note

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

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.

QC 20160516

Available from: 2016-05-16 Created: 2016-05-13 Last updated: 2017-05-09Bibliographically approvedOpen this publication in new window or tab >>From small space to small width in resolution### Filmus, Y.

### Lauria, Massimo

### Mikša, Mladen

### Nordström, Jakob

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_some",{id:"formSmash:j_idt184:3:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_some",multiple:true}); ### Vinyals, Marc

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_otherAuthors",{id:"formSmash:j_idt184:3:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_otherAuthors",multiple:true}); Show others...PrimeFaces.cw("SelectBooleanButton","widget_formSmash_j_idt184_3_j_idt188_j_idt202",{id:"formSmash:j_idt184:3:j_idt188:j_idt202",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt202",onLabel:"Hide others...",offLabel:"Show others..."}); 2014 (English)In: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2014, Vol. 25, p. 300-311Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2014
##### Series

Leibniz International Proceedings in Informatics, LIPIcs, ISSN 1868-8969 ; 25
##### Keywords

PCR, Polynomial calculus, Proof complexity, Resolution, Space, Width
##### National Category

Computer and Information Sciences
##### Identifiers

urn:nbn:se:kth:diva-158079 (URN)10.4230/LIPIcs.STACS.2014.300 (DOI)2-s2.0-84907818998 (Scopus ID)978-393989765-1 (ISBN)
##### Conference

31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, 5 March 2014 through 8 March 2014
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_j_idt359",{id:"formSmash:j_idt184:3:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_j_idt365",{id:"formSmash:j_idt184:3:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_j_idt371",{id:"formSmash:j_idt184:3:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt371",multiple:true});
#####

##### Note

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.

QC 20141222

Available from: 2014-12-22 Created: 2014-12-22 Last updated: 2018-01-11Bibliographically approvedOpen this publication in new window or tab >>Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)### Filmus, Yuval

### Lauria, Massimo

### Mikša, Mladen

### Nordström, Jakob

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_some",{id:"formSmash:j_idt184:4:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_some",multiple:true}); ### Vinyals, Marc

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_otherAuthors",{id:"formSmash:j_idt184:4:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_otherAuthors",multiple:true}); Show others...PrimeFaces.cw("SelectBooleanButton","widget_formSmash_j_idt184_4_j_idt188_j_idt202",{id:"formSmash:j_idt184:4:j_idt188:j_idt202",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt202",onLabel:"Hide others...",offLabel:"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, p. 437-448Conference paper, Published paper (Refereed)
##### Abstract [en]

##### 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
##### Keywords

Extended abstracts, Lower bounds, Pigeonhole principle, Polynomial calculus, Proof complexity, Proof system, Short cycle, Space complexity
##### National Category

Computer and Information Sciences
##### 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
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_j_idt359",{id:"formSmash:j_idt184:4:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_j_idt365",{id:"formSmash:j_idt184:4:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_j_idt371",{id:"formSmash:j_idt184:4:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt371",multiple:true});
#####

##### Note

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.

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.

QC 20131118

Available from: 2013-11-18 Created: 2013-11-15 Last updated: 2018-01-11Bibliographically approvedOpen this publication in new window or tab >>Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity### de Rezende, Susanna F.

### Meir, Or

### Nordström, Jakob

### Toniann, Pitassi

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_5_j_idt188_some",{id:"formSmash:j_idt184:5:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_5_j_idt188_some",multiple:true}); ### Robere, Robert

### Vinyals, Marc

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_5_j_idt188_otherAuthors",{id:"formSmash:j_idt184:5:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_5_j_idt188_otherAuthors",multiple:true}); Show others...PrimeFaces.cw("SelectBooleanButton","widget_formSmash_j_idt184_5_j_idt188_j_idt202",{id:"formSmash:j_idt184:5:j_idt188:j_idt202",widgetVar:"widget_formSmash_j_idt184_5_j_idt188_j_idt202",onLabel:"Hide others...",offLabel:"Show others..."}); (English)Manuscript (preprint) (Other academic)
##### Abstract [en]

##### National Category

Computer Sciences
##### Research subject

Computer Science
##### Identifiers

urn:nbn:se:kth:diva-249607 (URN)
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_5_j_idt188_j_idt359",{id:"formSmash:j_idt184:5:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_5_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_5_j_idt188_j_idt365",{id:"formSmash:j_idt184:5:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_5_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_5_j_idt188_j_idt371",{id:"formSmash:j_idt184:5:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_5_j_idt188_j_idt371",multiple:true});
#####

##### Note

KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.

KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:

- We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomialline space if coefficients are restricted to be of polynomial magnitude.

- We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.

An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

QC 20190529

Available from: 2019-04-12 Created: 2019-04-12 Last updated: 2019-05-29Bibliographically approved