Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus
Alexander Alexandrovich Razborov, Avi Wigderson, Andrew Chi-Chih Yao · 1997
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 1's in some column. Our primary motivation is that this models regular resolution proofs of the pigeonhole principle PHP m 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