ECCC-Report TR16-057https://eccc.weizmann.ac.il/report/2016/057Comments and Revisions published for TR16-057en-usTue, 12 Apr 2016 20:49:39 +0300
Paper TR16-057
| Total space in Resolution is at least width squared |
Ilario Bonacina
https://eccc.weizmann.ac.il/report/2016/057Given 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)$.
Tue, 12 Apr 2016 20:49:39 +0300https://eccc.weizmann.ac.il/report/2016/057