The Taub Faculty of Computer Science Events and Talks

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.