We prove that there is a constant K such that emph{Tseitin} formulas for an undirected graph G requires proofs of size 2 t w ( G ) (1 d ) in depth- d Frege systems for d K log n log log n , where t w ( 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 t w ( G ) (1 d ) pol y ( 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.
展开▼
机译：我们证明存在一个常数K，使得无向图G的 emph {Tseitin}公式需要在d K log n log log n的深度d Frege系统中证明尺寸为2 tw（G）（1 d）。 tw（G）是G的树宽。这将Hstad最近对网格图的下界扩展到任何图。此外，我们证明了在最高指数中我们的约束与乘法常数的紧密性。即，我们表明，如果图G的Tseitin公式的大小为s，那么对于所有足够大的d，它的深度d弗雷格证明的大小为2 t w（G）（1 d）pol y（s）。通过该结果，我们解决了M. Alekhnovich和A. Razborov提出的问题，即表明Tseitin公式的类别对于解析是准自动的。
展开▼
