Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Trade-offs between size and degree in polynomial calculus

Lagarde, Guillaume ; Nordström, Jakob LU ; Sokolov, Dmitry LU and Swernofsky, Joseph (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)
Please use this url to cite or link to this publication:
author
; ; and
organization
publishing date
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}},
}