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 [Fle+22] and independently Hrubeš and Pudlák [HP17] showed that when Δ = Θ(log 𝑛), any Cutting Planes proof for random Δ-CNF on 𝑛 variables requires size 2 𝑛/polylog𝑛 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 Ω(𝑛) on size CP-proofs for random (log 𝑛)-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.