has binary type $\gamma$. A [*universal constraint*]{} $c_\forall$ is a tuple $(\sigma, \gamma, \tau)$ where $\sigma, \tau \in \Sigma_T$ and $\gamma \in
\Gamma_T$. A structure with domain $D$ satisfies $c_\forall$ if no tuple $(a,b)\in D^2$ has binary type $\gamma$ if $a$ and $b$ have unary types $\sigma$ and $\tau$. A structure is a *solution* of $C$ if it satisfies all constraints in $C_\exists$ and $C_\forall$. The problem $C$ is solvable if it has a finite solution. The *size* $|C|$ of $C$ is . We emphasize that $C_\exists$ specifies required patterns whereas $C_\forall$ specifies forbidden patterns.

Let ${{\cal K}\xspace}$ be class of structures over a signature $T' \subseteq T$. The problem $C$ is *solvable on the class of structures ${{\cal K}\xspace}$* if it has a solution ${\ensuremath{\mathfrak{A}}}$ such that the restriction of ${\ensuremath{\mathfrak{A}}}$ to $T'$ belongs to ${{\cal K}\xspace}$. Such a solution will also be called *${{\cal K}\xspace}$-solution*.

The following lemma shows that ${\ensuremath{\mathrm{ESO}^2}\xspace}$-sentences can be translated into existential second-order constraint problems preserving satisfiability.

\[lemma:formulaToConstraint\] For every ${\ensuremath{\mathrm{ESO}^2}\xspace}$-sentence $\varphi$ there is a constraint problem $C$ such that $\varphi$ is ${{\cal K}\xspace}$-satisfiable if and only if $C$ has a ${{\cal K}\xspace}$-solution. The constraint problem $C$ can be computed in exponential time in 