Two-block quantified Boolean formula ($\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$.