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

Lower Bounds and Trade-offs in Proof ComplexityPrimeFaces.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();
}
}
2019 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

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

KTH Royal Institute of Technology, 2019. , p. 247
##### Series

TRITA-EECS-AVL ; 2019:47
##### Keywords [en]

Proof complexity, trade-offs, lower bounds, size, length, space
##### National Category

Computer Sciences
##### Research subject

Computer Science
##### Identifiers

URN: urn:nbn:se:kth:diva-249610ISBN: 978-91-7873-191-6 (print)OAI: oai:DiVA.org:kth-249610DiVA, id: diva2:1318061
##### Public defence

2019-06-14, Kollegiesalen, Brinellvägen 8, Stockholm, 14:00 (English)
##### Opponent

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt434",{id:"formSmash:j_idt434",widgetVar:"widget_formSmash_j_idt434",multiple:true});
##### Supervisors

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

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

##### List of papers

Propositional proof complexity is a field in theoretical computer science that analyses the resources needed to prove statements. In this thesis, we are concerned about the length of proofs and trade-offs between different resources, such as length and space.

A classical NP-hard problem in computational complexity is that of determining whether a graph has a clique of size k. We show that for all k ≪ n^(1/4) regular resolution requires length n^Ω(k) to establish that an Erdős–Rényi graph with n vertices and appropriately chosen edge density does not contain a k-clique. In particular, this implies an unconditional lower bound on the running time of state-of-the-artalgorithms for finding a maximum clique.

In terms of trading resources, we prove a length-space trade-off for the cutting planes proof system by first establishing a communication-round trade-off for real communication via a round-aware simulation theorem. The technical contri-bution of this result allows us to obtain a separation between monotone-AC^(i-1) and monotone-NC^i.

We also obtain a trade-off separation between cutting planes (CP) with unbounded coefficients and cutting planes where coefficients are at most polynomial in thenumber of variables (CP*). We show that there are formulas that have CP proofs in constant space and quadratic length, but any CP* proof requires either polynomial space or exponential length. This is the first example in the literature showing any type of separation between CP and CP*.

For the Nullstellensatz proof system, we prove a size-degree trade-off via a tight reduction of Nullstellensatz refutations of pebbling formulas to the reversible pebbling game. We show that for any directed acyclic graph G it holds that G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatzrefutation of the pebbling formula over G in size t + 1 and degree s.

Finally, we introduce the study of cumulative space in proof complexity, a measure that captures the space used throughout the whole proof and not only the peak space usage. We prove cumulative space lower bounds for the resolution proof system, which can be viewed as time-space trade-offs where, when time is bounded, space must be large a significant fraction of the time.

QC 20190527

Available from: 2019-05-27 Created: 2019-05-24 Last updated: 2019-05-27Bibliographically approved1. Clique Is Hard on Average for Regular Resolution$(function(){PrimeFaces.cw("OverlayPanel","overlay1294866",{id:"formSmash:j_idt495:0:j_idt499",widgetVar:"overlay1294866",target:"formSmash:j_idt495:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)$(function(){PrimeFaces.cw("OverlayPanel","overlay1069716",{id:"formSmash:j_idt495:1:j_idt499",widgetVar:"overlay1069716",target:"formSmash:j_idt495:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity$(function(){PrimeFaces.cw("OverlayPanel","overlay1304720",{id:"formSmash:j_idt495:2:j_idt499",widgetVar:"overlay1304720",target:"formSmash:j_idt495:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling$(function(){PrimeFaces.cw("OverlayPanel","overlay1304722",{id:"formSmash:j_idt495:3:j_idt499",widgetVar:"overlay1304722",target:"formSmash:j_idt495:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

5. Cumulative Space in Black-White Pebbling and Resolution$(function(){PrimeFaces.cw("OverlayPanel","overlay1093402",{id:"formSmash:j_idt495:4:j_idt499",widgetVar:"overlay1093402",target:"formSmash:j_idt495:4:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

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

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