TR99-022 Authors: Eli Ben-Sasson, Avi Wigderson

Publication: 16th June 1999 12:07

Downloads: 2950

Keywords:

The width of a Resolution proof is defined to be the maximal number of

literals in any clause of the proof. In this paper we relate proof width

to proof length (=size), in both general Resolution, and its tree-like

variant. The following consequences of these relations reveal width as a

crucial ``resource'' of Resolution proofs.

In one direction, the relations allow us to give simple, unified proofs

for almost all known exponential lower bounds on size of resolution

proofs, as well as several interesting new ones. They all follow from

width lower bounds, and we show how these follow from natural expansion

property of clauses of the input tautology.

In the other direction, the width-size relations naturally suggest a

simple dynamic programming procedure for automated theorem proving - one

which simply searches for small width proofs. This relation guarantees

that the running time (and thus the size of the produced proof) is at most

quasi-polynomial in the smallest tree-like proof. The new algorithm is

never much worse than any of the recursive automated provers (such as DLL)

used in practice. In contrast, we present a family of tautologies on which

it is exponentially faster.