We continue the program of proving circuit lower bounds via circuit satisfiability algorithms. So far, this program has yielded several concrete results, proving that functions in $\text{ Quasi-NP} = \text{ NTIME}[n^{ (\log n)^{ O(1)}}]$ and $\text{ NEXP}$ do not have small circuits from various circuit classes ${ \cal C}$, by showing that ${ \cal C}$ admits non-trivial satisfiability and/or $\#$SAT algorithms which beat exhaustive search by a minor amount. In this paper, we present a new strong lower bound consequence of non-trivial $\#$SAT algorithm for a circuit class ${ \mathcal C}$. Say a symmetric Boolean function $f(x_1,\ldots,x_n)$ is sparse if it outputs $1$ on $O(1)$ values of $\sum_i x_i$. We show that for every sparse $f$, and for all "typical" ${ \cal C}$, faster $\#$SAT algorithms for ${ \cal C}$ circuits actually imply lower bounds against the circuit class $f \circ { \cal C}$, which may be stronger than ${ \cal C}$ itself. In particular: $\#$SAT algorithms for $n^k$-size ${ \cal C}$-circuits running in $2^n/n^k$ time (for all $k$) imply $\text{ NEXP}$ does not have $f \circ { \cal C}$-circuits of polynomial size. $\#$SAT algorithms for $2^{ n^{ \epsilon}}$-size ${ \cal C}$-circuits running in $2^{ n-n^{ \epsilon}}$ time (for some $\epsilon > 0$) imply $\text{ Quasi-NP}$ does not have $f \circ { \cal C}$-circuits of polynomial size. Applying $\#$SAT algorithms from the literature, one immediate corollary of our results is that $\text{ Quasi-NP}$ does not have $\text{ EMAJ} \circ \text{ ACC}^0 \circ \text{ THR}$ circuits of polynomial size, where $\text{ EMAJ}$ is the "exact majority" function, improving previous lower bounds against $\text{ ACC}^0$ [Williams JACM'14] and $\text{ ACC}^0 \circ \text{ THR}$ [Williams STOC'14], [Murray-Williams STOC'18]. This is the first nontrivial lower bound against such a circuit class.

Categories: cs.CC

Lower Bounds Against Sparse Symmetric Functions of ACC Circuits: Expanding the Reach of $\#$SAT Algorithms