# Theory Seminar: Refuting Random 3-CNFs Using Polynomials Requires Large Proof Space

- Speaker:
- Nicola Galesi (Sapienza - University of Rome)
- Date:
- Wednesday, 7.6.2017, 12:30
- Place:
- Taub 201

To prove space lower bounds for refuting random k-CNF formulas in the UNSAT region we use the expansion property of the incidence graph of the formula, which guarantees large matchings. In Polynomial Calculus (PC), a proof system working with polynomials, simple matchings are no longer sufficient to obtain good space bounds and we need to guarantee large bi-matchings (or V-matchings).

Nevertheless, for 3-CNFs even bi-matchings are not longer sufficient.

After an overview of a framework to prove prove space lower bounds in PC, I will present a variant of (one side of) Hall's theorem stating that in bipartite graphs G=(L, R) with left-degree at most 3, L can be covered by certain families of disjoint paths (VW-matchings), provided that L expands in R by a factor of (2 − ε), for ε<1/5. With this tool in hand we can capture the space lower bound for the case random 3-CNFs in PC.