Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR16-057 | 11th April 2016 10:22

Total space in Resolution is at least width squared

RSS-Feed




TR16-057
Authors: Ilario Bonacina
Publication: 12th April 2016 20:49
Downloads: 1647
Keywords: 


Abstract:

Given an unsatisfiable $k$-CNF formula $\phi$ we consider two complexity measures in Resolution: width and total space. The width is the minimal $W$ such that there exists a Resolution refutation of $\phi$ with clauses of at most $W$ literals. The total space is the minimal size $T$ of a memory used to write down a Resolution refutation of $\phi$, where the size of the memory is measured as the total number of literals it can contain. We prove that $T=\Omega((W-k)^2)$.



ISSN 1433-8092 | Imprint