On Resolution with Clauses of Bounded Size
Zvi Galil · SIAM Journal on Computing · 1977
Several procedures based on (not necessarily regular) resolution for checking whether a formula in CF3 is contradictory are considered. The procedures use various methods of bounding the size of the clauses which are generated. The following results are obtained: 1. All of the proposed procedures which are forced to run in polynomial time do not always work—i.e., they do not identify all contradictory formulas. 2. Those which always work must run in exponential time. The exponential lower bounds for these procedures do not follow directly from Tseitin’s lower bound for regular resolution since these procedures also allow nonregular resolution trees.