Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Revision(s):

Revision #3 to TR20-034 | 26th January 2021 01:16

#### On Proof complexity of Resolution over Polynomial Calculus

Revision #3
Authors: Erfan Khaniki
Accepted on: 26th January 2021 01:16
Keywords:

Abstract:

The proof system \$Res(PC_1/R)\$ is a natural extension of the Resolution proof system that instead of clauses of literals operates with disjunctions of degree \$d\$ polynomials over a ring \$R\$ with boolean variables. Proving super-polynomial lower bounds for the size of \$Res(PC_1/R)\$-refutations of CNFs is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for \$Res(PC_1/\mathbb{F})\$ when \$\mathbb{F}\$ is a finite field such as \$\mathbb{F}_2\$. In this paper, we investigate \$Res(PC_1/R)\$ and tree-like \$Res(PC_1/R)\$ and prove size-width relations for them when \$R\$ is a finite ring. As an application, we get for every finite field \$\mathbb{F}\$ the following lower bounds on the number of clauses:

(1) We prove almost quadratic lower bounds for \$Res(PC_d/\mathbb{F})\$-refutations for every fixed \$d\$. The new lower bounds are for the following CNFs:

(a) mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$),

(b) Random \$k\$-CNFs with linearly many clauses.

(2) We also prove super-polynomial and exponential lower bounds for tree-like \$Res(PC_d/\mathbb{F})\$-refutations where \$d\$ is not too large with respect to \$n\$ for the following CNFs:

(a) mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$),
(b) Random \$k\$-CNFs,
(c) Pigeonhole principle.

The above results imply the first nontrivial lower bounds for \$Res(\oplus)\$ [Itsykson and Sokolov '14, Itsykson and Sokolov '20], \$Res(lin_\mathbb{F})\$ where \$\mathbb{F}\$ is a finite field [Part and Tzameret '20], and \$R(PC_d/\mathbb{F}_2)\$ [Kraj{\'\i}{\v{c}}ek '18]. Moreover, they imply the first super-polynomial and exponential lower bounds for tree-like \$R(PC_d/\mathbb{F}_2)\$-refutations of mod \$q\$ Tseitin formulas, random \$k\$-CNFs, and the Pigeonhole principle.

Changes to previous version:

New lower bounds for \$PHP^m_n\$ were added.

Revision #2 to TR20-034 | 28th November 2020 15:57

#### On Proof complexity of Resolution over Polynomial Calculus

Revision #2
Authors: Erfan Khaniki
Accepted on: 28th November 2020 15:57
Keywords:

Abstract:

The proof system \$Res(PC_d/R)\$ is a natural extension of the Resolution proof system that instead of clauses of literals operates with disjunctions of degree \$d\$ polynomials over a ring \$R\$ with boolean variables. Proving super-polynomial lower bounds for the size of \$Res(PC_1/R)\$-refutations of CNFs is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for \$Res(PC_1/\mathbb{F})\$ when \$\mathbb{F}\$ is a finite field such as \$\mathbb{F}_2\$. In this paper, we investigate \$Res(PC_d/R)\$ and tree-like \$Res(PC_d/R)\$ and prove size-width relations for them when \$R\$ is a finite ring. As an application, we get for every finite field \$\mathbb{F}\$ the following lower bounds on the number of clauses:
(1) We prove almost quadratic lower bounds for \$Res(PC_d/\mathbb{F})\$-refutations for every fixed \$d\$. The new lower bounds are for the following CNFs:
(a) mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$),
(b) Random \$k\$-CNFs with linearly many clauses.
(2) We also prove super-polynomial and exponential lower bounds for tree-like \$Res(PC_d/\mathbb{F})\$-refutations where \$d\$ is not too large with respect to \$n\$ for the following CNFs:
(a) mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$),
(b) Random \$k\$-CNFs.
The above results imply the first nontrivial lower bounds for \$Res(\oplus)\$ \cite{is,is2}, \$Res(lin_\mathbb{F})\$ where \$\mathbb{F}\$ is a finite field \cite{pt}, and \$R(PC_d/\mathbb{F}_2)\$ \cite{krrandom}. Moreover, they imply the first super-polynomial and exponential lower bounds for tree-like \$R(PC_d/\mathbb{F}_2)\$-refutations of mod \$q\$ Tseitin formulas and random \$k\$-CNFs.

Changes to previous version:

Added detailed proofs of the main theorems.

Revision #1 to TR20-034 | 20th April 2020 20:07

#### On Proof complexity of Resolution over Polynomial Calculus

Revision #1
Authors: Erfan Khaniki
Accepted on: 20th April 2020 20:07
Keywords:

Abstract:

The refutation system \${Res}_R({PC}_d)\$ is a natural extension of 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})\$. Based on properties of \$R\$, \${Res}_R({lin})\$ systems can be too strong to prove lower bounds for CNFs with current methods. The reachable goal might be proving lower bounds for \${Res}_R({lin})\$ when \$R\$ is a finite field such as \$\mathbb{F}_2\$. Interestingly, \${Res}_{\mathbb{F}_2}({lin})\$ is also 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 till now. In this paper we will investigate these refutation systems and make some progress toward understanding these systems, including the case \$d=1\$. 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 \$\mathbb{F}\$:
(1) We prove the first nontrivial lower bounds for \${Res}_\mathbb{F}({PC}_d)\$ for fixed \$d\$: a nearly quadratic lower bounds for:
(a) mod \$q\$ Tseitin formulas (\$char(\F)\neq q\$),
(b) Random \$k\$-CNFs with linearly many clauses.
(2) We also prove superpolynomial and exponential lower bounds for \${Res}^*_\mathbb{F}({PC}_{d})\$ where \$d\$ is not too large with respect to \$n\$ for the following principles:
(a) mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$),
(b) Random \$k\$-CNFs.

Changes to previous version:

Fixed some typos

### Paper:

TR20-034 | 12th March 2020 14:28

#### On Proof complexity of Resolution over Polynomial Calculus

TR20-034
Authors: Erfan Khaniki
Publication: 13th March 2020 17:56
Keywords:

Abstract:

The refutation system \${Res}_R({PC}_d)\$ is a natural extension of 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})\$. Based on properties of \$R\$, \${Res}_R({lin})\$ systems can be too strong to prove lower bounds for CNFs with current methods. The reachable goal might be proving lower bounds for \${Res}_R({lin})\$ when \$R\$ is a finite field such as \$\mathbb{F}_2\$. Interestingly, \${Res}_{\mathbb{F}_2}({lin})\$ is also 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 till now. In this paper we will investigate these refutation systems and make some progress toward understanding these systems, including the case \$d=1\$. 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 \$\mathbb{F}\$:
(1) We prove the first nontrivial lower bounds for \${Res}_\mathbb{F}({PC}_d)\$ for fixed \$d\$: a nearly quadratic lower bounds for mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$) for suitable graphs.
(2) We also prove superpolynomial and exponential lower bounds for \${Res}^*_\mathbb{F}({PC}_{d})\$ where \$d\$ is not too large with respect to \$n\$ for the following principles:
(a) mod \$q\$ Tseitin formulas (\$char(\mathbb{F})\neq q\$),
(b) Random \$k\$-CNFs.

ISSN 1433-8092 | Imprint