I will discuss recent work on beating exhaustive search for solving satisfiability on quantified Boolean formulas with a small number of quantifier blocks. The talk will include (i) an algorithmic result: satisfiability of QBF formulas of size poly(n) on n variables and with q quantifier blocks can be solved in time 2^{n-(n^{\Omega(1/q)})}  and (ii) a connection with lower bounds: even slight improvements of our algorithmic results would imply NEXP not in NC^1

 

This is based partly on joint works with Ruiwen Chen and Ryan Williams.