Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus
Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus
复制标题
只读一次分支程序、鸽巢原理和横向微积分的矩形证明
DOI：
10.1145/258533.258673
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
A. Yao
中科院分区：
文献类型：
--
作者：
A. Razborov;A. Wigderson;A. Yao
我们研究了只读分支程序的以下搜索问题：给定一个布尔m × n矩阵，m> n，找到一个全零行，或者在某列中有两个1。我们的主要动机是，这个模型的鸽子洞原则PHP n的定期决议证明，并为m> n 2没有下限是已知的长度，这样的证明。我们证明指数下界（对于任意大的m!）如果我们通过要求分支程序在询问关于另一行的查询之前完成一行查询（行模型）或设置双列限制（列模型）来进一步限制该模型。然后，我们调查一类特殊的解决方案证明PHP n操作的正条款的矩形形状，我们称之为这个片段的矩形演算。我们发现，所有已知的上限的大小的分辨率证明PHP n实际上引起证明在这个演算，并受到这一事实的启发，也给了一个非常简单的"矩形" reformula Steklov数学研究所，117966，莫斯科，俄罗斯。部分工作是这样做的，而笔者是访问特殊的一年逻辑和算法在DIMACS，普林斯顿。还得到俄罗斯基础研究基金会资助96 - 01 - 01222。耶路撒冷希伯来大学计算机科学研究所。这项工作的一部分是在高级研究所和普林斯顿大学的休假期间完成的。这项工作得到了美国-以色列BSF资助92 - 00106和以色列科学院管理的沃尔夫森研究奖以及斯隆基金会资助的支持。普林斯顿大学计算机科学系，普林斯顿，新泽西08544，美国。这项工作得到了美国国家科学基金会和DARPA的资助，资助号为CCR 9627819，美国-以色列BSF资助号为92 - 00106。的Haken-Buss-Turan下界的情况下m n。最后，我们表明，矩形演算是等价的列模型的一个方面，另一方面，横向演算，后者是一个自然的证明系统，估计从下面的横向大小的集合家庭。特别是，我们的指数下限列模型转换为矩形和横向结石。
We investigate read-once branching programs for the following search problem: given a Boolean m × n matrix with m > n, find either an all-zero row, or two 1’s in some column. Our primary motivation is that this models regular resolution proofs of the pigeonhole principle PHP n , and that for m > n 2 no lower bounds are known for the length of such proofs. We prove exponential lower bounds (for arbitrarily large m!) if we further restrict this model by requiring the branching program either to finish one row of queries before asking queries about another row (the row model) or put the dual column restriction (the column model). Then we investigate a special class of resolution proofs for PHP n that operate with positive clauses of rectangular shape; we call this fragment the rectangular calculus. We show that all known upper bounds on the size of resolution proofs of PHP n actually give rise to proofs in this calculus and, inspired by this fact, also give a remarkably simple “rectangular” reformula∗Steklov Mathematical Institute, 117966, Moscow, Russia. Part of the work was done while this author was visiting Special Year on Logic and Algorithms at DIMACS, Princeton. Also supported by Russian Basic Research Foundation grant 96-01-01222. †Institute of Computer Science, The Hebrew University, Jerusalem, Israel. Part of this work was done while on sabbatical leave at the Institute for Advanced Study and Princeton University, Princeton. This work was supported by USA-Israel BSF grant 92-00106 and by a Wolfson research award administered by the Israeli Academy of Sciences, as well as a Sloan Foundation grant. ‡Computer Science Department, Princeton University, Princeton, New Jersey 08544, USA. This work was supported in part by National Science Foundation and DARPA under grant CCR9627819, and by USA-Israel BSF grant 92-00106. tion of the Haken-Buss-Turan lower bound for the case m n. Finally we show that the rectangular calculus is equivalent to the column model on the one hand, and to transversal calculus on the other hand, where the latter is a natural proof system for estimating from below the transversal size of set families. In particular, our exponential lower bound for the column model translates both to the rectangular and transversal calculi.