Ironic Complicity: Satisfiability Algorithms and Circuit Lower Bounds

摘要: I discuss recent progress in developing and exploiting connections between SAT algorithms 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 formal connection from non-trivial SAT to also various the reverse direction, have led to improved k-SAT, Formula-SAT AC^0-SAT, among other problems.