I discuss recent progress in developing and exploiting connections betweenSAT algorithms and circuit lower bounds. The centrepiece of the article isWilliams' proof that NEXPACC0 , which proceeds via a newalgorithm for ACC0-SAT beating brute-force search. His result exploitsa formal connection from non-trivial SAT algorithms to circuitlower bounds. I also discuss various connections in the reverse direction,which have led to improved algorithms for k-SAT, Formula-SAT and AC0-SAT, among other problems.