We prove that for k ≪4n regular resolution requires length nΩ(k) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional nΩ(k) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.
We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF ? in n variables requires, with high probability, distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of ? requires, with high probability, clauses each of width to be kept at the same time in memory. This gives a lower bound for the total space needed in Resolution to refute ?.
© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma
