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

文章基本信息

  • 标题:On OBDD-based algorithms and proof systems that dynamically change order of variables
  • 本地全文:下载
  • 作者:Dmitry Itsykson ; Alexander Knop ; Andrei Romashchenko
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2019
  • 卷号:2019
  • 页码:1-30
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based proof systems that additionally contain a rule that allows changing the order in OBDDs. At first, we consider a proof system OBDD( , reordering) that uses the conjunction (join) rule and the rule that allows changing the order. We exponentially separate this proof system from OBDD( ) proof system that uses only the conjunction rule. We prove two exponential lower bounds on the size of OBDD( , reordering) refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD( ) proofs and the second one extends the result of Tveretina et al. from OBDD( ) to OBDD( , reordering).In 2004 Pan and Vardi proposed an approach to the propositional satisfiability problem based on OBDDs and symbolic quantifier elimination (we denote algorithms based on this approach as OBDD( , ) algorithms). An instance of the propositional satisfiability problem is considered as an existential quantified propositional formula. The algorithm chooses an order on variables and creates an ordered binary decision diagram (OBDD) D that initially represents the constant 1 function. Then the algorithm downloads to D clauses of the CNF one by one, and applies to D the elimination of the existential quantifier for variable x if all clauses that contain x are already downloaded. We augment these algorithms with the operation of reordering of variables and call the new scheme OBDD( , , reordering) algorithms. We notice that there exists an OBDD( , ) algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over F 2 that are hard for OBDD( , , reordering) algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F 2 that correspond to some checksum matrices of error correcting codes.

  • 关键词:communication complexity ; Error Correcting Codes ; OBDD ; Proof Complexity ; satisfiability algorithm
国家哲学社会科学文献中心版权所有