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

文章基本信息

  • 标题:Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams
  • 本地全文:下载
  • 作者:Luke Friedman ; Yixin Xu
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2013
  • 卷号:2013
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. Krajicek proved exponential lower bounds for a strong variant of this system using feasible interpolation, and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived from the Pigeonhole Principle.In this paper we prove the first lower bounds for refuting randomly generated unsatisfiable formulas in restricted versions of this OBDD-based proof system.In particular we consider two systems OBDD* and OBDD+; OBDD* is restricted by having a fixed, predetermined variable order for all OBDDs in its refutations, and OBDD+ is restricted by having a fixed order in which the clauses of the input formula must be processed. We show that for some constant 0">0, with high probability an OBDD* refutation of an unsatisfiable random 3-CNF formula must be of size at least 2n, and an OBDD+ refutation of an unsatisfiable random 3-XOR formula must be of size at least 2n.

  • 关键词:OBDDs; Ordered Binary Decision Diagrams; propositional proof complexity; Random formulas
国家哲学社会科学文献中心版权所有