Space in algebraic proof systems
Sep 13, 2016 17th Italian Conference on Theoretical Computer Science (ICTCS), Lecce – Best Italian PhD Thesis in TCS 2016
We consider logical proof systems from the point of view of their space complexity, in particular we focus on the following two: Resolution (RES), a well studied proof system that is at the core of state-of-the-art algorithms to solve SAT instances; Polynomial Calculus (PC), a proof system that uses polynomials to refute contradictions. Informally speaking, the space of a proof measures the size of an auxiliary memory that a verifier needs to check the correctness of the proof. For Polynomial Calculus the space measure counts the number of distinct monomials to be kept in memory (monomial space). For Resolution the measure refers to the number of clauses to be kept in memory (clause space) or to the total number of symbols (total space). We introduce abstract frameworks to prove monomial space lower bounds in PC and total space lower bound in RES. We then exemplify such frameworks proving new (asymptotically) optimal lower bounds both for monomial space and total space. We prove that every Polynomial Calculus refutation of a random k-CNF F, for k > 2, in n variables requires, with high probability, \Omega(n) distinct monomials to be kept simultaneously in memory.
Previous talks on this theme were given in:
May 25, 2015 Institute of Mathematics, Prague – Logic Seminar
Apr 24, 2015 Dagstuhl Seminar 15171 – Theory and Practice of SAT Solving
Apr 08, 2015 KTH Royal Institute of Technology – Complexity Seminar
Apr 07, 2015 KTH Royal Institute of Technology – Complexity Seminar
May 19, 2014 Aarhus University – Complexity Seminar
Sep 10, 2013 14th Italian Conference on Theoretical Computer Science (ICTCS), Palermo
Jun 30, 2013 CSEDays. Theory 2013, Ekaterinburg – Summer School
Jan 13, 2013 4th Innovations in Theoretical Computer Science (ITCS), Berkeley
Sep 27, 2012 Limits of Theorem Proving, Rome – Workshop
This series of talks is based on:
- Bonacina, I. 2015. Space in weak propositional proof systems. Sapienza University of Rome.
- Bonacina, I. and Galesi, N. 2013. Pseudo-partitions, transversality and locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems. 4th Conf. Innov. Theor. Comput. Sci. – ITCS (2013), 455–472.
- Bonacina, I. and Galesi, N. 2015. A Framework for Space Complexity in Algebraic Proof Systems. J. ACM. 62, 3 (Jun. 2015), 1–20.
- Bennett, P., Bonacina, I., Galesi, N., Huynh, T., Molloy, M. and Wollan, P. 2017. Space proof complexity for random 3-CNFs. Information and Computation. 255, (2017), 165–176.