Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

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

Bounded-depth Frege complexity of Tseitin formulas for all graphs

RSS-Feed




Revision #1
Authors: Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova
Accepted on: 12th May 2019 12:34
Downloads: 192
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
Downloads: 89
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 $\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)$.
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.



ISSN 1433-8092 | Imprint