How deep must Boolean circuits be, in order to compute explicit functions? A simple counting argument shows that, with high probability, a random function f : {0, 1} n → {0, 1} requires circuit depth at least Ω(n), for circuits over any bounded fan-in basis. However, finding 10:2
Towards Stronger Depth Lower Bounds specific (interesting) functions that require high depth is a major open problem. For example, it is open whether there are functions computable with a circuit family of size s(n) that require circuits of ω(log s(n)) depth: this is essentially equivalent to the famous P vs NC 1 question which asks whether every polynomial-time problem can be simulated in parallel in only O(log n) depth. 1 Focusing on the natural case of the DeMorgan basis, where the gates of our circuits are ANDs and ORs of fan-in two with NOTs for free, it is only known that there is a function computable in P that requires circuits of depth (3 -o( 1)) log 2 n. This lower bound was established thirty years ago by Håstad in FOCS 1993 (following earlier work), with some low-order improvements since then [3,27,40,23,47]. (For more general bases, e.g., where all functions g : {0, 1} 2 → {0, 1} are allowed as gates, only a (2 -o( 1)) log 2 n depth lower bound is known [39].) There has been a stream of recent work, motivated by a compelling conjecture of Karcher-Raz-Wigderson [32], working towards stronger depth lower bounds via communication complexity [19,22,18,36]. For example, a recent work of Dinur and Meir [19] recovers a (3 -o( 1)) log 2 n depth lower bound for Andreev's function using communication complexity techniques. Mihajlin and Sofronova [36] use communication complexity methods to show (for instance) that a modified version of Andreev's function [3] requires 3.15 log 2 (n) depth when the top 0.29 log 2 (n) layers are AND gates. 2 Note. All logarithms in this paper will be in base two. From here on, we shall drop the subscript 2 in our logarithms.
In this paper, we provide two rather different lines of attack on the notorious problem of finding functions with a provable (3 + α) log n depth lower bound, for some α > 0. We first give a plausible "algorithmic method" approach for the non-uniform case, showing how faster algorithms for solving #SAT on subcubic-size DeMorgan formulas would imply supercubic-size DeMorgan formula lower bounds (thus implying a (3 + α) log n depth lower bound as well) 3 , and we present unconditional depth lower bounds against uniform circuits attempting to solve the SAT problem, based on an extension of "indirect diagonalization" arguments to formulas.
Over the last decade, many connections have been shown between non-trivial algorithms for analyzing small circuits, and the task of constructing non-trivial functions that do not have small non-uniform circuits (e.g., [42,25,57,58,53,16,38,29,13] for a sample). The setting most relevant to us is that of subcubic-size DeMorgan formulas. Explicit lower bounds against them have been known for decades [46,3,27,40,23] by "shrinkage arguments", in which one sets variables to the formula in a careful way, and argues that the formula must "shrink" drastically in size from a relatively small number of variable 10:3 settings. Analogues of these shrinkage arguments have been applied to derive faster algorithms for the Formula Satisfiability (Formula-SAT) problem and its counting version #Formula-SAT [42,16,15,17,48]. For example, it is known that, for ε > 0: [17] there is a #SAT algorithm running in 2 n-n ε/1.63 time on n 2.63-ε -size formulas, and [48] there is a #SAT algorithm running in 2 n-n ε time on formulas of n 3-16ε size. In the case of "slightly superquadratic" formulas of size n 2.001 (for example), the above results imply #SAT algorithms running in 2 n-n 0.385 time and 2 n-n 0.06 time, respectively. Our first main result is that a seemingly minor-looking improvement on the running time of #SAT algorithms for "slightly superquadratic" formulas would already yield a non-trivial function with a supercubic DeMorgan formula lower bound.
▶ Theorem 1.1 (#SAT For "Small" Formulas Implies "Large" Formula Lower Bounds). There is a universal constant k > 0 such that, for every ε ∈ (0, 1), if #SAT for n 2+2ε+o (1) size formulas can be solved in 2 n-n 1-ε log k n time (even in zero-error randomized time), then there is a function in E NP = TIME [2 O(n) ] SAT that does not have n 3+ε size formulas.
In fact, the desired #SAT algorithm only has to succeed against DeMorgan formulas which are the conjunction of n 1-ε+o (1) subformulas, where each subformula has O(n 1+3ε ) size. It looks quite plausible that such a #SAT algorithm may be derivable from known methods: it is already known that such formulas are significantly more limited than general n 2+2ε+o (1) -size formulas [33,36], and current algorithms [17] can solve #SAT on n 1+3ε -size formulas in time O(2 n-n 1-1.8ε ), for small ε > 0.
The proof of Theorem 1.1 proceeds by first showing that the #SAT algorithmic hypothesis in fact implies a "non-trivial derandomization" for large, n 3+ε -size formulas: for any desired constant β > 0, there is an algorithm running in 2 n /n ω (1) time which can distinguish unsatisfiable n 3+ε -size formulas from those with at least β • 2 n satisfying assignments (a.k.a., a Gap-SAT algorithm, see Section 3 for a definition). Our reduction from Gap-SAT on "large" formulas to #SAT on "small" formulas works by applying approximating polynomials for DeMorgan formulas to a significant portion of the given "large" formula, in such a way that the counting of SAT assignments implicitly performs a portion of the large formula evaluation for us, allowing us to distinguish between the unsatisfiable and "highly satisfiable" cases. From there, we carefully adapt known strong connections between Gap-SAT algorithms for circuits and circuit lower bounds [14], to show an "ultra-fine-grained" connection: a non-trivial Gap-SAT algorithm for formulas of size O(s(n)) implies size-s(n) formula lower bounds. That is, the difference between the size handled by the Gap-SAT algorithm and the size lower bound is only constant factor.
Along the way to Theorem 1.1, the connection proved between Gap-SAT algorithms and circuit lower bounds is rather general: any non-trivial Gap-SAT algorithm for a size-O(s(n)) circuit class C such that (a) C can compute PARITY in size s(n), (b) C is closed under the OR of 3 copies of C, and (c) C is closed under negations of their outputs, and projections (0-1 assignments to some of the variables, and negations to some of the variables), implies size-s(n) lower bounds against C. Two other natural examples of such C are n 2+ε -size formulas over the full binary basis, and O(n)-size circuits over any complete basis.
We use this connection to conclude some new unconditional circuit lower bounds. Kabanets, Koroth, Lu, Myrisiotis, and Oliveira [29] studied the class Formula[s] • G of Boolean functions computed by size-s DeMorgan formulas where the leaves may be any Boolean I T C S 2 0 2 4 10:4
Towards Stronger Depth Lower Bounds functions from a class G. They showed that when the functions in G have low communication complexity, one can give interesting #SAT algorithms and pseudorandom generators for Formula[n 2-ε ] • G, and consequently also lower bounds (where ε > 0 denotes an arbitrarily small constant). Using our connection, we can prove lower bounds on Formula[n 2-ε ] • G for classes G that do not have low communication complexity. The general statement is:
For every ε > 0 and every class of functions G such that:
G is closed under variable projections, Formula[n 2-ε ] • G contains PARITY, and the acceptance probability of a conjunction of O(n) functions from G, over n variables, can be additively approximated to within
Applying Theorem 1.2 and prior work, we can conclude lower bounds against DeMorgan formulas composed with low-degree F 2 -polynomials.
Note that such circuits require 2 Ω(n ε ) bits to describe, to encode the polynomials.
A line of work initiated by Fortnow [20,21,49] proved model-independent time-space lower bounds (or equivalently, lower bounds against small-space algorithms) for SAT and related problems within the polynomial-time hierarchy. This approach was extended by Williams [54,55,56] into a framework which culminated in a proof that SAT does not have an n o(1) -space algorithm running in time n 2 cos(π/7) ≃ n 1.801 . (Buss and Williams [10] later proved that the 2 cos(π/7) exponent is optimal for this framework.)
An interesting feature of this line of work is that the proofs are highly algorithmic: one assumes SAT has a sufficiently efficient algorithm, and applies that algorithm in various ways until a contradiction to a known lower bound (by diagonalization) is reached. This type of reasoning is sometimes called "indirect diagonalization"; many other examples of such lower bounds can be found in the literature (e.g., [31,2,50,49,37]).
Here, we develop an indirect diagonalization method for lower bounds against uniform O(log n)-depth circuits (and equivalently, O(log n)-depth formulas). We establish supercubic depth lower bounds on solving SAT with uniform circuits over the NAND basis, where every gate computes the function
There are no internal negations; only input variables can be negated. It is well-known that the NAND basis is universal (every Boolean function can be computed with a NAND circuit), and it is surprisingly expressive. For example, it is known that every boolean function on n variables has NAND formulas of depth n + O(log * n) [35], nearly matching the n + O(1) depth in DeMorgan's basis. Furthermore, the hard example function for DeMorgan formulas, Andreev's function, has NAND formulas of depth (3 + o(1)) log n (and therefore has NAND formulas of size n 3+o (1) ), matching the lower bound for the DeMorgan basis up to low-order terms [23]. (See the appendix of the full version [5] for a construction of low-depth formulas for Andreev's function.) Therefore, one cannot use Andreev's function to prove a significantly stronger depth lower bound for NAND formulas, and the lower bound proved in this work have deeper implications than a weak expressiveness of NAND formulas.
Here, our main result is that SAT requires supercubic depth for uniform circuits composed of NAND gates: ▶ Theorem 1.4. For every c < 4 cos(π/7) ≃ 3.603, SAT does not have uniform NAND formulas of depth (c -o(1)) log n.
Our notion of uniformity can be defined as follows.
▶ Definition 1.5 ("Input-aware" polylog-time uniform formulas). A family of formulas (φ n ) n≥1 of depth (c + o(1)) log n is polylog-time uniform if there exists a RAM machine A φ such that for every n, every x ∈ {0, 1} n and every b ∈ {0, 1} ≤(c+o(1)) log n , A φ (x, b, n) outputs a description of the gate at position b in φ n in time log O (1) n.
Here, for a bitstring b of length at most (c + o(1)) log n, the "gate at position b" in φ n is the gate reached by iterating over all bits of b, starting from the root, moving to the left child of the current gate when reading a 0, and to its right child otherwise. We will see the need for this stronger definition in Section 4.2, where we need to give O(log n) bits of information from the input to the descriptor to dynamically select a subformula.
Observe that this is a more general notion than (say) PLOGTIME-uniformity, which is common in the literature [52], hence the lower bounds that we give against this model also hold for PLOGTIME-uniform formulas.
Under the hood, indirect diagonalization results often provide an unconditional method for simulating weak algorithms super-efficiently, using more powerful models. For example, all proofs that SAT cannot be solved in n 1+δ time and poly log(n) space, for various δ > 0, exploit the fact that algorithms using small space can be quickly simulated by algorithms that use a small number of alternations [12] (a generalization of nondeterminism). Theorem 1.4 is obtained from constructing an extremely efficient method for evaluating a uniform NAND formula, with an algorithm using a small number of alternations. This evaluation method is combined with other ideas from previous indirect diagonalization lower bounds (in particular, results on "alternation-trading proofs" [56,10]) to obtain the result.
Organization of the Rest of the Paper. Section 2 covers some preliminaries. Section 3 proves that faster #SAT algorithms for superquadratic-size formulas would imply supercubicsize lower bounds, along with an "ultra-fine-grained" connection from Gap-SAT algorithms to circuit lower bounds. Section 4 proves SAT lower bounds against NAND circuits of depth 3.6 log n. Section 5 concludes with a discussion of further work.
We first recall some basic notions in circuit complexity that are relevant for the paper. Later in the preliminaries, we discuss some notions particular to the paper.
A Boolean formula ϕ over n inputs is a rooted full binary tree 4 whose internal nodes, called gates, are labeled by a function f : {0, 1} 2 → {0, 1}, and leaves are labeled with either a variable x i , its negation ¬x i for some i, 1 ≤ i ≤ n, or a constant c ∈ {0, 1}. The depth of a formula is the depth of the underlying tree. A formula is read-once if each of its input 4 Full means that every node has either zero or two children.
Towards Stronger Depth Lower Bounds variables appears on at most one leaf. Given an input x ∈ {0, 1} n , the value of ϕ at x can be defined as the value of its root on input x, where the value of a gate is defined inductively as follows:
x i if g is labeled with the variable x i ¬x i if g is labeled with ¬x i f (ϕ(g 1 ), ϕ(g 2 )) if g is labeled f , and g 1 , g 2 are the children of g Throughout this paper, we are concerned with formulas over the DeMorgan basis of functions f : {0, 1} 2 → {0, 1}, including all 2-input Boolean functions except the XOR and EQUALS function. It is not hard to show that this is equivalent to considering formulas over AND/OR/NOT, with NOT gates considered to be "free" (zero cost in size and depth).
In the half of this work on SAT lower bounds (4), we focus on NAND formulas, that is, whose gates are all labeled with the function NAND : x, y → ¬(x ∧ y). DeMorgan's law implies that NAND(x, y) = ¬x ∨ ¬y, therefore NAND formulas are equivalent to "alternating OR/AND" formulas (up to negations of some inputs) where all gates of even depth are ORs, and odd-depth gates are ANDs (and the root is said to have depth 0). This "alternating" point of view will be useful when describing procedures to compute the value of a formula.
A formula family is a sequence {ϕ n } n∈N of formulas such that for every n, ϕ n is a formula on n inputs x 1 , . . . , x n . A language L ⊆ {0, 1} * is computed byfoot_0 the formula family {ϕ n } n∈N if for every n and every
Since a separate formula is allowed for each input length, there are formula families of constant size and depth computing undecidable languages.
The depth complexity of a function f : {0, 1} ⋆ → {0, 1} is the function d : N → N such that d(n) is the minimum depth of any formula computing f n , the restriction of f to n-bit inputs. Observe that the notion does not change when we replace "formula" with "circuit": any circuit of depth d can be simulated by a formula of depth d and size O(2 d ). For this reason, formula size lower bounds imply depth complexity lower bounds, but the converse does not necessarily hold.
In the half of this paper on SAT lower bounds (Section 4), we restrict our attention to uniform formulas: formula families such that the description of the n-input formula can be computed efficiently. We recall here the notion of uniformity, stated in the introduction, that we use.
Finally, for any c ≥ 0, we define NDepth [c log n] to be the class of languages that have uniform polylog-time NAND formulas of depth(c + o(1)) log n. Observe that uniform logdepth NAND formulas can be efficiently simulated by random-access machines, due to the negligible runtime overhead of the description: for every c > 1, we have 10:7 (1) , where TISP n c , n o (1) denotes the class of languages solvable by an algorithm (in a standard random-access model) running in n c+o (1) time and n o (1) space.
Along with the above notation for NAND formula complexity classes, in Section 4 it will be extremely convenient to use quantifier notation to express alternating complexity classes, that define a fined-grained version of the polynomial hierarchy, just as was used in prior work on alternation-trading proofs [55,56,10,37]).
Given a complexity class C (defined by some machine model) and constants k, (a i ) i≤k , we consider the alternating complexity class (Q
Computation in an alternating complexity class is defined as follows: A k and a C machine M such that, given an input x of length n: for every i ≤ k, A i takes as input x i along with y i , a string of n ai+o (1) nondeterministic bits, runs in time n ai+o (1) and outputs a string x i of length at most n ai+o (1) , with the convention that x 0 := x. The output of the last stage, x k , is passed to the machine M .
The computation accepts x starting from stage i if either:
, and there exists a y i such that the computation accepts x i starting from stage i + 1, Q i is ∀, and for every y i , the computation accepts x i starting from stage i + 1.
x is in L if the computation x accepts starting from stage 1.
Counting SAT Assignments to "Small" Formulas Implies Lower Bounds for "Large" Formulas
In this section, we prove the following theorem:
▶ Reminder of Theorem 1.1. There is a universal constant k > 0 such that, for every ε ∈ (0, 1), if #SAT for n 2+2ε size formulas can be solved in 2 n-n 1-ε log k n time (even in randomized zero-error time), then there is a function in
The proof is broken into two parts. First, in Section 3.1, we show that the #SAT hypothesis of Theorem 1.1 implies that the following promise problem can be solved in 2 n /n ω (1) time, for all constants β > 0.
Problem: Gap-Formula-SAT with gap β ∈ (0, 1) Input: A DeMorgan formula F on n inputs, with n 3+ε size. Promise: Either F is unsatisfiable, or at least β • 2 n of its 2 n assignments are satisfying. Decide: which is the case.
Second, in Section 3.2, we show that the resulting algorithm for Gap-Formula-SAT for all constant β > 0 implies the circuit lower bound, building on prior work [57,7,14].
Towards Stronger Depth Lower Bounds
In this section, we prove the following lemma:
There is a universal constant k > 0 such that, for every ε ∈ (0, 1), if #SAT for n 2+2ε+o (1) -size formulas can be solved in 2 n-n 1-ε log k n time, then for any β ∈ (0, 1), the Gap-Formula-Sat problem with gap β on DeMorgan formulas of n inputs and size n 3+ε can be solved in 2 n /n ω (1) time.
Our Gap-Formula-SAT requires a couple of ingredients. First, we will use the following fundamental result for approximating DeMorgan formulas with low-degree polynomials, which built on a long line of prior work.
▶ Theorem 3.2 (Reichardt [41], Kabanets-Koroth-Lu-Myrisiotis-Oliveira [30]). For every positive integer s and α ∈ (0, 1/2), and for every DeMorgan formula F of size s, there is a polynomial
Furthermore, given the description of F , a description of a P F with the above property and degree O(
The proof of Reichardt only shows the existence of such a polynomial P F , and does not consider the cost of constructing it. Kabanets-Koroth-Lu-Myrisiotis-Oliveira [30] credit an anonymous reviewer with an algorithm for constructing the polynomial P F ; see their paper for details.
The second ingredient we need (which incidentally, is also used in the algorithm of Theorem 3.2) is the following decomposition result for formulas: ▶ Theorem 3.3 (Impaglizzo-Meka-Zuckerman [26], Tal [47]). There is a polynomial-time algorithm that, given a formula F of size S and a parameter K ∈ [S], outputs a read-once formula
We now turn to proving Lemma 3.1. Suppose we are given a formula F of size n 3+ε , and we are promised that F is either unsatisfiable, or has at least β2 n satisfying assignments. We want to determine which is the case, using a #SAT algorithm for formulas of only n 2+2ε+o (1) size.
First, we apply Theorem 3.3 with
Second, we compute an approximating polynomial P F ′ of degree O(n 1-ε log n • log(1/α)) for the polynomial F ′ , with error α ∈ (0, 1). (For now, let us leave α as a parameter.) By Theorem 3.2, such a P F ′ can be computed in 2 Õ(n 1-ε log(1/α)) time, and has T := 2 Õ(n 1-ε log(1/α)) terms.
Over the boolean hypercube, the polynomial P F ′ can be naturally written as a sum of T conjunctions on t = O(n 2-2ε ) variables each, where each conjunction has width O(n 1-ε log n log(1/α)). Composing P F ′ with the subformulas G 1 , . . . , G t , our n 3+ε -size formula F is close (in the sense of Theorem 3.2) to an expression of the generic form:
That is, S(x) is a sum of T = 2 Õ(n 1-ε log(1/α)) terms, where each term is a conjunction of t = O(n 1-ε log n log(1/α)) formulas, each formula has O(n 1+3ε ) size, and each coefficient c
Now, suppose we have an algorithm that can solve #SAT for formulas of size n 2+2ε+o(1) in time O(2 n /T 2 ) ≤ 2 n-n 1-ε log(1/α) log k n , for a sufficiently large constant k > 0. Then, as every summand of S(x), i.e. each expression of the form
has size Õ(n 2+2ε ) ≤ n 2+2ε+o (1) , we can compute the sum a S(a) over all inputs, which has the form (1) .
Finally, we observe that computing a S(a) is enough to determine Gap-Formula-SAT, for an appropriate choice of the parameters α and β.
Suppose
Suppose F has at least β • 2 n SAT assignments. Then, every SAT assignment to F adds at least 1 -α to the sum, while each UNSAT assignment subtracts no more than α from the sum, in the worst case. So in this case,
Provided that (1 -α)β -α(1 -β) > α, we can distinguish between the two cases using the value a S(a). Manipulating the inequality, we find:
Thus for any gap parameter β ∈ (0, 1), the above inequality holds for α := β/3. (We could even let β := 1/2 n o (1) , for example.)
This concludes the proof of Lemma 3.1.
We remark that the above approach is easily generalizable. Letting t ≪ n be a parameter, every formula of size n 3+ε can be converted into a sum of the form
Note that such a transformation is only meaningful for t ≪ n: otherwise, the running time of converting the formula into S(x) already exceeds 2 n . The above argument shows that if we can solve #SAT on formulas of O(n 3+ε /t) size (in fact, a conjunction of O(t) formulas of n 3+ε /t 2 size), in time 2 n-Ω(t/(log n) 2 ) , then we obtain a nontrivial Gap-Formula-SAT algorithm.
Discussion: What Can Current Formula-SAT Algorithms Achieve?
Before moving on, let us briefly comment on how known #SAT algorithms based on shrinkage behave, and speculate on whether they can be generalized to achieve the kind of running time / formula size tradeoff that we seek.
Roughly speaking, all state-of-the-art algorithms work in the following way. First, they solve #SAT on all O(n/ log 2 n)-size formulas by brute force, building a 2 o(n) -size look-up table for them. Next, they apply a concentration version of a shrinkage lemma to show that, by setting all possible assignments to some n -k variables, a formula of size s shrinks to size approximately k 2 • s/n 2 , on all but 2 n-Ω(k) assignments. When k 2 • s/n 2 < O(n/ log 2 n), the algorithm can consult the lookup table in the shrunken case, which means we need
to use the lookup table efficiently, and obtain 2 n-Ω(k) time. In summary, one might expect to obtain 2 n-Ω(k) time for solving #SAT on formulas of size n 3 /(k 2 log 2 n), for the relevant values of k.
However, for our desired running time in the hypothesis of Theorem 1.1, we require k > n 1-ε . In that case, the algorithm will only work for size
In principle, this is not necessarily a major issue: recall that we only need to solve #SAT on formulas which are conjunctions of n 1-ε subformulas of size n 1+2ε . It appears plausible to us that a form of "simultaneous shrinkage", where we consider the shrinkage of n 1-ε subformulas of size n 1+2ε simultaneously under a common random restriction (analogous to "multi-switching" lemmas that work on a set of formulas [25,24]), could be applied to obtain the necessary #SAT algorithm.
Next, we show that the Gap-Formula-SAT algorithm derived in the previous subsection would be sufficient to establish the desired lower bound. Recall in the previous section, we showed that, under the #SAT algorithm hypothesis of Theorem 1.1, it follows that for every constant β ∈ (0, 1), we can solve Gap-Formula-SAT on formulas of size n 3+ε in time 2 n-Ω(n 1-ε ) , in that we can distinguish UNSAT formulas from those satisfied by at least a (1 -β)-fraction of possible assignments. Chen and Williams [14] show there is a universal constant β ⋆ > 0 such that, for any class of circuits C that is closed under taking negations of the output, and variable projections (negating inputs and/or replacing inputs by constants), if there is a Gap-SAT algorithm running in 2 n /n ω (1) time for polynomial-size circuits C which are the AND of three circuits from C, distinguishing UNSAT circuits from those with at least β ⋆ 2 n satisfying assignments, then NEXP does not have polynomial-size circuits from C.
Here, we will explain how to modify their argument, by combining other ideas from [57,7,14], to show that a faster Gap-Formula-SAT algorithm for formulas of size O(n 3+ε ) actually implies that there is a function in E NP = TIME[2 O(n) ] SAT which does not have formulas of size n 3+ε . The main difficulty is that we have to be very careful to "respect" the formula size in the argument, so that it does not ever increase by more than a constant factor. We achieve this by (yet) another level of indirection, using the hypothesis E NP has formulas of size n 3+ε in multiple ways. Indeed, we start by assuming that E NP does have formulas of size n 3+ε . We will eventually show that every unary language L ∈ NTIME[2 n ] (languages over the input alphabet {1}) can then be solved in nondeterministic time o(2 n ), contradicting the Nondeterministic Time Hierarchy Theorem (which holds for unary languages as well).
In the following, let k > 0 be a sufficiently large universal constant. First, we show (drawing from prior work) that a non-trivial Gap-Circuit-Sat algorithm for poly(n)-size circuits would imply our desired lower bound. Next, we will show that a Gap-Formula-Sat algorithm suffices for the lower bound, even if the algorithm only works on O(n 3+ε )-size formulas.
▶ Lemma 3.4 ([57, 7, 14]). If Gap-Circuit-Sat on circuits with n + k log n inputs and size O(n k • n 3+ε ) can be solved in 2 n /n ω (1) time, then E NP does not have DeMorgan formulas of size O(n 3+ε ). (In fact, circuit lower bounds would follow.)
] be an arbitrary unary language. Our goal is to show that a nontrivial Gap-Circuit-Sat algorithm, combined with small circuits for E NP , would allow us to nondeterministically decide L in o(2 n ) time, contradicting the Nondeterministic Time Hierarchy theorem [4].
Following prior work [57,7,14], we can choose a succinct PCP verifier V for L, with proofs of length 2 n • n k , randomness n + k log n, and for each choice of randomness, the verifier's q = O(1) queries can be computed by a fixed n k -size circuit C n which takes in the n + k log n bits of randomness as input, and outputs q strings of length n + k log n corresponding to the indices of the proof bits for each query, along with sign bits (whether the outcome of the query should be negated, or not). The verifier accepts on a given random string if and only if the OR of the q queries is true, and the n k -size circuit C n implementing the verifier can be constructed in poly(n k ) time.
If E NP has formulas of size n 3+ε , then for every n, if 1 n ∈ L, there exists a family of formulas F n of size n 3+ε on n + k log n inputs such that the 2 n • n k -bit truth table of F n encodes a PCP π that the PCP verifier V accepts with probability 1. Indeed, there exists a 2 O(n) -time algorithm with a SAT oracle (a.k.a. an E NP algorithm) that on input (1 n , i) outputs the i-th bit of such a proof π: this follows by a standard reduction from search-to-decision [57], augmented with exhaustive search over all random strings of length n + k log n to verify that the probability that V accepts π is 1.
We can simulate L on the input 1 n as follows. First, nondeterministically guess a formula F n of size n 3+ε that is intended to encode a PCP π n for the PCP verifier V on 1 n . Next, we construct a n k -size circuit C n with n + k log n input bits encoding the verifier's query computation. Supposing the verifier makes q = O(1) queries, we compose C n with q copies of the formula F n , and take the OR of the q copies of F n . More precisely, letting the q output strings of C n be C
(1) n (r), . . . , C (q) n (r) be subcircuits of C n such that C (i) n (r) prints the (n + k log n)-bit index of the i-th query on randomness r, and letting S (i) n (r) be the sign bit for the i-th query, we construct the circuit
This circuit C check has size at most O(n k • n 3+ε ), and C check (r) = 1 if and only if the verifier V on randomness r accepts with proof oracle F n .
Since V is a PCP, we have two properties: If 1 n ∈ L, then there is a choice of F n of n 3+ε size such that C check is true on all inputs r. (Note such F n exists, only assuming E NP has n 3+ε size formulas.) If 1 n / ∈ L, then for every choice of F n , C check is false on at least a 1 -β fraction of its possible inputs r, where β ∈ (0, 1) is determined by the soundness probability of the PCP protocol.
To line this up with our Gap-SAT formulation, we work with the negation of C check : either ¬C check is unsatisfiable, or ¬C check is satisfiable on at least a (1 -β)-fraction of its possible assignments.
So now we are faced with the following task: given a circuit C check with n + k log n inputs and O(n k • n 3+ε ) size, and we wish to distinguish whether C check is unsatisfiable on all possible inputs, or is satisfiable on at least a β-fraction. So far, everything is analogous to what one finds in earlier work showing how improving exhaustive search implies circuit lower bounds [57,7]. If we can solve this task in o(2 n ) time, we will contradict the Nondeterministic Time Hierarchy Theorem. ◀
Our goal now is to show that, if E NP has n 3+ε -size DeMorgan formulas, and Gap-Formula-Sat can be solved in 2 n /n ω (1) time on O(n 3+ε )-size formulas for arbitrary constant-sized gaps, then we actually obtain the Gap-Circuit-Sat algorithm needed in the previous part.
We will apply ideas similar to that of the proof of Theorem 5 of Chen and Williams [14], which shows how to prove super-polynomial C-circuit lower bounds for NEXP from a Gap-SAT algorithm for the conjunction (AND) of three C-circuits that distinguishes the case where C is UNSAT from the case where C has a non-zero constant fraction of SAT assignments. (The following exposition is not entirely self-contained, but it should be quite friendly to a reader who has [14] open at their proof of Theorem 5.)
We work with a polynomial-time linear constant-rate error-correcting code Enc : {0, 1} n → {0, 1} cn with a polynomial-time decoder Dec : {0, 1} cn → {0, 1} n , which can decode up to some relative distance δ ECC > 0 [44]. We use the ECC to modify the circuit C check we want to solve Gap-SAT for, so that if C check has a satisfying assignment, then the resulting circuit D has an assignment that is δ ECC -far from any of its satisfying assignments. More precisely, as in [14], we define a circuit
where Dec is the decoder for the aforementioned error-correcting code. Since Dec is a polynomial-time function, it has a circuit of size at most O(n k ) for large enough k, and the circuit D can be implemented in size at most O(n 2k ). ▷ Claim 3.5. Let x ∈ {0, 1} n and let y = Enc(x). Then:
If x is a satisfying assignment of C check , then y is δ ECC -far from any satisfying assignment of D. That is, one must flip more than a δ ECC -fraction of bits of y in order to obtain a satisfying assignment to D. If x is a non-satisfying assignment of C check , then y satisfies D.
Proof. Let x be such that C check (x) = 1, and let y = Enc(x). For any string z that has relative distance at most δ ECC from y, we have Dec(z) = x by the definition of an ECC with decoding distance δ ECC . Therefore we also have
It follows that y must be δ ECC -far from any z such that D(z) = 1.
For the second item, observe that D(y) = D(Enc(x)) = ¬C check (Dec(Enc(x))) = ¬C check (x). So if x does not satisfy C check , then y satisfies D. ◁
As in [14], we employ a PCP of Proximity (PCPP) for the Circuit-Eval problem [6]: given a circuit D on n inputs and y ∈ {0, 1} n , the Circuit-Eval problem asks whether D(y) = 1. The following lemma describes the important properties of this PCPP.
▶ Lemma 3.6 (3-query PCP of Proximity for Circuit Evaluation with perfect completeness [14, Lemma 24]). For any proximity parameter δ P CP ∈ (0, 1), there exists s ∈ (0, 1) such that there is a PCP of proximity system for Circuit-Eval with proximity δ P CP , soundness s, randomness r ≤ O(log n), and the following properties:
Given the r random coins, a polynomial-time verifier V computes the OR on three queried bits (with some bits possibly negated), accepting if and only if the OR is true. Given a pair (D, y) such that D is a circuit, y is an input of length n, and D(y) = 1, a proof π can be constructed in poly(|D| + |y|) time that makes the verifier V accept (D, y, π) with probability 1.
Given (D, y), if y is δ P CP -far from all satisfying assignments to D, then for all proofs π, the verifier V accepts (D, y, π) with probability at most s. In other words, the PCPP consists of an efficient verifier which is given a circuit D and input y, queries only three bits of the proof π, and tries to determine if D(y) = 1. If D(y) = 1 is true, then there is a proof π of this fact that always convinces the verifier, and can be efficiently constructed. If D(y) = 0 is false, and y is in fact far in Hamming distance from every SAT assignment to D, then the verifier will catch that D(y) ̸ = 1 with probability at least 1 -s, regardless of the proof π.
We apply this PCPP to the circuit D defined above, with input y = Enc(x), and show how we can combine it with the algorithm of Lemma 3.1 to decide Gap-SAT for C. The PCPP has randomness r ≤ O(log n), proximity parameter δ P CP > 0, and soundness s < 1, for fixed constants δ P CP and s. Letting V be the verifier for the PCPP, as we vary over the m := 2 r = poly(n) possible random strings, we obtain a set of 3-OR constraints on a given proof (y, π). Let H 1 , . . . , H m be the corresponding constraints. From the properties of the PCPP, we find:
If C check (x) = 0, then D(y) = 1, and there is a proof π such that all H i are satisfied by the pair (y, π).
If C check (x) = 1, then y is δ ECC -far from the set of all satisfying assignments to D. By setting δ P CP < δ ECC , at most an s fraction of the constraints {H i } are ever satisfied by (y, π).
In the case where C check is unsatisfiable, there is a proof π(x) for every y = Enc(x), such that the verifier V accepts (D, y, π(x)) with probability 1. For our setting, it is crucial that the proof function π(x) can be computed in E NP (so that it will also have n 3+ε -size DeMorgan formulas, by assumption).
To verify this, we go back to the original argument (before we began to invoke Chen and Williams [14]). Given an input (n, x, i) of length n + O(log n), where n is encoded in O(log n) bits, x is n + O(log n) bits, and i is O(log n) bits, here is an E NP procedure (an algorithm running in 2 O(n) time with a SAT oracle) for constructing a proof π(x) for the relevant circuit C check defined in (1): First, use a SAT oracle to construct the lexicographically first formula F n of size n 3+ε which is a witness for our original PCP verifier for L (if 1 n ∈ L, then F n exists). Then, build the circuit C check using F n , evaluate y = Enc(x), and construct the proof π(x) for (C check , x) in polynomial time (which can be done by the construction of the PCP of Proximity). Finally, output the i-th bit of the proof π(x).
Since this is an E NP procedure with input of length O(n), there is a formula of size O(n 3+ε ) that, given (x, i), outputs the i-th bit of π(x).
Following the notation of [14], we let T i be the O(n 3+ε )-size formula printing the i-th bit of π(x), and let T (x) be the concatenation of all T i (x). We let G i (x) be the constraint H i (an OR of 3 literals) evaluated on the pair (Enc(x), T (x)), and recall that there are only m = poly(n) constraints H 1 , . . . , H m . As our error-correcting code is linear, each bit of Enc(x) is a parity over some bits of x. Therefore, each G i is an OR of 3 formulas, some of which are parities over a subset of the bits of x, and some of which are copies of T j (x) for some j. Observe (crucially) that, since PARITY has O(n 2 )-size DeMorgan formulas, every formula G i in fact has size only O(n 3+ε ).
Finally, we compare the two cases when C check is UNSAT, and when C check has many satisfying assignments, and show that a non-trivial Gap-Formula-SAT algorithm for O(n 3+ε ) size is sufficient for distinguishing these cases.
When 1 n ∈ L and we've guessed the "good" formula F n of size O(n 3+ε ), the constructed circuit C check is UNSAT. In that case, as we argued above, there exists a polynomial-sized set of formulas {T i } that we can guess, each of size O(n 3+ε ), so that the verifier V always outputs 1, over all choices of randomness. Therefore for all i ∈ [m], every constraint formula G i (x) will be true, over all assignments x. It follows that, if we run a Gap-Formula-SAT algorithm on ¬G i for all i = 1, . . . , m, it will always return an "UNSAT" answer.
When 1 n / ∈ L, then no matter what formula F n we guess to construct C check with, the circuit C check will be satisfied by at least a (1 -β)-fraction of its possible assignments. Then, for all possible choices of the set of formulas {T i }, over all assignments x, and all i, at most a β + s fraction of pairs (x, i) are such that G i (x) is true. By averaging, there must be some i ⋆ such that G i ⋆ (x) has at most a β + s fraction of SAT assignments. Let β > 0 be sufficiently small, so that (1 -β -s) ≥ (1 -s)/2. Then, given a Gap-Formula-SAT algorithm that outputs "MANY-SAT" when at least a (1 -s)/2 > 0 fraction of assignments are satisfying, this algorithm will return "MANY-SAT" on at least one ¬G i .
Therefore, our Gap-Formula-SAT algorithm (which works for any constant fraction of SAT assignments) lets us determine whether or not 1 n is in L. After poly(n) bits of guessing, our nondeterministic algorithm for deciding L calls the Gap-Formula-SAT algorithm for poly(n) times, on formulas of size O(n 3+ε ). Therefore the entire nondeterministic procedure runs in only o(2 n ) time, assuming the Gap-Formula-SAT algorithm runs in 2 n /n ω (1) time. Thus we can decide L in NTIME[o(2 n )], contradicting the Nondeterministic Time Hierarchy Theorem. This completes the proof.
Finally, observe that, even if our Gap-Formula-SAT algorithm was zero-error randomized, this would still suffice for constructing a nondeterministic algorithm for L.
Let us summarize this subsection with the tight connection between algorithms and lower bounds that we have proved: ▶ Theorem 3.7. Let ε > 0. Suppose for every β > 0, there is a Gap-Formula-SAT algorithm for O(n 3+ε )-size formulas that runs in 2 n /n ω (1) time, and distinguishes unsatisfiable formulas from those with at least a β-fraction of satisfying assignments. Then E NP does not have O(n 3+ε )-size formulas.
It is easy to see that the proof of Theorem 3.7 can be generalized to other circuit classes, beyond just DeMorgan formulas. The properties we used of DeMorgan formulas are that they are: closed under negation of their output, closed under variable projections (replacing variables with constants or their negations), closed under the OR of three copies, and PARITY has subcubic-size DeMorgan formulas -below the size bound of our DeMorgan formulas. We can generalize the connection from Gap-Sat algorithms to lower bounds in a natural way, as follows. Recall that Formula[n 2-ε ] • G denotes the functions computable by DeMorgan formulas of size n 2-ε with functions from the class G at their leaves [29].
▶ Reminder of Theorem 1.2. For every ε > 0 and every class of functions G such that:
G is closed under variable projections, Formula[n 2-ε ] • G contains PARITY, and the acceptance probability of a conjunction of O(n) functions from G, over n variables, can be additively approximated to within 1/2 n 1-ε/3 in 2 n-Ω(n 1-ε/3 ) deterministic time,
We confine ourselves to a sketch of the proof of Theorem 1.2, as it closely mimics the proofs of previous subsections. First, in the proof of Lemma 3.1, we reduced the problem of computing Gap-SAT for a formula of size n 3+ε , to the problem of computing #SAT on a formula of size n 2-2ε . In particular, the reduction produced 2 Õ(n 1-ε log n) instances of #SAT on formulas which are conjunctions of Õ(n 1-ε ) formulas of O(n 1+3ε ) size. This was accomplished by first applying Theorem 3.3 to decompose the n 3+ε -size formula into an O(n 2-2ε )-size formula of O(n 1+3ε )-size formulas, then applying Theorem 3.2 to reduce the O(n 2-2ε )-size formula to a linear sum of 2 Õ(n 1-ε log n) conjunctions on Õ(n 1-ε ) variables.
Let C be a circuit from Formula[n 2-2ε ] • G. (For simplicity of exposition, we consider size n 2-2ε instead of n 2-ε , to more closely model the situation in Lemma 3.1.) Performing exactly the same steps as above on the n 2-2ε -sized formula part of C, we can reduce C to a sum of 2 Õ(n 1-ε log n) conjunctions of Õ(n 1-ε ) functions from G. By the same analysis as in Lemma 3.1, if we have a deterministic 2 n-Ω(n 1-2ε/3 ) -time algorithm for approximating the acceptance probability of a conjunction of functions from G to within a gap of 1/2 n 1-2ε/3 , then we can determine Gap-Sat for the circuit C in time (1) .
Next, assuming that G satisfies the hypotheses of Theorem 1.2, it follows that the circuit class Formula[n 2-ε ] • G is closed under negation of the output (because DeMorgan formulas are), closed under the OR of three copies (because DeMorgan formulas are), closed under variable projections (by assumption on G, and contains PARITY (by assumption). Therefore this class has all the closure properties necessary to apply the proof of Theorem 3.7 directly. Applying our algorithm for Gap-Sat on Formula[n 2-ε ]•G circuits (obtained in the previous paragraph), we can conclude that E NP does not have Formula[n 2-ε ] • G circuits.
Here is one example of a canonical class that has high communication complexity, yet we can still prove circuit lower bounds for it.
▶ Reminder of Corollary 1.3. For all ε > 0, E NP does not have Formula[n 2-ε ] • G circuits, where G is the class of n ε/3 -degree polynomials over F 2 .
Proof. Observe that Formula[n 2-ε ]•G contains PARITY (a degree-one F 2 -polynomial), and that G is closed under variable projections. It remains to show that the algorithmic hypothesis of Theorem 1.2 is satisfied: namely, that we can estimate the acceptance probability of conjunctions of functions from G in 2 n-Ω(n 1-ε/3 ) time.
Building on the randomized algorithm of Lokshtanov, Paturi, Tamaki, Williams, and Yu [34], Chan and Williams [11] show that the #SAT problem for systems of m degree-d F 2 -polynomials in n variables can be solved in deterministic 2 n-n/O(d) • poly(m) time. Their algorithm works for all d < o( √ n). Therefore we can set d = n ε/3 and get a #SAT algorithm running in 2 n-Ω(n 1-ε/3 ) time, satisfying the algorithmic hypothesis of Theorem 1.2. ◀
Let us remark that we could have also applied known pseudorandom generators for degree-d F 2 -polynomials to obtain a good Gap-Sat algorithm, but we would have obtained a weaker degree bound. Namely, the best-known seed length for a PRG fooling degree-d [51], so enumerating over all seeds would cost at least 2 Ω(2 d ) time.
Uniform Depth Lower Bounds for SAT
We now give an overview of how we implement "indirect diagonalization" to show that SAT does not have uniform NAND formulas of depth less than c log n, for a value of c > 3 that we will specify later. Recall (Section 2) that we define NDepth [c log n] to be the class of languages that have uniform polylog-time NAND formulas of depth (c + o( 1)) log n.
A central component of our proof technique is a construction that allows us to simulate NDepth [c log n] very efficiently, using alternating machines with a low number of alternations. Following [55,10], we call it a "Speedup Rule". roughly means that we can evaluate a NAND formula of depth d log n on an input X of length n by first existentially guessing n x/2+o (1) bits Y , then universally choosing n 1+o (1) bits Z, then evaluating a NAND formula of depth (d -x) log n on the input (X, Y, Z) (with some low-overhead computation). That is, NAND formulas of depth d log n can informally be simulated by "Σ 2 -type" NAND formulas of depth (d -x) log n, with n x/2+o (1) auxiliary bits of input.
To prove that SAT does not have NAND formulas of depth less than c log n, we start by assuming that SAT ∈ NDepth [c log n], and aim to reach a contradiction. As SAT is NP-complete under polylog-time computable first-order projections [21,49,28], this inclusion extends to every language in NTIME[n] with negligible overhead. Since NDepth [c log n] corresponds to NAND depth (c+o(1)) log n (and NDepth [c log n] is closed under complement), we have:
Using this property, we can derive another important ingredient in the lower bound, the so-called Slowdown Rule, which allows us to reduce the number of quantifiers in an alternating computation, at the cost of an increased NAND depth:
Let y denote the n x/2+o (1) bits received from the universal quantifier. Let us describe the procedure from the output gate (which is an OR). If the first bit of y is 0, the OR gate is replaced by its left child, otherwise it is replaced by its right child. In both cases, we reach an AND gate. We then apply this procedure recursively on the two OR gates below that AND gate, using the separately the two halves of the rest of y, until we reach depth x/2 log n. The resulting formula ϕ ′ starts with (x/2) log n levels of AND gates, followed by smaller alternating OR/AND formulas ϕ i of depth (d -x + o(1)) log n. Using the above observation, for a given x, there is a choice of y x such that ϕ ′ (x) = 1 if and only if ϕ(x) = 1. The ∃ stage outputs the input x and the corresponding string y x . Upon receiving (x, y), the ∀ stage universally guesses x 2 log n nondeterministic bits z that represent an index i, and outputs x and x log n bits that encode a path from the root of ϕ to the root of ϕ i . As ϕ ′ is the conjunction of the n x/2 formulas ϕ i , it evaluates to 1 on input x if and only if for every index i ≤ n x/2 , ϕ i (x) = 1.
Finally, recall that the definition of alternating computation requires that there exists a single machine M ′ that runs the final stage of computation for every possible choice of nondeterministic bits: that is, the machine cannot depend on the nondeterministic bits. This is where our strong notion of uniformity comes in (from Definition 1.5), where the descriptor machine has random access to the input: giving M ′ access to (a few) bits of the input, allows us to adapt its behavior depending on the nondeterministic bits. If M is a machine that describes ϕ, we define the machine M ′ , that on input a ′ of length n ′ = n + x log n for some n, sets a ′ = ab, where a has length n and b has length x log n, and returns M ′ (a ′ , i, n ′ ) = M (a, bi, n). We use the random access to move x log n bits from the input to the position of the gate that we want to describe. (1) , n o (1) .
A close inspection of the proof of Lemma 4.1 reveals that the ∀ quantifier here uses only d 2 log n nondeterministic bits. Therefore, we can use exhaustive search over the n d/2 strings of nondeterministic bits of length d 2 log n to remove this quantifier. For every such string, we perform a n o(1) -time computation, hence we get that NDepth (1) ].
The inclusion in coNTIME[n d/2+o (1) ] follows from the closure of NDepth [d log n] under complement.
◀
Next, we show that the assumption SAT ∈ NDepth [c log n] extends to every language in NP without significant overhead.
Later, this result will allow us to remove the quantifier from an alternating class, at the cost of an increased depth of the verifier.
A key idea for the proof of Lemma 4.5 is the fact that any language in NTIME[n] can be reduced to SAT via so-called uniform poly-log time first-order projections, where instances of size n can be mapped to formulas of size n 1+o (1) [21,49]. A first-order projection is a depth 0 circuit, i.e., each output bit is either a constant (0 or 1), an input x i , or its negation ¬x i . For an in-depth exposition of first-order projections, see for example [1,End of Sec. 3]. See the full version [5] for the proof of Lemma 4.5.
We need to be careful when applying the lemma to alternating classes 6 : the (i + 1)-th computation stage takes as input a string of length m = n ai , not n. Since the previous result only holds for NTIME[n d ] when d is at least 1, we need to take into account the edge case where the running time of the (i + 1)-th stage is sublinear in the size of its input. (This is the case below in the proof of Lemma 4.2.)
While the primary use of the Speedup Rule (Lemma 4.1) is to reduce the depth of the verifier at the cost of increasing the number of quantifiers, we show that we can combine it with the above lemma to efficiently remove quantifiers from an alternating NDepth computation. where Q ∈ {∃, ∀} and ¬Q is the opposite quantifier.
See the full version [5] for the proof.
We now prove the Conditional Depth hierarchy theorem, stated without proof in Section 4. ⊆ NTIME[n a+o (1) ].
6 See Definition 2.1 for the definition of alternating classes and of (a i ).
The first inclusion follows Lemma 4.5, whereas the second inclusion follows from the above argument, as 2c > 1. The last inclusion uses the efficient simulation of NDepth by (nondeterministic) RAMs. The proof for c < 1/2 is similar, except that the second inclusion follows from 2c < 1. We have proven NTIME[n 2a ] = NTIME[n a+o (1) ] for some a > 1, which contradicts the Nondeterministic Time Hierarchy Theorem. ◀
Note that this theorem relies heavily on the assumption that SAT ∈ NDepth [c log n], hence this theorem is conditional, but it is sufficient for our use case. To prove Theorem 1.4, it suffices to find a sequence of rules (called a proof ) to apply that results in a class inclusion that contradicts Theorem 4.3, using the assumption that SAT ∈ NDepth [c log n], for any c < 4 cos(π/7). See the full version [5] for a construction of such proofs.
Finally, we comment briefly on the potential optimality of our results (within known techniques). In the case of SAT vs small-space algorithms, Buss and Williams [10] proved that the result SAT / ∈ TISP n c , n o (1) for c < 2 cos(π/7) is optimal for the alternation-trading proofs framework. This was later extended and simplified by Mudigonda and Williams [37], who showed lower bounds against randomized and quantum classes. As far as we can tell, it appears that their generalization covers our framework as well, therefore we cannot prove SAT / ∈ NDepth [c log n] for c ≥ 4 cos(π/7) without finding a new (and improved) way to speed up NDepth computation using alternations.
In this paper, we have considered two rather disparate approaches to proving stronger depth lower bounds: one for the non-uniform setting, and another for the uniform case. Let us highlight a few interesting steps for further work.
The Non-Uniform Setting: Obviously the most pressing open problem is to design faster #SAT algorithms for DeMorgan formulas. Until now, researchers designing faster SAT algorithms for formulas and other weak classes have generally stated their time bounds in the form 2 n-n δ where δ > 0 is unspecified. Our work has shown that improving these δ factors, even for slightly-superquadratic formulas, would have interesting lower bound implications. Another open problem is to consider other forms of circuit-analysis algorithms, and understand their implications. It is surprising (to us) that #SAT for formulas can be so powerful. The main intuition is that, by using low-degree approximate polynomials for formulas, the act of counting SAT assignments actually performs a non-trivial amount of the formula evaluation itself. Are there other representations of formulas which can be similarly exploited?
The Uniform Setting: As mentioned in the introduction, the uniform lower bounds we have proved are "merely" depth lower bounds, which are weaker than size lower bounds, since the latter directly imply the former. However, Spira [45], Brent [9], and Bonet and Buss [8] have given a partial converse, that allows converting a cα log n depth lower bounds into an n c size lower bound, where α > 1 depends on the computational basis.
Unfortunately, for NAND formulas, the best known conversion theorems have α > 2, making them useless for our purposes. For most families of formulas, the current best
In what follows, we may use "L has formulas ..." for "L is computed by a formula family..."