Quantified boolean formula problem

From Wikipedia, the free encyclopedia

In computational complexity theory, the quantified boolean formula problem (QBF) is a generalization of the boolean satisfiability problem in which both existential quantifiers and universal quantifiers can be applied to each variable. Put another way, it asks whether a first-order logic sentential form over a set of boolean variables is true or false. For example, the following is an instance of QBF:

$\forall x\ \exists y\ \exists z\ (x \lor y \lor z) \land (\lnot x \lor \lnot y \lor \lnot z)$

QBF is the canonical complete problem for PSPACE, the class of problems solvable by a deterministic or nondeterministic Turing machine in polynomial space and unlimited time.¹ Given the formula in the form of an abstract syntax tree, the problem can be solved easily by a set of mutually recursive procedures which evaluate the formula. Such an algorithm uses space proportional to the height of the tree, which is linear in the worst case, but uses time exponential in the number of quantifiers.

Provided that MA ≠ PSPACE, which is widely believed, QBF cannot be solved, nor can a given solution even be verified, in either deterministic or probabilistic polynomial time (in fact, unlike the satisfiability problem, there's no known way to specify a solution succinctly). It is trivial to solve using an alternating Turing machine in linear time, which is no surprise since in fact AP = PSPACE, where AP is the class of problems alternating machines can solve in polynomial time. ²

When the seminal result IP = PSPACE was shown (see interactive proof system), it was done by exhibiting an IP interactive proof system that could solve QBF by solving a particular arithmetization of the problem.³

QBF formulas have a number of useful canonical forms. For example, it can be shown that there is a polynomial-time many-one reduction that will move all quantifiers to the front of the formula and make them alternate between universal and existential quantifiers. There is another reduction that proved useful in the IP = PSPACE proof where no more than one universal quantifier is placed between each variable's use and the quantifier binding that variable. This were critical in limiting the number of products in certain subexpressions of the arithmetization.

[edit] References

1. M. Garey and D. Johnson. Computers and intractability, a guide to the theory of NP-completeness. W. H. Freeman, San Francisco, California. 1979. ISBN 0-7167-1045-5.

2. A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. Journal of the ACM, volume 28, issue 1, p.114-133. 1981.

3. Adi Shamir. IP = PSPACE. Journal of the ACM, volume 39, issue 4, p.869-877. October 1992.