Abstract: We give the first algorithms for the QBF Satisfiability problem beating brute force search. We show that the QBF satisfiability question for CNF instances with $n$ variables, $q$ quantifier blocks and size $poly(n)$ can be solved in time $2^{n-\Omega(n^{1/(q+1)})}$, and that the QBF satisfiability question for circuit instances with $n$ variables, $q$ quantifier blocks and size $poly(n)$ can be solved in time $2^{n-\Omega(q)}$. We also show that improvements on these algorithms would lead to super-polynomial formula size lower bounds for NEXP (this is joint work with Ryan Williams).
