A generalized method for proving polynomial calculus degree lower bounds
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
A generalized method for proving polynomial calculus degree lower bounds. / Mikša, Mladen; Nordström, Jakob.
30th Conference on Computational Complexity, CCC 2015. red. / David Zuckerman. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. s. 467-487 (Leibniz International Proceedings in Informatics, LIPIcs, Bind 33).Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - A generalized method for proving polynomial calculus degree lower bounds
AU - Mikša, Mladen
AU - Nordström, Jakob
PY - 2015/6/1
Y1 - 2015/6/1
N2 - 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.
AB - 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.
KW - Degree
KW - Functional pigeonhole principle
KW - Lower bound
KW - PCR
KW - Polynomial calculus
KW - Polynomial calculus resolution
KW - Proof complexity
KW - Size
UR - http://www.scopus.com/inward/record.url?scp=84958256296&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CCC.2015.467
DO - 10.4230/LIPIcs.CCC.2015.467
M3 - Article in proceedings
AN - SCOPUS:84958256296
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 467
EP - 487
BT - 30th Conference on Computational Complexity, CCC 2015
A2 - Zuckerman, David
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 30th Conference on Computational Complexity, CCC 2015
Y2 - 17 June 2015 through 19 June 2015
ER -
ID: 251869007