Short propositional refutations for dense random 3CNF formulas

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Ω(n^1.5−ε)$\mathrm{\Omega }(n^{1.5-\epsilon })$ clauses (Chvátal and Szemerédi 14], Ben-Sasson and Wigderson 10]). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Ω(n²/log?n)$\mathrm{\Omega }(n^2/\log ?n)$ clauses, shown by Beame et al. 6]. In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are TC⁰${\mathit{T}\mathit{C}}^0$ formulas (i.e., TC⁰${\mathit{T}\mathit{C}}^0$-Frege proofs) for random 3CNF formulas with n   variables and Ω(n^1.4)$\mathrm{\Omega }(n^{1.4})$ clauses.