We revisit the complexity of the satisfiability problem for quantified Boolean formulas. We show that satisfiabilityof quantified CNFs of size \poly(n) on n variables with O(1)quantifier blocks can be solved in time 2n−n(1) by zero-errorrandomized algorithms. This is the first known improvement over brute force search in the general case,even for quantified polynomial-sized CNFs with one alternation. The algorithm gives an improvement over 2n when the number of quantifier blocks is q=o(loglognlogloglogn) . We also show how to achieve non-trivial savings on formulae when the number of quantifier blocks is q=(logn).

Next, we study the time complexities of QBF satisfiability over CNF formulas versus QBF over arbitrary Boolean formulas. We present surprisingly strong relationships between these time complexities, showing how to efficiently express Boolean formulas as quantified CNFs. As a consequence, the two problems have essentially equivalent time complexities in many cases, and further improvements over brute force search for quantified CNF satisfiability would imply breakthroughs in circuit complexity. For example, if satisfiability of quantified CNF formulae with n variables, \poly(n) size and at most q quantifier blocks can be solved in time 2n−nq(1q) , then \NEXP does not have O(logn) depth circuits of polynomial size. Furthermore, solving satisfiability of quantified CNF formulae with n variables, \poly(n) size and O(logn) quantifier blocks in time 2n−(log(n)) time would imply the same circuit complexity lower bound. Therefore, substantial improvements on the algorithms of this paper would imply new circuit complexity lower bounds.