On the Relative Strength of Pebbling and Resolution
On the Relative Strength of Pebbling and Resolution
复制标题
关于卵石和分辨率的相对强度
DOI：
10.1145/2159531.2159538
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Jakob Nordström
中科院分区：
文献类型：
--
作者：
Jakob Nordström
在过去的十年里，在证明复杂性的背景下，人们对卵石博弈的兴趣又恢复了。Pebbling已被证明是一个有用的工具，用于研究基于分辨率的证明系统，比较不同子系统的强度，显示证明空间的界限，并建立大小空间的权衡。典型的方法是将图上的卵石博弈编码为CNF公式，然后认为这个公式的证明必须继承底层图的卵石性质（的各个方面）。不幸的是，这里使用的缩减并不严格。要通过pebbling模拟分辨率证明，需要非确定性黑白pebbling的全部强度，而分辨率仅已知能够模拟确定性黑色pebbling。因此，为了得到强有力的结果，需要找到特定的图族，这些图族要么对黑色和黑白卵石具有基本相同的性质（一般来说根本不成立），要么在分辨率上允许模拟黑白卵石。本文有助于这两种方法。首先，我们设计了一个限制形式的黑白卵石，可以模拟的分辨率，并表明，有图形的家庭，这种限制卵石可以渐近优于黑色卵石。这证明了，也许有点出乎意料，分辨率可以严格击败黑色的鹅卵石，特别是在[Ben-Sasson和Nordstrom 2008]中鹅卵石公式的空间下限是紧的。其次，我们提出了一个多功能的参数化图形家庭基本上相同的属性为黑色和黑白卵石，这使得尖锐的同时权衡黑色和黑白卵石的各种参数设置。我们的两个贡献都有助于获得基于分辨率的证明系统的时空权衡结果[Ben-Sasson and Nordstrom 2009]。
The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. The typical approach has been to encode the pebble game played on a graph as a CNF formula and then argue that proofs of this formula must inherit (various aspects of) the pebbling properties of the underlying graph. Unfortunately, the reductions used here are not tight. To simulate resolution proofs by pebblings, the full strength of nondeterministic black-white pebbling is needed, whereas resolution is only known to be able to simulate deterministic black pebbling. To obtain strong results, one therefore needs to find specific graph families which either have essentially the same properties for black and black-white pebbling (not at all true in general) or which admit simulations of black-white pebblings in resolution. This paper contributes to both these approaches. First, we design a restricted form of black-white pebbling that can be simulated in resolution and show that there are graph families for which such restricted pebblings can be asymptotically better than black pebblings. This proves that, perhaps somewhat unexpectedly, resolution can strictly beat black-only pebbling, and in particular that the space lower bounds on pebbling formulas in [Ben-Sasson and Nordstrom 2008] are tight. Second, we present a versatile parametrized graph family with essentially the same properties for black and black-white pebbling, which gives sharp simultaneous trade-offs for black and black-white pebbling for various parameter settings. Both of our contributions have been instrumental in obtaining the time-space trade-off results for resolution-based proof systems in [Ben-Sasson and Nordstrom 2009].