Abstract / Description of output
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 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.
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 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.
| Original language | English |
|---|---|
| Pages (from-to) | 108 |
| Number of pages | 14 |
| Journal | Electronic Colloquium on Computational Complexity (ECCC) |
| Volume | 20 |
| Publication status | Published - 10 Aug 2013 |