In this talk, we'll explore a self-improvement phenomenon for Circuit-SAT, $\#$Circuit-SAT and its fully quantified variants. We'll see that even modest improvements over brute-force algorithms for large circuits—where satisfiability is polynomial-time solvable—can be amplified into significant speedups for smaller, subexponential-size circuits. The arguments will also work for a variety of models solving circuit-analysis problems, including non-uniform circuits and randomized models of computation.
