Are Short Proofs Narrow? QBF Resolution Is Not So Simple
Are Short Proofs Narrow? QBF Resolution Is Not So Simple
复制标题
DOI：
10.1145/3157053
复制
发表时间：
2018-02-01
影响因子：
0.5
通讯作者：
Shukla, Anil
中科院分区：
文献类型：
--
作者：
Beyersdorff, Olaf;Chew, Leroy;Shukla, Anil
由Ben-Sasson和Wigderson （J. ACM 2001）撰写的开创性论文“短证明是窄分辨率的简化”介绍了今天可以论证的获得分辨率下界的主要技术：显示证明宽度的下界。分辨率的另一个重要度量是空间，在他们的基础工作中，Atserias和Dalmau (J. Comput；系统。Sci. 2008)表明空间的下界同样可以通过宽度的下界得到。在本文中，我们评估了类似的技术是否对量化布尔公式（QBFs）的分辨率演算有效。有许多不同的QBF解析演算，如q -解析（命题解析到QBF的经典扩展）和较新的演算。Exp+ Res和IR-calc。对于这些系统，出现了一幅复杂的画面。我们的主要结果表明，大小和宽度之间以及空间和宽度之间的关系在q分辨率中急剧失效，即使在其较弱的树状版本中也是如此。另一方面，对于基于展开式的分辨率系统，我们得到了积极的结果。然而，Exp+ Res和IR-calc仅在弱树状模型中存在。从技术上讲，我们的负面结果依赖于显示宽度下界以及同时显示大小和空间的上界。对于我们的积极结果，我们展示了在QBF分辨率计算之间的空间和宽度保持模拟。
The ground-breaking paper "Short Proofs Are Narrow-ResolutionMade Simple" by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that lower bounds for space again can be obtained via lower bounds for width.In this article, we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBFs). There are a number of different QBF resolution calculi like Q-resolution (the classical extension of propositional resolution to QBF) and the more recent calculi. Exp+ Res and IR-calc. For these systems, a mixed picture emerges. Our main results show that the relations both between size and width and between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems. Exp+ Res and IR-calc, however, only in the weak tree-like models.Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results, we exhibit space and width-preserving simulations between QBF resolution calculi.