A relativized hierarchy of conjunctive normal forms is introduced, recognizable and SAT decidable in polynomial time. The corresponding hardness parameter, the first level of inclusion in the hierarchy, is studied in detail, admitting several characterizations, e.g., using pebble games, the space complexity of (relativized) tree-like resolution or nested input resolution, ... more >>>

Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that any arbitrary OBDD Apply refutation of the pigeonhole formula has an exponential size: we prove that the size of one ... more >>>