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