New Algorithms for QBF Satisfiability and Implications for Circuit Complexity

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 2n−n Ω(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 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 = ω(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 2n−n ω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 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. ISSN 1433-8092 Electronic Colloquium on Computational Complexity, Report No. 108 (2013)