|Résumé||Introduced by Cleggs et al. (STOC'96) to capture Gröbner basis computations, Polynomial Calculus Resolution (PCR) is an algebraic proof system for certifying the unsatisfiability of CNF formulas. Impagliazzo et al. (CC'99) established that if an unsatisfiable k-CNF formula over n variables has a refutation of small size in PCR (that is, polynomial size), then this formula also has a refutation of small degree, i.e., O(sqrt(n log n)). A natural question is to know whether we can achieve both small size and small degree in the same refutation.
A situation similar in spirit arises in the more classical resolution proof system where degree is replaced by width and size by length. In this setting, Thapen (TOC '16) adressed the tradeoff question by providing a negative answer: the decrease in width necessarily comes at the expense of an exponential blow-up in length.
Extending ideas from Thapen, our main result is to prove that a strong size-degree tradeoff is also necessary in PCR.
Joint work with Jakob Nordström, Dmitry Sokolov, Joseph Swernofsky |