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

文章基本信息

  • 标题:On Tseitin formulas, read-once branching programs and treewidth
  • 本地全文:下载
  • 作者:Ludmila Glinskih ; Dmitry Itsykson
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2019
  • 卷号:2019
  • 页码:1-14
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    We show that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an n n grid graph has size at least 2 ( n ) . Then using the Excluded Grid Theorem by Robertson and Seymour we show that for arbitrary graph G ( V E ) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least 2 ( t w ( G ) ) for all 1 36 , where t w ( G ) is the treewidth of G (for planar graphs and some other classes of graphs the statement holds for = 1 ). We also show an upper bound O ( E 2 p w ( G ) ) , where p w ( G ) is the pathwidth of G .We apply the mentioned results in the analysis of the complexity of derivation in the proof system OBD D ( r eorderin g ) and show that any OBD D ( r eorderin g ) -refutation of an unsatisfiable Tseitin formula based on a graph G has size at least 2 ( t w ( G ) ) .

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