文章基本信息

标题：A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
本地全文：下载
作者：Mladen Miksa ; Jakob Nordstr{\"o}m
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：33
页码：467-487
DOI：10.4230/LIPIcs.CCC.2015.467
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We study the problem of establishing 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.
关键词：proof complexity; polynomial calculus; polynomial calculus resolution; PCR; degree; size; functional pigeonhole principle; lower bound