归结中空间与长度的最佳分离
Towards an Optimal Separation of Space and Length in Resolution
摘要：
当今最先进的可满足性算法是DPLL过程的变体，增加了子句学习。这种算法的主要瓶颈，除了明显的时间之外，是所使用的内存量。在证明复杂性领域，时间和内存资源对应于归结证明的长度和空间。有一个长期的研究试图理解这些证明复杂性的措施，但虽然强有力的结果已被证明的长度，我们对空间的理解仍然相当差。例如，一个公式在短长度内可证明的事实是否意味着它在小空间内也是可证明的，或者相反，这些度量是否在短证明可以相对于空间任意复杂的意义上是无关的，这仍然是一个悬而未决的问题。在本文中，我们提出了一些证据，真正的答案应该是，后者的情况下举行。我们通过证明Theta（sqrt（n））在大小为n的金字塔图上所谓的卵石矛盾所需的空间上的紧界来做到这一点。这产生了第一个多项式空间下界，它不是对应的宽度下界的结果，这是另一个研究得很好的分辨率度量，也是对Nordstrom 2006中空间和宽度从对数到多项式的弱分离的改进。此外，继续（Ben-Sasson 2002）发起的研究路线，在不同的证明复杂性度量之间进行权衡，我们提出了一个简化的证明（Hertel和Pitassi 2007）中最近的长度-空间权衡结果，并展示了我们的想法如何可以用来证明分辨率的其他指数权衡。
英文摘要：
Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, but while strong results have been proven on length our understanding of space is still quite poor. For instance, it remains open whether the fact that a formula is provable in short length implies that it is also provable in small space or whether on the contrary these measures are unrelated in the sense that short proofs can be arbitrarily complex with respect to space. In this paper, we present some evidence that the true answer should be that the latter case holds. We do this by proving a tight bound of Theta(sqrt(n)) on the space needed for so-called pebbling contradictions over pyramid graphs of size n. This yields the first polynomial lower bound on space that is not a consequence of a corresponding lower bound on width, another well-studied measure in resolution, as well as an improvement of the weak separation in (Nordstrom 2006) of space and width from logarithmic to polynomial. Also, continuing the line of research initiated by (Ben-Sasson 2002) into trade-offs between different proof complexity measures, we present a simplified proof of the recent length-space trade-off result in (Hertel and Pitassi 2007), and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
