Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs
Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs
复制标题
了解分辨率中的空间：最佳下界和指数权衡
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Jakob Nordström
中科院分区：
文献类型：
--
作者：
Eli Ben;Jakob Nordström
对于目前基于DPLL过程和子句学习的可满足性算法，两个主要瓶颈是所使用的时间和存储量。因此，理解时间和记忆消耗，以及它们之间的关系，是一个具有相当实际意义的问题。在证明复杂性领域，这些资源对应于合取范式（CNF）公式归结证明的长度和空间。已经有一个长期的研究调查这些证明复杂性的措施，但虽然强有力的结果已经建立了长度，我们的理解空间，以及它如何与长度仍然相当差。特别是，分辨率证明是否可以同时针对长度和空间进行优化，或者这两种措施之间是否存在权衡，这个问题基本上仍然是开放的，除了在非常有限的设置中受到各种技术限制的一些结果之外。在本文中，我们纠正这种情况，证明了主机的长度空间权衡结果的决议在一个完全一般的设置。我们的trade-offs集合覆盖了从常数到O（n/loglogn）的整个区间的空间，其中大多数是超多项式甚至指数的。我们的关键技术贡献是以下，有点令人惊讶的，定理：任何CNF formulaF可以通过简单的替代转化为一个新的公式F 0，这样，如果F有正确的性质，F 0可以证明在基本上相同的长度为F，而F 0所需的最小空间是下界的变量数同时提到的任何证明forF。将这个定理应用于有向无圈图上的pebble博弈中定义的pebbling公式，然后利用pebbling文献中的已知结果以及证明了几个新的结果，得到了我们的分解折衷定理.
For current state-of-the-art satisfiability algorithms ba sed on the DPLL procedure and clause learning, the two main bottlenecks are the amounts of time and memory used. Understanding time and memory consumption, and how they are related to one another, is therefore a question of considerable practical importance. In the field of proof complexity, thes e resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There has been a long line of research investigating these proof complexity measures, but while strong results have been established for length, our understanding of space and how it relates to length has remained quite poor. In particular, the question whether resolution proofs can be optimized for length and space simultaneously, or whether there are trade-offs between these two measures, has remained essentially open apart from a few results in very limited settings suffering from various technical r estrictions. In this paper, we remedy this situation by proving a host of length-space trade-off results for resolution in a completely general setting. Our collection of tr ade-offs cover space ranging over the whole interval from constant to O(n/loglogn), and most of them are superpolynomial or even exponential. Our key technical contribution is the following, somewhat surprising, theorem: Any CNF formulaF can be transformed by simple substitution into a new formula F 0 such that if F has the right properties, F 0 can be proven in essentially the same length as F while the minimal space needed for F 0 is lowerbounded by the number of variables mentioned simultaneously in any proof forF . Applying this theorem to so-called pebbling formulas defined in terms of pebble gam es on directed acyclic graphs, and then using known results from the pebbling literature as well as a proving a couple of new ones, we obtain our resolution trade-off theorems.