Two-block quantified Boolean formula (source code)

= Two-block quantified Boolean formula
{title2=$\exists X\,\forall Y\,\psi(X,Y)$}

A <propositional formula> with two blocks of quantified <Boolean variables>. Determining the truth of an existential-then-universal instance is a canonical complete problem for the existential <second level of the polynomial hierarchy>, $\Sigma_2^{\mathrm P}$. For completeness one may restrict the matrix $\psi$ to a disjunction of terms with at most three literals. The order of the quantifiers matters: the assignment to $X$ must work for every assignment to $Y$.