首页    期刊浏览 2025年05月01日 星期四
登录注册

文章基本信息

  • 标题:IPS-like Proof Systems Based on Binary Decision Diagrams
  • 本地全文:下载
  • 作者:Alexander Knop
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2017
  • 卷号:2017
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    It is well-known that there is equivalence between ordered resolution and ordered binary decision diagrams (OBDD) [LNNW95]; i.e., for any unsatisfiable formula ?, the size of the smallest ordered resolution refutation of ? equal to the size of the smallest OBDD for the canonical search problem corresponding to ?. But there is no such equivalence between resolution and branching programs (BP). In this paper, we study different proof systems equivalent to classes of branching programs between BP and OBDD. These proof systems are similar to roABP-IPS, an algebraic proof system defined by Forbes et al. [FSTW16] and based on the ideal proof system introduced by Grochow and Pitassi [GP14]. In the paper, we show that proof systems equivalent to k-OBDD are not comparable with resolution and cutting planes. We also prove exponential lower bounds for these proof systems on Tseitin formulas. Additionally, we show that proof systems equivalent to (1,+k)-BP are strictly stronger than regular resolution.

  • 关键词:Expander Graphs ; Karchmer-Wigderson games ; OBDD ; read once branching programs
国家哲学社会科学文献中心版权所有