Algorithms for quantified Boolean formulas
Ryan Williams · 2002
We present algorithms for solving quantified Boolean formulas (QBF, or sometimes QSAT) with worst case runtime asymptotically less than O(2^n) when the clause-to-variable ratio is smaller or larger than some constant. We solve QBFs in conjunctive normal form (CNF) in O(1.709^m) time and space, where m is the number of clauses. Extending the technique to a quantified version of constraint satisfaction problems (QCSP), we solve QCSP with domain size d = 3 ) time, and QCSPs with d 4 in O(d m/2 # time and space for # > 0, where m is the number of constraints. For 3-CNF QBF, we describe an polynomial space algorithm with time complexity O(1.619 ) when the number of 3-CNF clauses is equal to n