In this talk, we study versions of Polynomial Calculus and Sum-of-Squares proof systems. Current techniques for size lower on these proof systems bounds significantly use {0, 1} encoding of variables. More formally, we need to be able to assign any variable by a feasible value in a way to kill a term, that helps us to reduce a question about size to a question about degree.

We know the for ``Fourier'' $\{\pm 1\}$ encoding of boolean variables degree lower bound is not enough to prove size lower bounds [Buss et al. 2001]. In this talk we present show exponential lower bounds on monomial size of proofs in SoS and PCR as well as separation between these systems. It is a solution to an open problem from [Impagliazzo, Mouli, Pitassi 2019].

Докладчиком предлагается рассмотреть две темы. Распределение времени семинара между темами будет определяться пожеланиями слушателей семинара.

Title: A proof of the Sensitivity Conjecture

In this talk we will show that for any function f block sensitivity of f is bounded by a polynomial of sensitivity of f.

Based on paper of Hao Huang: "Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture".

Title: A tradeoff between length and width in PCR

For various proof systems we know that proof of small size can be translated into a proof of small degree (or small width). In this constructions, the size of the final proof is usually exponential in terms of variables of the formula. For Resolution Thapen showed that it is necessary. We extend his result into polynomial calculus proof system.

More formally:
We construct a formula \varphi of size n that in polynomial calculus resolution (PCR) has a refutation of polynomial size and degree c := n^{1 - o(1)} and hence a refutation of exponential size and degree n^{0.5 + o(1)}. However, we show that there is no refutation achieving both polynomial size and degree at most c - O(\lg n)$ at the same time.

Joint work with Guillaume Lagarde, Jakob Nordström, Joseph Swernofsky.

I will show how to remove a small number of edges from a hypergraph of small degree to break it into small connected components. I will then use it to solve CSP-SAT instances in which no variable appears in too many constraints and to give refutations of Tseitin formulas in small degree graphs with savings independent of the degree.

Joint work with Michal Koucký and Vojtěch Rödl.