### Short proofs are narrow—resolution made simpleShort proofs are narrow—resolution made simple

Access Restriction
Subscribed

 Author Ben-Sasson, Eli ♦ Wigderson, Avi Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2001 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Abstract The $\textit{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 runnuing time (and thus the size of the produced proof) is at most quasi-polynomial in the smallest tree-like proof. This 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. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2001-03-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 48 Issue Number 2 Page Count 21 Starting Page 149 Ending Page 169

#### Open content in new tab

Source: ACM Digital Library