迈向 Resolution 中空间与长度的最优分离
计算复杂性
2009-09-29 v1 计算机科学中的逻辑
摘要
当今大多数最先进的可满足性算法都是增广了子句学习的 DPLL 过程的变体。对于此类算法，除了明显的时间瓶颈外，主要的瓶颈在于内存使用量。在证明复杂性领域，时间和内存资源分别对应于 Resolution 证明的长度和空间。长期以来一直有研究试图理解这些证明复杂性度量，虽然关于长度已证明了强有力的结果，但我们对空间的理解仍然相当匮乏。例如，一个公式能在短长度内被证明是否意味着它也能在小空间内被证明，或者相反，这些度量是否无关，即短证明在空间方面可以是任意复杂的，这一问题仍然悬而未决。在本文中，我们提供了一些证据表明后者才是正确答案。为此，我们证明了大小为 n 的金字塔图上的所谓 Pebbling 矛盾所需空间的紧界为 Theta(sqrt(n))。这产生了第一个不依赖于宽度（Resolution 中另一个被广泛研究的度量）相应下界的空间多项式下界，并将 (Nordstrom 2006) 中空间与宽度的弱分离从对数级改进为多项式级。此外，延续 (Ben-Sasson 2002) 发起的关于不同证明复杂性度量之间权衡的研究路线，我们给出了 (Hertel and Pitassi 2007) 中近期长度 - 空间权衡结果的简化证明，并展示了如何利用我们的思想证明 Resolution 中的其他几个指数级权衡。
引用
@article{arxiv.0803.0661,
title = {Towards an Optimal Separation of Space and Length in Resolution},
author = {Jakob Nordström and Johan Håstad},
journal= {arXiv preprint arXiv:0803.0661},
year = {2009}
}