I discuss recent progress in developing and exploiting connections between
SAT algorithms and circuit lower bounds. The centrepiece of the article is
Williams' proof that $NEXP \not \subseteq ACC^0$, which proceeds via a new
algorithm for $ACC^0$-SAT beating brute-force search. His result exploits
a formal connection from non-trivial SAT algorithms to circuit
lower bounds. I also discuss various connections in the reverse direction,
which have led to improved algorithms for $k$-SAT, Formula-SAT and $AC^0$-SAT, among other problems.