eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-08-23
56:1
56:13
10.4230/LIPIcs.ICALP.2016.56
article
Total Space in Resolution Is at Least Width Squared
Bonacina, Ilario
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol055-icalp2016/LIPIcs.ICALP.2016.56/LIPIcs.ICALP.2016.56.pdf
Resolution
width
total space