On a generalization of extended resolution ?
Motivated by improved SAT algorithms ((O. Kullmann, DIMACS Series, vol. 35, Amer. Math. Soc., Providence, RI, 1997; O. Kullmann, Theoret. Comput. Sci. (1999); O. Kullmann, Inform. Comput., submitted); yielding new worst-case upper bounds) a natural parameterized generalization GER of Extended Resolution (ER) is introduced. ER can simulate polynomially GER, but GER allows special cases for which exponential lower bounds can be proven.
extended resolution lower bounds propositional logic blocked clauses generalized extended resolution