All Talks ⇦

Total space in resolution

Feb 06, 2017 Universidad Politecnica de CatalunyaALBCOM 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, TorontoWorkshop 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.PetersburgSpecial Semester on Complexity Theory
May 19, 2016 Steklov Institute of Mathematics, St.PetersburgProof Complexity Workshop
Oct 20, 2014 55th Annual Symposium on Foundations of Computer Science (FOCS), Philadelphia
Oct 16, 2014 Dagstuhl Seminar 14421Optimal algorithms and proofs
Jul 13, 2014 Vienna Summer of Logic, WienWorkshop on proof complexity
Feb 07, 2014 KTH Royal Institute of Technology, Stockholm – Complexity Seminar

This series of talks is based on: