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

Space 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();
}
}
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

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

Stockholm: KTH Royal Institute of Technology, 2017. , p. 318
##### Series

TRITA-CSC-A, ISSN 1653-5723 ; 2017:15
##### Keywords [en]

proof complexity, resolution, polynomial calculus, cutting planes, space complexity, computational complexity, pebble games, communication complexity, CDCL
##### National Category

Computer Sciences
##### Research subject

Computer Science
##### Identifiers

URN: urn:nbn:se:kth:diva-206571ISBN: 978-91-7729-422-1 (print)OAI: oai:DiVA.org:kth-206571DiVA, id: diva2:1094244
##### Public defence

2017-06-09, E2, Lindstedtsvägen, 3, Stockholm, 14:00 (English)
##### Opponent

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

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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt622",{id:"formSmash:j_idt622",widgetVar:"widget_formSmash_j_idt622",multiple:true});
##### Funder

EU, FP7, Seventh Framework Programme, 279611
##### Note

##### List of papers

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.

QC 20170509

Available from: 2017-05-10 Created: 2017-05-09 Last updated: 2018-01-13Bibliographically approved1. Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)$(function(){PrimeFaces.cw("OverlayPanel","overlay664987",{id:"formSmash:j_idt738:0:j_idt745",widgetVar:"overlay664987",target:"formSmash:j_idt738: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_idt738:1:j_idt745",widgetVar:"overlay1069716",target:"formSmash:j_idt738:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

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

4. Trade-offs between time and memory in a tighter model of CDCL SAT solvers$(function(){PrimeFaces.cw("OverlayPanel","overlay1047764",{id:"formSmash:j_idt738:3:j_idt745",widgetVar:"overlay1047764",target:"formSmash:j_idt738:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

5. Hardness of Approximation in PSPACE and Separation Results for Pebble Games$(function(){PrimeFaces.cw("OverlayPanel","overlay928552",{id:"formSmash:j_idt738:4:j_idt745",widgetVar:"overlay928552",target:"formSmash:j_idt738:4:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

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

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