Total space in resolution
Feb 06, 2017 Universidad Politecnica de Catalunya – ALBCOM Seminar on Algorithms and Theory of Computation
In this series of talks we cover some results on the space complexity of Resolution and in particular a connection between total space and width. Given a k-CNF formula F, the width is the minimal integer W such that there exists a Resolution refutation of 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 F, where the size of the memory is measured as the total number of literals it can contain. We show that T=\Omega((W-k)^2). This connection between total space and width relies on some basic properties of another, perhaps less known, complexity measure in Resolution: the “asymmetric width”.
Previous talks on this theme were given in:
Aug 19, 2016 Fields Institute, Toronto – Workshop on Theoretical Foundations of SAT Solving
Jul 14, 2016 43rd International Colloquium on Automata, Languages and Programming (ICALP)
May 30, 2016 Steklov Institute of Mathematics, St.Petersburg – Special Semester on Complexity Theory
May 19, 2016 Steklov Institute of Mathematics, St.Petersburg – Proof Complexity Workshop
Oct 20, 2014 55th Annual Symposium on Foundations of Computer Science (FOCS), Philadelphia
Oct 16, 2014 Dagstuhl Seminar 14421 – Optimal algorithms and proofs
Jul 13, 2014 Vienna Summer of Logic, Wien – Workshop on proof complexity
Feb 07, 2014 KTH Royal Institute of Technology, Stockholm – Complexity Seminar
This series of talks is based on:
- Bonacina, I. 2016. Total Space in Resolution is at Least Width Squared. 43rd International Colloquium on Automata, Languages, and Programming – ICALP (2016), 56:1–56:13.
- Bonacina, I., Galesi, N. and Thapen, N. 2016. Total Space in Resolution. SIAM J. Comput. 45, 5 (Jan. 2016), 1894–1909.
- Bonacina, I., Galesi, N. and Thapen, N. 2014. Total Space in Resolution. 55th Annu. Symp. Found. Comput. Sci. – FOCS (Oct. 2014), 641–650.