slideshow 3

Logic seminar

Space proof complexity of random 3CNFs

Ilario Bonacina
Sapienza University of Rome

 

Monday, 25. May 2015 - 13:30
IM, rear building, ground floor
We prove that Resolution refutations of random 3CNFs in n variables and O(n) clauses require, with high probability, Ω(n) clauses each of width Ω(n) to be kept at the same time in memory. In Polynomial Calculus with Resolution refutations of a random 3-CNF in n variables and O(n) clauses require, with high probability, Ω(n) distinct monomials to be kept simultaneously in memory. For k > 3 such results were proven in joint works with N. Galesi and N. Thapen. The case k = 3 requires some additional work but essentially rely on a purely graph theoretic result: a variant of Hall’s Lemma. We show that in bipartite graphs G with bipartition (L,R) and left-degree at most 3, L can be covered by certain families of disjoint paths, called VW-matchings, provided that L expands in R by a factor of (2 − ε), for small enough ε. Talk based on a joint work with P. Bennet, N. Galesi, T. Huynh, M. Molloy, P. Wollan.