PhD in Computer Science

Space Lower Bounds in Algebraic Proof Systems

Academic year 2013/2014

Sommario del corso

• Course objectives
• Notes
• Teaching tools

Course objectives

Abstract:

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, 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 and PCR.  

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-Frassè , 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 Expander Graph PigeonHole Principle, which is a PigeonHole Principle 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.

It is a joint work with Ilario Bonacina, appeared in the Proceedings of Innovations in Theoretical Computer Science 2013.

Class schedule

Note

The seminar will be held by

Nicola Galesi

Sapienza University - Rome

• Teaching materials
• Exams and finals
• Go to Moodle
• Visit the forums