Ironic Complicity: Satisfiability Algorithms and Circuit Lower Bounds
Rahul Santhanam · Bulletin of the European Association for Theoretical Computer Science · 2012
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 ot\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.