Lower Bounds Against Sparse Symmetric Functions of ACC Circuits: Expanding the Reach of #SAT Algorithms
share
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 Quasi-NP = NTIME[n^(log n)^O(1)] and NEXP do not have small circuits from various circuit classes C, by showing that 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 C. Say a symmetric Boolean function f(x_1,...,x_n) is sparse if it outputs 1 on O(1) values of ∑_i x_i. We show that for every sparse f, and for all "typical" C, faster #SAT algorithms for C circuits actually imply lower bounds against the circuit class f ∘ C, which may be stronger than C itself. In particular: #SAT algorithms for n^k-size C-circuits running in 2^n/n^k time (for all k) imply NEXP does not have f ∘ C-circuits of polynomial size. #SAT algorithms for 2^n^ϵ-size C-circuits running in 2^n-n^ϵ time (for some ϵ > 0) imply Quasi-NP does not have f ∘ C-circuits of polynomial size. Applying #SAT algorithms from the literature, one immediate corollary of our results is that Quasi-NP does not have EMAJ∘ACC^0 ∘THR circuits of polynomial size, where EMAJ is the "exact majority" function, improving previous lower bounds against ACC^0 [Williams JACM'14] and ACC^0 ∘THR [Williams STOC'14], [Murray-Williams STOC'18]. This is the first nontrivial lower bound against such a circuit class.
READ FULL TEXT