Read-Once Branching Programs,
Rectangular Proofs of the Pigeonhole Principle and the
Transversal Calculus |
| |
Authors: | Alexander Razborov Avi Wigderson? Andrew Yao? |
| |
Institution: | (1) Steklov Mathematical Institute, 117966 Moscow, Russia;(2) Institute of Computer Science, Hebrew University, Jerusalem, Israel;(3) Computer Science Department, Princeton University, Princeton, New Jersey 08544, USA |
| |
Abstract: | We investigate read-once branching programs for the
following search problem: given a Boolean
m × n matrix with m > n, nd either an all-zero row, or two
1s in some column. Our primary motivation is that this models
regular resolution proofs of the pigeonhole principle
, 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
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
actually give rise to
proofs in this calculus and, inspired by this fact, also give a
remarkably simple rectangular reformulation of the
Haken–Buss–Turán lower bound for the case m
n
2. 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.* 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. 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. This work was supported in part by National
Science Foundation and DARPA under grant CCR-9627819, and by
USA-Israel BSF grant 92-00106. |
| |
Keywords: | 03F20 68Q17 |
本文献已被 SpringerLink 等数据库收录! |
|