The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Skip to content



Narrow proofs may be spacious: separating space and width in resolution

Nordstrom, J (Royal Institute of Technology, Stockholm)
Wednesday 12 April 2006, 10:30-11:00

Seminar Room 1, Newton Institute


The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously been studied and related to the refutation size of unsatisfiable CNF formulas. Also, the resolution refutation space of a formula has been proven to be at least as large as the refutation width, but it has remained unknown whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is non-constant, thus solving an open problem mentioned in several previous papers.


[pdf ]


MP3MP3 Real AudioReal Audio

Back to top ∧