Complexity one-alternation SMT I'm looking for the complexity of satisfiability of a formula $\forall y_1, \dots,y_n, \exists x_1,\dots,x_m, \phi$ or of a formula $ \exists x_1,\dots,x_m \forall y_1, \dots,y_n,\phi$ where $\phi$ is formula of the form : 
$$\phi:= \phi \wedge\phi ~| ~\neg \phi ~| ~ \phi\to \phi~| ~\psi$$
$$\psi := t&gt;t~| ~t=t$$
$$ t:= t+t~| ~x_i~|~y_i ~| ~c$$
Where $c$ are the constant in $\mathbb{N}$, and the domain of variables $x_i,y_i$ is also $\mathbb{N}$.

In fact the $y_i$ are either $0$ or $1$. Does that simplify the complexity?

All answer with references would be gladly accepted.

Thanks
The question of truth in Presburger Arithmetic with bounded quantifier alternation has been answered with quite some precision by Reddy and Loveland:

C.R. Reddy &amp; D.W. Loveland: Presburger Arithmetic with Bounded Quantifier Alternation.

The paper may be found here (sorry for the ugly link). Their main result is stated as follows:


  The membership in $\mathrm{PA}(m)$ (where $m$ is the number of quantifier alternations) of length $n$ can be decided within space
  $$ 2^{dn^{m+4}}$$
  and in (deterministic) time
  $$ 2^{2^{en^{m+4}}}$$
  Where $d$ and $e$ are constants.


Taking $m=2$, this seems to give at least an upper bound on what you want, and I suspect it's not far from tight, as you have almost full Presburger atomic formulas "at the root".