关于Pebbling与Resolution的相对强度

过去十年中，在证明复杂性背景下，对pebble游戏的兴趣重新兴起。在比较不同子系统的强度、证明空间的下界以及建立大小-空间权衡时，Pebbling已被证明是研究基于resolution的证明系统的有用工具。典型的方法是将图上进行的pebble游戏编码为CNF公式，然后论证该公式的证明必须继承底层图的pebbling性质（的各个方面）。不幸的是，这里使用的归约并不紧致。为了用pebbling模拟resolution证明，需要非确定性黑白pebbling的全部强度，而resolution仅已知能模拟确定性黑pebbling。因此，为了获得强结果，需要找到特定的图族，这些图族要么对黑pebbling和黑白pebbling具有本质上相同的性质（这在一般情况下完全不成立），要么允许在resolution中模拟黑白pebbling。本文对这两种方法都有贡献。首先，我们设计了一种可以在resolution中模拟的受限形式的黑白pebbling，并表明存在一些图族，对于这些图族，这种受限pebbling可以渐近地优于黑pebbling。这证明了，或许有些出乎意料，resolution可以严格优于纯黑pebbling，并且特别地，[Ben-Sasson and Nordstrom 2008]中关于pebbling公式的空间下界是紧的。其次，我们提出了一个通用的参数化图族，它对黑pebbling和黑白pebbling具有本质上相同的性质，从而为各种参数设置下的黑pebbling和黑白pebbling提供了尖锐的同时权衡。我们的两个贡献对于在[Ben-Sasson and Nordstrom 2009]中获得基于resolution的证明系统的时间-空间权衡结果都起到了关键作用。