Description |
We give the first algorithms for the QBF Satisfiability problem beating brute force search. We show that the QBF satisfiability question for CNF instances with $n$ variables, $q$ quantifier blocks and size poly(n) can be solved in time 2^{n-\Omega(n^{1/(q+1))}, and that the QBF satisfiability question for circuit instances with $n$ variables, $q$ quantifier blocks and size poly(n) can be solved in time 2^{n-\Omega(q)}. We also show that improvements on these algorithms would lead to super-polynomial formula size lower bounds for NEXP (this is joint work with Ryan Williams).
|