A fundamental problem in circuit complexity is to find explicit functions that require large depth to compute. When considering the natural DeMorgan basis of $\{\text{OR},\text{AND}\}$, where negations incur no cost, the best known depth lower bounds for an explicit function in NP have the form $(3-o(1))\log_2 n$, established by H{\aa}stad (building on others) in the early 1990s. We make progress on the problem of improving this factor of $3$, in two different ways:
- We consider an ``algorithmic method'' approach to proving stronger depth lower bounds for non-uniform circuits in the DeMorgan basis. We show that slightly faster algorithms (than what is known) for counting the number of satisfying assignments on \emph{subcubic}-size DeMorgan formulas would imply \emph{supercubic}-size DeMorgan formula lower bounds, implying that the depth must be at least $(3+\varepsilon)\log_2 n$ for some $\varepsilon > 0$. For example, if $\#$SAT on formulas of size $n^{2+2\varepsilon}$ can be solved in $2^{n - n^{1-\varepsilon}\log^k n}$ time for some $\varepsilon > 0$ and a sufficiently large constant $k$, then there is a function computable in $2^{O(n)}$ time with a SAT oracle which does not have $n^{3+\varepsilon}$-size formulas. In fact, the $\#$SAT algorithm only has to work on formulas that are a conjunction of $n^{1-\varepsilon}$ subformulas, each of which is $n^{1+3\varepsilon}$ size, in order to obtain the supercubic lower bound. As a proof of concept, we show that our new algorithms-to-lower-bounds connection can be applied to prove new lower bounds for ``hybrid'' DeMorgan formula models which compute interesting functions at their leaves.

- Turning to the ${ \text{NAND} }$ basis, we establish a greater-than-$(3 \log_2 n)$ depth lower bound against \emph{uniform} circuits solving the SAT problem, using an extension of the ``indirect diagonalization'' method for NAND formulas.
Note that circuits over the NAND basis are a special case of circuits over the DeMorgan basis; however, hard functions such as Andreev's function (known to require depth $(3-o(1))\log_2 n$ in the DeMorgan basis) can still be computed with NAND circuits of depth $(3+o(1))\log_2 n$. Our results imply that SAT requires polylogtime-uniform NAND circuits of depth at least $3.603 \log_2 n$.