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 ... 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 >>>