Complexity one-alternation SMT

Question

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>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

Answer 1

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 & 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".

Answer 2

A single alternation in Presburger arithmetic is enough to obtain exponential lower bounds, more precisely formulae as in the question with $m=1$ and $n$ not fixed suffice (Grädel 1989).

Answer 3

I do not know references for the quantified fragment but your problem is not the same as deciding well studied fragments of Presburger arithmetic because you have unit coefficients.

The paper below by Pratt studies the case where constraints are of the form $x + c < y$, where $x$ and $y$ are variables and $c$ in a natural number. He shows that the problem of deciding if a conjunction of such constraints can be done efficiently using a graph algorithm.

Two easy theories whose combination is hard. Pratt, 1977.

This fragment is also called difference logic and was, for a brief time, unfortunately called separation logic (because $x$ and $y$ are separated by a constant). The following paper provides a practical view of solving the quantifier-free fragment of the problem.

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. Chao Wang, Franjo Ivančić, Malay Ganai, Aarti Gupta, 2005.

At present, your question only permits the coefficients $0$ and $1$. If you also allow $-1$ as a coefficient, the conjunctions of constraints you get are called octagons in the program analysis literature. Conjunctions and disjunctions of constraints are form the logic of Unit Two Variables Per Inequality (UTVPI). The introduction of the following paper surveys algorithms for deciding satisfiability of conjunctions of quantifier-free UTVPI constraints.

An Efficient Decision Procedure for UTVPI Constraints. Shuvendu K. Lahiri and Madanlal Musuvathi, 2005.

We are still in a very restricted fragment. The extension to conjunctions of $n$-variable linear inequalities with unit coefficients has is called an octahedron. It is such a natural extension that I would expect it has been studied in the mathematical programming and optimization literature but I do not know that literature myself. The paper below gives an $\mathcal{O}(3^n)$ procedure for deciding satisfiability of such constraints. Note that we are still in the quantifier free fragment.

The Octahedron Abstract Domain. Robert Clarisó and Jordi Cortadella, 2004.

For the bounded quantifier alternation case, I do not know of better results than those of Reddy and Loveland but maybe an expert can point you in the right direction.