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

A generalized method for proving polynomial calculus degree lower boundsPrimeFaces.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();
}
}
2015 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Dagstuhl Publishing , 2015, Vol. 33, p. 467-487Conference paper, Published paper (Refereed)
##### Resource type

Text
##### Abstract [en]

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

Dagstuhl Publishing , 2015. Vol. 33, p. 467-487
##### Keywords [en]

Degree, Functional pigeonhole principle, Lower bound, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Size
##### National Category

Mathematical Analysis
##### Identifiers

URN: urn:nbn:se:kth:diva-187389DOI: 10.4230/LIPIcs.CCC.2015.467Scopus ID: 2-s2.0-84958256296ISBN: 978-393989781-1 (print)OAI: oai:DiVA.org:kth-187389DiVA, id: diva2:931257
##### Conference

30th Conference on Computational Complexity, CCC 2015; Portland; United States
#####

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

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

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

##### In thesis

We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. ’99] also on proof size. [Alekhnovich and Razborov’03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov’02], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution. Thus, while Onto-FPHP formulas are easy for polynomial calculus, as shown in [Riis’93], both FPHP and Onto-PHP formulas are hard even when restricted to bounded-degree expanders.

QC 20160527

Available from: 2016-05-27 Created: 2016-05-23 Last updated: 2016-11-30Bibliographically approved1. On Complexity Measures in Polynomial Calculus$(function(){PrimeFaces.cw("OverlayPanel","overlay1051001",{id:"formSmash:j_idt785:0:j_idt789",widgetVar:"overlay1051001",target:"formSmash:j_idt785:0:parentLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

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

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