Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Revision(s):

Revision #1 to TR19-069 | 12th May 2019 12:34

#### Bounded-depth Frege complexity of Tseitin formulas for all graphs

Revision #1
Authors: Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova
Accepted on: 12th May 2019 12:34
Keywords:

Abstract:

We prove that there is a constant $K$ such that \emph{Tseitin} formulas for an undirected graph $G$ requires proofs of
size $2^{\mathrm{tw}(G)^{\Omega(1/d)}}$ in depth-$d$ Frege systems for $d<\frac{K \log n}{\log \log n}$, where $\mathrm{tw}(G)$ is the treewidth of $G$. This extends Håstad's recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent.
Namely, we show that if a Tseitin formula for a graph $G$ has size $s$, then for all large enough $d$, it has a depth-$d$ Frege proof of size $2^{\mathrm{tw}(G)^{\mathcal{O}(1/d)}} \mathrm{poly}(s)$.
Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

### Paper:

TR19-069 | 6th May 2019 17:57

#### Bounded-depth Frege complexity of Tseitin formulas for all graphs

TR19-069
Authors: Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova
Publication: 12th May 2019 12:21
We prove that there is a constant $K$ such that \emph{Tseitin} formulas for an undirected graph $G$ requires proofs of
size $2^{\mathrm{tw}(G)^{\Omega(1/d)}}$ in depth-$d$ Frege systems for $d<\frac{K \log n}{\log \log n}$, where $\tw(G)$ is the treewidth of $G$. This extends H{\aa}stad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent.
Namely, we show that if a Tseitin formula for a graph $G$ has size $s$, then for all large enough $d$, it has a depth-$d$ Frege proof of size $2^{\mathrm{tw}(G)^{\O(1/d)}} \mathrm{poly}(s)$.