Abstract
The proof system Res(PCd, (R)) is a natural extension of the Resolution proof system that instead of disjunctions of literals operates with disjunctions of degree d multivariate polynomials over a ring R with Boolean variables. Proving super-polynomial lower bounds for the size of Res( PC1, (R))-refutations of Conjunctive normal forms (CNFs) is one of the important problems in propositional proof complexity.
The existence of such lower bounds is even open for Res( PC1,(F)) when F is a finite field, such as F-2. In this article, we investigate Res(PCd, (R)) and tree-like Res(PCd, (R)) and prove size-width relations for them when R is a finite ring.
As an application, we prove new lower bounds and reprove some known lower bounds for every finite field F as follows: (1) We prove almost quadratic lower bounds for Res(PCd, F)-refutations for every fixed d. The new lower bounds are for the following CNFs: (a) Mod q Tseitin formulas (char (F) not equal q) and Flow formulas, (b) Random k-CNFs with linearly many clauses. (2) We also prove super-polynomial (more than nk for any fixed k) and also exponential (2(n epsilon) for an epsilon > 0) lower bounds for tree-like Res(PCd, F)-refutations based on how big d is with respect to n for the following CNFs: (a) Mod q Tseitin formulas (char (F) not equal q) and Flow formulas, (b) Random k-CNFs of suitable densities, (c) Pigeonhole principle and Counting mod q principle.
The lower bounds for the dag-like systems are the first nontrivial lower bounds for these systems, including the case d = 1. The lower bounds for the tree-like systems were known for the case d = 1 (except for the Counting mod q principle, in which lower bounds for the case d > 1 were known too).
Our lower bounds extend those results to the case where d > 1 and also give new proofs for the case d = 1.