Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Theory Seminar: Refuting Random 3-CNFs Using Polynomials Requires Large Proof Space
event speaker icon
Nicola Galesi (Sapienza - University of Rome)
event date icon
Wednesday, 07.06.2017, 12:30
event location icon
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.