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^{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 to finish one row of queries before asking queries about another row (the row model) or put the dual column restriction (the column model).
展开▼
