Space bounds for resolution. (English) Zbl 0924.03020
Meinel, Christoph (ed.) et al., STACS 99. 16th annual symposium on Theoretical aspects of computer science, Trier, Germany, March 4–6, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1563, 551-560 (1999).
Summary: We introduce a new way to measure the space needed in a resolution refutation of a CNF formula in propositional logic. With the former definition [H. Kleine Büning and T. Lettmann, Aussagenlogik: Deduktion und Algorithmen (1994; Zbl 0809.03003)] the space required for the resolution of any unsatisfiable formula in CNF is linear in the number of clauses. The new definition allows a much finer analysis of the space in the refutation, ranging from constant to linear space. Moreover, the new definition allows to relate the space needed in a resolution proof of a formula to other well studied complexity measures. It coincides with the complexity of a pebble game in the resolution graphs of a formula, and as we show, has strong relationships to the size of the refutation. We also give upper and lower bounds on the space needed for the resolution of unsatisfiable formulas.
For the entire collection see [Zbl 0909.00052].
For the entire collection see [Zbl 0909.00052].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03B05 | Classical propositional logic |
| 03D15 | Complexity of computation (including implicit computational complexity) |
| 68Q25 | Analysis of algorithms and problem complexity |
