Beating Exhaustive Search for Quantified Boolean Formulas and Connections to Circuit Complexity

We study algorithms for the satisfiability problem for quantified Boolean formulas (QBFs), and consequences of faster algorithms for circuit complexity. 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 . 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 2n−n1/(q + 1)· 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 2n–Ω(q) · poly(s) time when the number of quantifier blocks is q. 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 2n–nwq (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 2n–w(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.