首页    期刊浏览 2025年02月26日 星期三
登录注册

文章基本信息

  • 标题:Strong (D)QBF Dependency Schemes via Implication-free Resolution Path
  • 本地全文:下载
  • 作者:Olaf Beyersdorff ; Joshua Blinkhorn ; Tomáš Peitl
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2021
  • 卷号:21
  • 语种:English
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new infinite collection of implication-free DQBF dependency schemes that generalise the reflexive resolution path dependency scheme. We establish soundness of all these schemes, implying that they can be used in any DQBF proof system. We further explore the power of QBF and DQBF resolution systems parameterised by implication-free dependency schemes and show that the hierarchical structure naturally present among the dependency schemes translates isomorphically to a hierarchical structure of parameterised proof systems with respect to p-simulation. As a special case, we demonstrate that our new schemes are exponentially stronger than the reflexive resolution path dependency scheme when used in Q-resolution, thus resulting in the strongest QBF dependency schemes known to date.
  • 关键词:dependency schemes;DQBF;Proof Complexity;QBF;QBF proof systems
国家哲学社会科学文献中心版权所有