首页    期刊浏览 2024年11月07日 星期四
登录注册

文章基本信息

  • 标题:Bounded-depth Frege complexity of Tseitin formulas for all graphs
  • 本地全文:下载
  • 作者:Nicola Galesi ; Dmitry Itsykson ; Artur Riazanov
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2019
  • 卷号:2019
  • 页码:1-19
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    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.

国家哲学社会科学文献中心版权所有