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

文章基本信息

  • 标题:Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond
  • 本地全文:下载
  • 作者:Olga Tveretina ; Carsten Sinz ; Hans Zantema
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2009
  • 卷号:2009
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponentialsize and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that any arbitrary OBDD Apply refutation of the pigeonhole formula has an exponentialsize: we prove that the size of one of the intermediate OBDDs is at least (114n). We also present a family of CNFs that require exponential increase for all OBDD refutations based on Apply method to simulate unrestricted resolution refutation.

  • 关键词:Ordered Binary Decision Diagrams; pigeonhole formulas; Proof Complexity; Resolution
国家哲学社会科学文献中心版权所有