Bounded-depth Frege complexity of Tseitin formulas for all graphs
Bounded-depth Frege complexity of Tseitin formulas for all graphs
复制标题
所有图的 Tseitin 公式的有界深度弗雷格复杂度
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
A. Sofronova
中科院分区：
文献类型：
--
作者：
Nicola Galesi;D. Itsykson;Artur Riazanov;A. Sofronova
我们证明了存在一个常数K，使得无向图G的tseittin公式需要在深度-d Frege系统中证明大小为2twpGq Ωp1{dq，其中twpGq是G的树宽度，这将H ^ H ^ H的最近下界扩展到任何图。进一步，我们证明了上指数上一个乘常数的约束的严密性。也就是说，我们证明，如果图G的tseittin公式的大小为s，那么对于所有足够大的d，它有一个深度d的Frege证明，大小为2twpGq Op1{dq polysq。通过这一结果，我们解决了M. Alekhnovich和A. Razborov提出的关于tseittin公式类在求解上是拟自动化的问题。
We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2twpGq Ωp1{dq in depth-d Frege systems for d ă K logn log logn , where twpGq is the treewidth of G. This extends H̊astad 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 2twpGq Op1{dq polypsq. 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.