Name
Abstract | ||
|---|---|---|
We introduce a new way to measure the space needed in resolution refutations of CNF formulas in propositional logic. With the former definition (1994, B. H. Kleine and T. Lettman, "Aussangenlogik: Deduktion und Algorithmen, Teubner, Stuttgart) 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 us 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 relationships to the size of the refutation. We also give upper and lower bounds on the space needed for the resolution of unsatisfiable formulas. We show that Tseitin formulas associated to a certain kind of expander graphs of n nodes need resolution space n-c for some constant c. Measured on the number of clauses, this result is the best possible. We also show that the formulas expressing the general pigeonhole principle with n holes and more than n pigeons need space n+1 independent of the number of pigeons. Since a matching space upper bound of n+1 for these formulas exists, the obtained bound is exact. We also point to a possible connection between resolution space and resolution width, another measure for the complexity of resolution refutations. 2001 Elsevier Science. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1006/inco.2001.2921 | Symposium on Theoretical Aspects of Computer Science |
Keywords | Field | DocType |
resolution refutation,unsatisfiable formula,resolution space n-c,resolution,pebble game,resolution space,matching space,space n,space bounds,space bound,new definition,resolution proof,linear space,resolution graph,upper and lower bounds,propositional logic | Discrete mathematics,Combinatorics,Upper and lower bounds,Satisfiability,Linear space,Propositional calculus,Binary tree,Conjunctive normal form,Ranging,Resolution (logic),Mathematics | Journal |
Volume | Issue | ISSN |
171 | 1 | Information and Computation |
ISBN | Citations | PageRank |
3-540-65691-X | 58 | 1.94 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Juan Luis Esteban | 1 | 209 | 11.27 |
| Jacobo Torán | 2 | 564 | 49.26 |
| JL Esteban | 3 | 58 | 1.94 |