An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

TL;DR

This paper establishes that any OBDD-based proof of the pigeonhole principle requires exponential size, extending previous results to all OBDD refutations and highlighting inherent complexity.

Contribution

It proves that all OBDD refutations of the pigeonhole formula have exponential size, generalizing prior specific case results.

Findings

Any OBDD refutation has size at least (1.025^n)

Intermediate OBDDs in the refutation are exponentially large

Supports exponential lower bounds for OBDD-based proof systems

Abstract

Haken proved that every resolution refutation of the pigeonhole formula has at least exponential size. Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size. Here we show that any arbitrary OBDD refutation of the pigeonhole formula has an exponential size, too: we prove that the size of one of the intermediate OBDDs is at least $\Omega(1.025^n)$.