Random (log n)-CNF Are Hard for Cutting Planes (Again)

The random Δ-CNF model is one of the most important distribution over Δ-SAT instances. It is closely connected to various areas of computer science, statistical physics, and is a benchmark for satisfiability algorithms. Fleming, Pankratov, Pitassi, and Robere and independently Hrubeš and Pudlák showed that when Δ = Θ(logn), any Cutting Planes proof for random Δ-CNF on n variables requires size 2n / n in the regime where the number of clauses guarantees that the formula is unsatisfiable with high probability. In this paper we show tight lower bound 2Ω(n) on size -proofs for random (logn)-CNF formulas. Moreover, our proof is much simpler and self-contained in contrast with previous results based on Jukna’s lower bound for monotone circuits.