<p>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 (<a href="http://dx.doi.org/10.1016/0168-0072(89)90023-7">Grädel 1989</a>).</p>

CC BY-SA 3.0
2013-04-24T21:00:13.897Z
2013-04-24T21:00:13.897Z
Sylvain
<p>The question of truth in Presburger Arithmetic with bounded quantifier alternation has been answered with quite some precision by Reddy and Loveland:</p>

<p>C.R. Reddy &amp; D.W. Loveland: <em>Presburger Arithmetic with Bounded Quantifier Alternation</em>.</p>

<p>The paper may be found <a href="http://delivery.acm.org/10.1145/810000/804361/p320-reddy.pdf?ip=128.2.74.227&amp;acc=ACTIVE%20SERVICE&amp;key=C2716FEBFA981EF1D8ED4F16102DA82BADDD11EBB600FF97&amp;CFID=208989787&amp;CFTOKEN=20527215&amp;__acm__=1366822425_8b68699129c304f21844d58cf89f642a">here</a> (sorry for the ugly link). Their main result is stated as follows:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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".</p>

CC BY-SA 3.0
2013-04-24T17:00:09.750Z
2013-04-24T17:00:09.750Z
cody
<p>I do not know references for the quantified fragment but your problem is <em>not the same</em> as deciding well studied fragments of Presburger arithmetic because you have unit coefficients.</p>

<p>The paper below by Pratt studies the case where constraints are of the form $x + c &lt; 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.</p>

<blockquote>
  <p><a href="http://boole.stanford.edu/pub/sefnp.pdf">Two easy theories whose combination is hard.</a> Pratt, 1977.</p>
</blockquote>

<p>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.</p>

<blockquote>
  <p><a href="http://vlsi.colorado.edu/~wangc/pubDOC/Wang05SLICE.pdf">Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination.</a> Chao Wang, Franjo Ivančić, Malay Ganai, Aarti Gupta, 2005.</p>
</blockquote>

<p>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 <em>octagons</em> in the program analysis literature. Conjunctions and disjunctions of constraints are form the logic of <em>Unit Two Variables Per Inequality (UTVPI)</em>. The introduction of the following paper surveys algorithms for deciding satisfiability of conjunctions of quantifier-free UTVPI constraints.</p>

<blockquote>
  <p><a href="http://research.microsoft.com/pubs/70176/tr-2005-67.pdf">An Efficient Decision Procedure for UTVPI Constraints.</a> Shuvendu K. Lahiri and Madanlal Musuvathi, 2005.</p>
</blockquote>

<p>We are still in a very restricted fragment. The extension to conjunctions of $n$-variable linear inequalities with unit coefficients has is called an <em>octahedron</em>. 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. </p>

<blockquote>
  <p><a href="http://www.lsi.upc.edu/~jordicf/gavina/BIB/files/sas2004.pdf">The Octahedron Abstract Domain.</a>  Robert Clarisó and Jordi Cortadella, 2004.</p>
</blockquote>

<p>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.</p>

CC BY-SA 3.0
2013-04-24T22:07:37.910Z
2013-04-24T22:07:37.910Z
Vijay D
<p>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}$.</p>

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

<p>All answer with references would be gladly accepted.</p>

<p>Thanks </p>

CC BY-SA 3.0
2013-04-24T11:07:58.490Z
If phi was Boolean, then you're in the second level of polynomial hierarchy  because I can solve the problem by a non-deterministic Turing machine using a SAT solver as an oracle. Wouldn't the same reasoning work here?
Mikolas
CC BY-SA 3.0
2013-04-24T12:13:17.860Z
As stated in the question it seems even undecidable, since it includes Hilberts 10th problem http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem
Magnus Find
CC BY-SA 3.0
2013-04-24T13:14:42.073Z
@MagnusFind Thanks, you are right. But in fact I don't have the multiplication (edited, sorry).
wece
CC BY-SA 3.0
2013-04-24T13:17:07.600Z
@Mikolas by second level you mean $\Pi_2$ or $\Sigma_2$? In not really familiar with polynomial hierarchy sorry.
wece
CC BY-SA 3.0
2013-04-24T22:13:04.960Z
Do you have other free variables other than those quantified ones? If so you should clarify that also. Btw, an easy observation seems to be that this is at least hard for the third level of polynomial hierarchy even if you take the quantified variables to be $0$ and $1$.
Kaveh
<cc.complexity-theory><reference-request><lo.logic>
Complexity one-alternation SMT
wece
# Complexity one-alternation SMT

(Asked by: username_0 on 2013-04-24)

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

**Tags:** cc.complexity-theory, reference-request, lo.logic
> **Comments:**
> **username_1**: If phi was Boolean, then you're in the second level of polynomial hierarchy  because I can solve the problem by a non-deterministic Turing machine using a SAT solver as an oracle. Wouldn't the same reasoning work here?  
> **username_2**: As stated in the question it seems even undecidable, since it includes Hilberts 10th problem http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem  
> **username_0**: @MagnusFind Thanks, you are right. But in fact I don't have the multiplication (edited, sorry).  
> **username_0**: @Mikolas by second level you mean $\Pi_2$ or $\Sigma_2$? In not really familiar with polynomial hierarchy sorry.  
> **username_3**: Do you have other free variables other than those quantified ones? If so you should clarify that also. Btw, an easy observation seems to be that this is at least hard for the third level of polynomial hierarchy even if you take the quantified variables to be $0$ and $1$.  

---

## 3 answers

### Answer by username_4 on 2013-04-24. Score: 6

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](http://dx.doi.org/10.1016/0168-0072(89)90023-7)).


---

### Answer by username_5 on 2013-04-24. Score: 6

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](http://delivery.acm.org/10.1145/810000/804361/p320-reddy.pdf?ip=128.2.74.227&acc=ACTIVE%20SERVICE&key=C2716FEBFA981EF1D8ED4F16102DA82BADDD11EBB600FF97&CFID=208989787&CFTOKEN=20527215&__acm__=1366822425_8b68699129c304f21844d58cf89f642a) (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 by username_6 on 2013-04-24. Score: 5

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.](http://boole.stanford.edu/pub/sefnp.pdf) 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.](http://vlsi.colorado.edu/~wangc/pubDOC/Wang05SLICE.pdf) 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.](http://research.microsoft.com/pubs/70176/tr-2005-67.pdf) 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.](http://www.lsi.upc.edu/~jordicf/gavina/BIB/files/sas2004.pdf) 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.


---

