I. Introduction
Proving unconditional circuit lower bounds for explicit functions (with the ultimate goal of proving NP ⊄ P/ poly) is one of the holy grails of theoretical computer science. Back in the 1980s, there was a number of significant progress in proving circuit lower bounds for AC0 (constant depth circuits consisting of AND/OR gates of unbounded fan-in) [1], [2], [3], [4] and AC0[p] [5], [6] (AC0 circuits extended with MODp gates) for a prime p. But this quick development was then met with an obstacle—there were little progresses in understanding the power of AC0[m] for a composite m, despite it had been conjectured that they cannot even compute the majority function. In fact, it was a long-standing open question in computational complexity that whether NEXP (non-deterministic exponential time) has polynomial-size ACC0 circuits1, until a seminal work by Williams [8] from a few years ago, which proved NEXP does not have polynomial-size ACC0 circuits, via a new algorithmic approach to circuit lower bounds [9].