CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt154",{id:"formSmash:upper:j_idt154",widgetVar:"widget_formSmash_upper_j_idt154",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt155_j_idt157",{id:"formSmash:upper:j_idt155:j_idt157",widgetVar:"widget_formSmash_upper_j_idt155_j_idt157",target:"formSmash:upper:j_idt155:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)PrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
2016 (English)In: 2016 IEEE 57th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society, 2016, Vol. 2016, p. 295-304Conference paper, Published paper (Refereed)
##### Abstract [en]

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

IEEE Computer Society, 2016. Vol. 2016, p. 295-304
##### Series

Annual IEEE Symposium on Foundations of Computer Science, ISSN 0272-5428 ; 2016
##### Keywords [en]

proof complexity, communication complexity, circuit complexity, cutting planes, trade-offs, pebble games
##### National Category

Computer Sciences
##### Identifiers

URN: urn:nbn:se:kth:diva-200426DOI: 10.1109/FOCS.2016.40ISI: 000391198500032Scopus ID: 2-s2.0-85009372730ISBN: 978-1-5090-3933-3 (print)OAI: oai:DiVA.org:kth-200426DiVA, id: diva2:1069716
##### Conference

57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016, New Brunswick, United States, 9 October 2016 through 11 October 2016
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt474",{id:"formSmash:j_idt474",widgetVar:"widget_formSmash_j_idt474",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt481",{id:"formSmash:j_idt481",widgetVar:"widget_formSmash_j_idt481",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt488",{id:"formSmash:j_idt488",widgetVar:"widget_formSmash_j_idt488",multiple:true});
##### Note

##### In thesis

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.

QC 20170130

Available from: 2017-01-30 Created: 2017-01-27 Last updated: 2019-05-24Bibliographically approved1. Space in Proof Complexity$(function(){PrimeFaces.cw("OverlayPanel","overlay1094244",{id:"formSmash:j_idt828:0:j_idt832",widgetVar:"overlay1094244",target:"formSmash:j_idt828:0:parentLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. Lower Bounds and Trade-offs in Proof Complexity$(function(){PrimeFaces.cw("OverlayPanel","overlay1318061",{id:"formSmash:j_idt828:1:j_idt832",widgetVar:"overlay1318061",target:"formSmash:j_idt828:1:parentLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

doi
isbn
urn-nbn$(function(){PrimeFaces.cw("Tooltip","widget_formSmash_j_idt1324",{id:"formSmash:j_idt1324",widgetVar:"widget_formSmash_j_idt1324",showEffect:"fade",hideEffect:"fade",showDelay:500,hideDelay:300,target:"formSmash:altmetricDiv"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1377",{id:"formSmash:lower:j_idt1377",widgetVar:"widget_formSmash_lower_j_idt1377",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1378_j_idt1380",{id:"formSmash:lower:j_idt1378:j_idt1380",widgetVar:"widget_formSmash_lower_j_idt1378_j_idt1380",target:"formSmash:lower:j_idt1378:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});