We study algorithms for the satisfiability problem for quantified Boolean formulas (QBFs), and consequences of faster algorithms for circuit complexity.
\begin{itemize}
\item We show that satisfiability of quantified 3-CNFs with $m$ clauses, $n$ variables, and two quantifier blocks (one existential block and one universal) can be solved deterministically in time
$2^{n-\Omega(\sqrt{n})} \cdot \poly(m)$. For the case of multiple quantifier blocks (alternations), we show that satisfiability
of quantified CNFs of size $\poly(n)$ on $n$ variables with $q$
quantifier blocks can be solved in $2^{n-n^{1/(q+1)}}\cdot \poly(n)$ time by a zero-error randomized algorithm. These are the first provable improvements over brute force search in the general case, even for quantified polynomial-sized CNFs with two quantifier blocks.

A second zero-error randomized algorithm solves QBF on circuits of size $s$ in $2^{n-\Omega(q)} \cdot \poly(s)$ time when the number of quantifier blocks is $q$.

\item
We complement these algorithms by showing that improvements on them would imply new circuit complexity lower bounds. For example, if satisfiability of quantified CNF formulas with $n$ variables, $\poly(n)$ size and at most $q$ quantifier blocks can be solved in time $2^{n-n^{\omega_{q}(1/q)}}$, then the complexity class $\NEXP$ does not have $O(\log n)$ depth circuits of polynomial size.

Furthermore, solving satisfiability of quantified CNF formulas with $n$ variables, $\poly(n)$ size and $O(\log n)$ quantifier blocks in time $2^{n - \omega(\log(n))}$ time would imply the same circuit complexity lower bound. The proofs of these results proceed by establishing strong relationships between the time complexity of QBF satisfiability over CNF formulas and the time complexity of QBF satisfiability over arbitrary Boolean formulas.

Improved algorithm for QBF Satisfiability, which is optimal modulo new circuit lower bounds

We revisit the complexity of the satisfiability problem for quantified Boolean formulas. We show that satisfiability
of quantified CNFs of size $\poly(n)$ on $n$ variables with $O(1)$
quantifier blocks can be solved in time $2^{n-n^{\Omega(1)}}$ by zero-error
randomized 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 $2^n$ when the number of quantifier blocks is $q = o(\log \log n/\log \log \log n)$. We also show how to achieve non-trivial savings on formulae when the number of quantifier blocks is $q = \omega(\log n)$.

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 $2^{n-n^{\omega_{q}(1/q)}}$, then $\NEXP$ does not have $O(\log n)$ depth circuits of polynomial size. Furthermore, solving satisfiability of quantified CNF formulae with $n$ variables, $\poly(n)$ size and $O(\log n)$ quantifier blocks in time $2^{n - \omega(\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.