Oliver Kullmann

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

Olga Tveretina, Carsten Sinz, Hans Zantema

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