Non-uniform circuit lower bounds are among the strongest impossibility results attainable in complexity theory, but they are also among the most difficult to prove. The circuit class ACC consists of circuit families with constant depth over unbounded fan-in AND, OR, NOT, and MODm gates, where $m > 1$ is an arbitrary constant. Despite the apparent simplicity of such circuits, the power of MODm has been very hard to reason about. For instance, it was not known whether a complexity class as large as $EXP^{NP}$ (the class of languages recognized in $2^{O(n^k)}$ time with an NP oracle) could be simulated with depth-$3$ polynomial size circuits made out of only MOD6 gates. We prove: - There are functions computable in Nondeterministic Exponential Time that cannot be simulated with non-uniform ACC circuits of polynomial size. The size lower bound can be slightly strengthened to quasi-polynomials and other less natural functions. - There are functions in $EXP^{NP}$ that cannot be simulated with non-uniform ACC circuits of $2^{n^{o(1)}}$ size. The lower bound gives an exponential size-depth tradeoff: for every $d$ and $m$ there is a $b > 0$ such that the relevant function doesn't have depth-$d$ ACC circuits of size $2^{n^b}$ with MODm gates. The proofs are more interesting than the results. The high-level strategy is to design faster algorithms for the circuit satisfiability problem over ACC circuits, then show how such algorithms can be applied to yield lower bound proofs against ACC circuits, via a more general "algorithm-lower bound" connection. This connection provides a new direction for further progress in circuit complexity.