Criticality of Regular Formulas

We define the criticality of a boolean function f : {0,1}^n -> {0,1} as the minimum real number lambda >= 1 such that Pr [DT_{depth}(f|R_p) >= t] <= (p lambda)^t for all p in [0,1] and t in N, where R_p is the p-random restriction and DT_{depth} is decision-tree depth. Criticality is a useful parameter: it implies an O(2^((1- 1/(2 lambda))n)) bound on the decision-tree size of f, as well as a 2^{-Omega(k/lambda)} bound on Fourier weight of f on coefficients of size >= k. In an unpublished manuscript [Rossmann, 2018], the author showed that a combination of Håstad’s switching and multi-switching lemmas [Håstad, 1986; Håstad, 2014] implies that AC^0 circuits of depth d+1 and size s have criticality at most O(log s)^d. In the present paper, we establish a stronger O(1/d log s)^d bound for regular formulas: the class of AC^0 formulas in which all gates at any given depth have the same fan-in. This result is based on (i) a novel switching lemma for bounded size (unbounded width) DNF formulas, and (ii) an extension of (i) which analyzes a canonical decision tree associated with an entire depth-d formula. As corollaries of our criticality bound, we obtain an improved #SAT algorithm and tight Linial-Mansour-Nisan Theorem for regular formulas, strengthening previous results for AC^0 circuits due to Impagliazzo, Matthews, Paturi [Impagliazzo et al., 2012] and Tal [Tal, 2017]. As a further corollary, we increase from o(log n /(log log n)) to o(log n) the number of quantifier alternations for which the QBF-SAT (quantified boolean formula satisfiability) algorithm of Santhanam and Williams [Santhanam and Williams, 2014] beats exhaustive search.