A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
(2024) In Journal of the ACM 71(6).- Abstract
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 conjunctive normal form (CNF) formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop their techniques 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. We also show how a weaker structural condition is sufficient to obtain lower... (More)
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 conjunctive normal form (CNF) formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop their techniques 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. We also show how a weaker structural condition is sufficient to obtain lower bounds on width for the resolution proof system, and give a unified treatment that highlights similarities and differences between resolution and polynomial calculus (PC) lower bounds. As a corollary of our main technical theorem, 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 (PCR). 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.
(Less)
- author
- Mikša, Mladen and Nordström, Jakob LU
- organization
- publishing date
- 2024-11
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- degree, expander graph, functional pigeonhole principle, lower bound, PCR, polynomial calculus, polynomial calculus resolution, Proof complexity, resolution, size, width
- in
- Journal of the ACM
- volume
- 71
- issue
- 6
- article number
- 37
- publisher
- Association for Computing Machinery
- external identifiers
-
- scopus:85212293957
- ISSN
- 0004-5411
- DOI
- 10.1145/3675668
- language
- English
- LU publication?
- yes
- id
- 0686453d-de72-467e-ba1d-fbd199dd8a26
- date added to LUP
- 2025-01-21 15:21:20
- date last changed
- 2025-05-28 01:23:00
@article{0686453d-de72-467e-ba1d-fbd199dd8a26,
abstract = {{<p>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 conjunctive normal form (CNF) formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop their techniques 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. We also show how a weaker structural condition is sufficient to obtain lower bounds on width for the resolution proof system, and give a unified treatment that highlights similarities and differences between resolution and polynomial calculus (PC) lower bounds. As a corollary of our main technical theorem, 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 (PCR). 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.</p>}},
author = {{Mikša, Mladen and Nordström, Jakob}},
issn = {{0004-5411}},
keywords = {{degree; expander graph; functional pigeonhole principle; lower bound; PCR; polynomial calculus; polynomial calculus resolution; Proof complexity; resolution; size; width}},
language = {{eng}},
number = {{6}},
publisher = {{Association for Computing Machinery}},
series = {{Journal of the ACM}},
title = {{A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds}},
url = {{http://dx.doi.org/10.1145/3675668}},
doi = {{10.1145/3675668}},
volume = {{71}},
year = {{2024}},
}