首页    期刊浏览 2024年09月15日 星期日
登录注册

文章基本信息

  • 标题:Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs
  • 本地全文:下载
  • 作者:Dmitry Itsykson ; Artur Riazanov ; Danil Sagunov
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2019
  • 卷号:2019
  • 页码:1-37
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    We show that the size of any regular resolution refutation of Tseitin formula T ( G c ) based on a graph G is at least 2 ( t w ( G ) log n ) , where n is the number of vertices in G and t w ( G ) is the treewidth of G . For constant degree graphs there is known upper bound 2 O ( t w ( G )) [AR11, GTT18], so our lower bound is tight up to a logarithmic factor in the exponent.In order to prove this result we show that any regular resolution proof of Tseitin formula T ( G c ) of size S can be converted to a read-once branching program computing satisfiable Tseitin formula T ( G c ) of size S O ( log n ) . Then we show that any read-once branching program computing satisfiable Tseitin formula T ( G c ) has size at least 2 ( t w ( G )) ; the latter improves the recent result of Glinskih and Itsykson [GI19].

  • 关键词:lower bound ; read-once branching program ; regular resolution ; Treewidth ; Tseitin Formulas
国家哲学社会科学文献中心版权所有