ECCC-Report TR19-069https://eccc.weizmann.ac.il/report/2019/069Comments and Revisions published for TR19-069en-usSun, 12 May 2019 12:34:59 +0300
Revision 1
| Bounded-depth Frege complexity of Tseitin formulas for all graphs |
Artur Riazanov,
Dmitry Itsykson,
Nicola Galesi,
Anastasia Sofronova
https://eccc.weizmann.ac.il/report/2019/069#revision1We 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.Sun, 12 May 2019 12:34:59 +0300https://eccc.weizmann.ac.il/report/2019/069#revision1
Paper TR19-069
| Bounded-depth Frege complexity of Tseitin formulas for all graphs |
Artur Riazanov,
Dmitry Itsykson,
Nicola Galesi,
Anastasia Sofronova
https://eccc.weizmann.ac.il/report/2019/069We 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.Sun, 12 May 2019 12:21:17 +0300https://eccc.weizmann.ac.il/report/2019/069