Logic seminar

On the proof complexity of Resolution over Polynomial Calculus

The refutation system Res_R(PC_d) is a natural extension of the Resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called Res_R(lin). One of the important open problems in Proof Complexity is proving lower bounds for Res_R(lin) when R is a finite field such as F_2. Interestingly, Res_{F_2}(lin) is fairly strong, and there is no known nontrivial lower bound for it, but for Res^*_R(lin) (tree-like Res_R(lin)) we know exponential lower bounds for every finite field.

For the stronger systems Res_R(PC_d) and Res_R^*(PC_d) for d>1 on finite ring R, there is no known lower bounds. In this talk, we prove a size-width relation for Res_R(PC_d) and Res^*_R(PC_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for Res and Res^* using extension variables. As a by product, we get the following new lower bounds for every finite field F:
1. We prove a nontrivial lower bound for Res_F(PC_d) for fixed d: a nearly quadratic lower bound for mod q Tseitin formulas (char(F) is not equal to q).
2. We also prove superpolynomial and exponential lower bounds for Res^*_F(PC_d) where d is not too large with respect to n for the following principles:
a. mod q Tseitin formulas (char(F) is not equal to q),
b. Random k-CNFs.