Nicola Galesi: Space Lower Bounds in Algebraic Proof Systems

The study of space measure in Proof Complexity has a gained in the last years more and more importance: first it is clearly of theoretical importance in the study of complexity of proofs; second it is connected with SAT solving, since it might provide theoretical explanations of efficiency or inefficiency of specific Theorem Provers or SAT-solvers; finally in certain cases (like the calculus of Resolution) it is connected with important characterizations studied in Finite Model Theory, thus providing a solid link between the two research fields.

In the talk I will present a recent work, joint with Ilario Bonacina, where we devise a new general combinatorial framework for proving space lower bounds in algebraic proof systems like Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR). A simple case of our method allows us to obtain all the currently known space lower bounds for PC/PCR (CT_n, PHP^m_n, BIT PHP^m_n, XOR-PHP^m_n).

Our method can be view as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution. This can be seen as a first step towards a precise characterization of the space for algebraic systems in terms of combinatorial games, like Ehrenfeucht-Fraisse, which are used in Finite Model Theory.

More importantly, using our approach in its full potentiality, we answer to the open problem of proving space lower bounds in Polynomial Calculus and Polynomials Calculus with Resolution for the polynomial encoding of randomly chosen k-CNF formulas. Our result holds for k >= 4. Then in PC and in PCR refuting a random k-CNF over n variables requires high space measure of the order of Omega(n). Our method also applies to the Graph-PHP^m_n, which is a PHP^m_n defined over a constant (left) degree bipartite expander graph.

In the talk I will discuss a number of open problems which arise form our works which might be solved generalizing our approach.

The speaker was invited by Jakob Nordström.