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...
more
