Narrow Proofs May Be Spacious: Separating Space and Width in Resolution

Speaker: Jakob Nordström

Slides

Abstract:

Resolution is a proof system for proving tautologies in propositional logic. It works by showing that the negation of a tautology, encoded as a CNF formula, is unsatisfiable. There is only one derivation rule, namely that from the clauses C ∨ x and D ∨ ¬ x we can resolve on the variable x to derive the resolvent clause C ∨ D. A resolution proof refutes an unsatisfiable formula F by deriving the empty clause 0, i.e., the clause with no literals, from F.

Because of its simplicity, resolution is well adapted to proof search algorithms. Many real-world automated theorem provers are based on resolution. It is also perhaps the single most studied propositional proof system from a theoretical point of view in the area of proof complexity.

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is, intuitively, the maximal number of clauses one needs to keep in memory while verifying the proof. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable CNF formulas. Also, the refutation space of a formula has been proven to be at least as large as the refutation width, but it has been open 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 a problem mentioned in several previous papers.

Our result has been published as ECCC Report TR05-066, and an extended abstract appeared in STOC '06 (co-winner of Danny Lewin Best Student Paper Award).

The talk will be given in Swedish or English depending on the participants, and is intended to last for 2x45 minutes.