Space characterizations of complexity measures and size-space trade-offs in propositional proof systems
Space characterizations of complexity measures and size-space trade-offs in propositional proof systems
复制标题
命题证明系统中复杂性度量的空间特征和尺寸空间权衡
DOI：
--
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
A. Razborov
中科院分区：
文献类型：
--
作者：
Theodoros Papamakarios;A. Razborov
我们确定了两个新的证明复杂度度量的大集群，它们等价于多项式和log n个因子。除其他外，第一个聚类包含树状解析大小的对数、正则化（即乘以证明长度的对数）子句和单项空间，以及正则和树状解析中的普通和正则子句空间。因此，将子句或单项空间从树状分辨率大小的对数中分离出来，与显示子句或单项空间与证明长度之间的强烈权衡是一样的，也与显示子句空间与深度之间的超临界权衡是一样的。第二个集群包含宽度，Σ 2空间（子句空间到深度2 Frege系统的推广），普通和正则化，以及系统R中树状大小的对数（log）。作为其中一些模拟的应用，我们改进了已知的多项式微积分的大小空间权衡。在下界方面，我们展示了在子句空间4中可反驳的公式的树状分辨率大小的二次下界。在我们的方法中，我们引入了另一个介于深度和树状大小的对数之间的证明复杂性度量，这可能是独立的兴趣。
We identify two new big clusters of proof complexity measures equivalent up to polynomial and log n factors. The first cluster contains, among others, the logarithm of tree-like resolution size, regularized (that is, multiplied by the logarithm of proof length) clause and monomial space, and clause space, both ordinary and regularized, in regular and tree-like resolution. As a consequence, separating clause or monomial space from the (logarithm of) tree-like resolution size is the same as showing a strong trade-off between clause or monomial space and proof length, and is the same as showing a super-critical trade-off between clause space and depth. The second cluster contains width, Σ 2 space (a generalization of clause space to depth 2 Frege systems), both ordinary and regularized, as well as the logarithm of tree-like size in the system R (log). As an application of some of these simulations, we improve a known size-space trade-off for polynomial calculus with resolution. In terms of lower bounds, we show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4. We introduce on our way yet another proof complexity measure intermediate between depth and the logarithm of tree-like size that might be of independent interest.