Bounded-Depth Frege Lower Bounds for Random 3-CNFs via Deterministic Restrictions
Svyatoslav Gryaznov, Navid Talebanfard
TL;DR
This work addresses the open problem of super-polynomial lower bounds for bounded-depth Frege proofs on random 3-CNFs with linear clause density. It introduces deterministic restrictions adapted to proof complexity through formula assignments and leverages weak boundary expanders to preserve hardness under restriction, culminating in a depth-$k$ Frege lower bound of Ω($n^{1+ε_k}$) steps for random 3-CNFs with ε_k = 2^{-Θ($k$)}. The key innovation is the Regularization Lemma, which combines live and forced subformulas with variable and formula assignments to obtain a restricted, width-controlled semantic refutation, yielding a contradiction with width lower bounds. The results mark the first non-trivial AC0-Frege lower bounds for random 3-CNFs and point to promising future directions, including extensions to AC0[$2$]-Frege and related systems via formula assignments and deterministic restrictions. This advances our understanding of proof complexity for random instances and supports broader conjectures about the hardness of random formulas under low-depth proof systems.
Abstract
A major open problem in proof complexity is to demonstrate that random 3-CNFs with a linear number of clauses require super-polynomial size refutations in bounded-depth Frege systems. We take the first step towards addressing this question by establishing a super-linear lower bound: for every $k$, there exists $ε_k > 0$ such that any depth-$k$ Frege refutation of a random $n$-variable 3-CNF with $Θ(n)$ clauses has $Ω(n^{1 + ε_k})$ steps w.h.p. Our proof involves a novel adaptation of the deterministic restriction technique introduced by Chaudhuri and Radhakrishnan (STOC'96). For a given formula, this technique provides a method to fix a small number of variables in a bottom-up manner, ensuring that every surviving gate has small fan-in. Consequently, the resulting formula depends on a limited number of variables and can be simplified to a constant by a small variable assignment. Adapting this approach to proof complexity requires addressing the usual challenges associated with maintaining the hardness of a given instance. To this end, we introduce the following generalizations of standard proof complexity tools: - Weak expanders: These bipartite graphs relax the classical notion of expansion by only requiring that small sets have a non-empty boundary, while intermediate-sized sets have a large boundary. This property is sufficient to preserve hardness (e.g., for resolution width) and is easier to maintain as we remove vertices from the graph. - Formula assignments: To simplify a Frege proof, we consider a generalization of partial restrictions that assign values to formulas instead of just variables. We treat these assignments as new axioms added to our formula, as they generally cannot be expressed as variable substitutions.