The problem is to decide whether a quantified boolean formula (QBF) F defined as:
F = FORALL Y EXISTS X G
(where X and Y are disjoint sets of variables and G is a CNF formula over variables from X union Y) is true. That is, we want to know whether it is true that for each truth assignment to the variables in Y there is a truth assignment to the variables in X which makes G true.
INPUT: Sets of variables X and Y, CNF formula G
OUTPUT: message YES if G holds; otherwise NO.