Trade-offs between size and degree in polynomial calculus
(2020) 11th Innovations in Theoretical Computer Science Conference, ITCS 2020 In Leibniz International Proceedings in Informatics, LIPIcs 151.- Abstract
Building on [Clegg et al.’96], [Impagliazzo et al.’99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(n log S). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen’16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is... (More)
Building on [Clegg et al.’96], [Impagliazzo et al.’99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(n log S). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen’16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.
(Less)
- author
- Lagarde, Guillaume ; Nordström, Jakob LU ; Sokolov, Dmitry LU and Swernofsky, Joseph
- organization
- publishing date
- 2020-01
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Colored polynomial local search, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Resolution, Size-degree trade-off
- host publication
- 11th Innovations in Theoretical Computer Science Conference, ITCS 2020
- series title
- Leibniz International Proceedings in Informatics, LIPIcs
- editor
- Vidick, Thomas
- volume
- 151
- article number
- 72
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 11th Innovations in Theoretical Computer Science Conference, ITCS 2020
- conference location
- Seattle, United States
- conference dates
- 2020-01-12 - 2020-01-14
- external identifiers
-
- scopus:85078035428
- ISSN
- 1868-8969
- ISBN
- 9783959771344
- DOI
- 10.4230/LIPIcs.ITCS.2020.72
- language
- English
- LU publication?
- yes
- id
- 942f6ecd-ac4c-41fc-9d2b-30bdaf1b9e9b
- date added to LUP
- 2020-12-18 22:15:00
- date last changed
- 2022-05-12 08:44:27
@inproceedings{942f6ecd-ac4c-41fc-9d2b-30bdaf1b9e9b, abstract = {{<p>Building on [Clegg et al.’96], [Impagliazzo et al.’99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(n log S). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen’16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.</p>}}, author = {{Lagarde, Guillaume and Nordström, Jakob and Sokolov, Dmitry and Swernofsky, Joseph}}, booktitle = {{11th Innovations in Theoretical Computer Science Conference, ITCS 2020}}, editor = {{Vidick, Thomas}}, isbn = {{9783959771344}}, issn = {{1868-8969}}, keywords = {{Colored polynomial local search; PCR; Polynomial calculus; Polynomial calculus resolution; Proof complexity; Resolution; Size-degree trade-off}}, language = {{eng}}, publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}}, series = {{Leibniz International Proceedings in Informatics, LIPIcs}}, title = {{Trade-offs between size and degree in polynomial calculus}}, url = {{http://dx.doi.org/10.4230/LIPIcs.ITCS.2020.72}}, doi = {{10.4230/LIPIcs.ITCS.2020.72}}, volume = {{151}}, year = {{2020}}, }