Random small logn CNF formulas are hard for shallow modular logic proofs
Random ($\log{n}$)-CNF Formulas Are Hard for Depth-$2$ Frege with Modular Gates
Computational Complexity
Summary
The paper shows that certain random logical formulas with a small logarithmic number of variables per clause are very difficult to prove false using specific limited logical systems called depth-2 modular logic proofs. The authors prove that to refute these formulas requires very complex algebraic manipulations, indicating these formulas are hard for such logical systems. They also find that this difficulty level is almost as high as it can be with this approach, meaning that stronger proof techniques or different formulas are needed for further progress.
What this means in practice
- •For logic circuit designers: Identify limitations of shallow modular logic layers to efficiently prove unsatisfiability of complex formulas, informing circuit depth needed for verification tasks.
- •For automated theorem proving teams: Understand inherent complexity barriers for refuting certain random formulas with depth-2 modular proof systems, guiding development of stronger proof methods.
A theory result. No direct application yet.
Authors
Jonas Conneryd
Abstract
We prove that, with high probability, refuting a random $k$-CNF formula on $n$ variables with ${M = n2^{k}}$ clauses for $ω_n(1) \leq k \leq O(\log{n})$ requires polynomial calculus degree at least ${n/2-O(n/\sqrt{k})}$ over every field. Through Pang's recent tradeoff between $\mathsf{AC}^0[p]$-Frege size and polynomial calculus degree [Pang 2026, arXiv:2610.00837v2], this implies a size lower bound of $\exp(Ω_p(\sqrt{k} \log{n}))$ for depth-$2$ $\mathsf{AC}^0[p]$-Frege. In this range of $k$, the bound is superpolynomial in $M$ while $M \leq \mathrm{poly}(n)$. We also prove a nearly matching degree upper bound of $n/2-n\ln(k)/{2k} +O(n/k)$, which shows that other formula families are needed to obtain lower bounds for full $\mathsf{AC}^0[p]$-Frege through Pang's tradeoff.