3
$\begingroup$

All known examples for double exponential lower bounds for real quantifier elimination involves polynomial inequalities with degree $>1$.

Is there an example of double exponentiality with polyhedral inequalities where polyhedral inequalities refers degree is at most $1$?

Conjecture: There is none and if you have $t$ quantifications with $n$ variables per quantification and $m$ constraints the complexity is $O(poly(n^{O(t)}m))$.

Perhaps the complexity is even $O(poly(ntm))$.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ The easy bound on time is $a^{2^v}$, where $a$ is the number of atomic formulas and $v$ is the number of variables. We prove this by induction: if the $\phi_j$ are atomic formulas, then $\exists x \bigwedge \phi_j$ is equivalent to the conjunction of formulas like $x < p_j$, $x=q_j$, $x>r_j$, which is equivalent to the conjunction of formulas like $p_j > q_k$, $p_j > r_k$, $q_j > r_k$ or $q_j = q_k$, which eliminates one variable and at most squares the number of atomic formulas. But I expect a better bound is available. $\endgroup$
    – user44143
    Commented Sep 29, 2019 at 15:38
  • $\begingroup$ @MattF. Is there an example for $$\exists{\bf x}\in\mathcal P\cap\mathbb R^n\mbox{ }\forall{\bf y}\in\mathcal Q\cap\mathbb R^{n'}$$$$\exists{\bf u}\in\mathcal L\cap\mathbb R^m\mbox{ }\forall{\bf v}\in\mathcal M\cap\mathbb R^{m'}$$ $$\bf A\cdot\{x,y,u,v\}^T\leq b$$ type dequantification where $\mathcal P,\mathcal Q,\mathcal L,\mathcal M$ are all bounded compact polytopes given in $\mathcal H$ representation and $\bf A,v$ are constant real matrix and vector respectively giving a set of linear inequalities in $\bf{x,y,u,v}$? As I understand we remove $x$ first and then $y$ and so on correct? $\endgroup$
    – VS.
    Commented Oct 5, 2019 at 19:35
  • $\begingroup$ The quantifier elimination I know goes from the inside out. Eg $\forall v\in [2,3)\ fv + g < h$ is equivalent to $f>0 \wedge 3f+g \le h$ or $f=0 \wedge g<h$ or $f<0 \wedge 2f + g < h$. $\endgroup$
    – user44143
    Commented Oct 5, 2019 at 19:51
  • $\begingroup$ That is fine since I do not know much about this area and I am sure I made a mistake. Is there good helpful example with $n>1$, $n'>1$, $m>1$ and $m'>1$? $\endgroup$
    – VS.
    Commented Oct 5, 2019 at 19:52
  • $\begingroup$ write down an example, and see what you get when you remove the innermost quantifier or two! $\endgroup$
    – user44143
    Commented Oct 5, 2019 at 20:02

1 Answer 1

Reset to default
4
$\begingroup$

I believe the following is a counterexample to the stronger $O(\mathrm{poly}(n,t,m))$ conjecture. Start with variables $x_i$ for $1 \leq i \leq n$ and $t_{ij}$ for $1 \leq i < j \leq n$. Consider the formula $$\phi=\exists t_{12} \ldots \exists t_{n-1,n}\left(\bigwedge_i x_i = \sum_{j<i} t_{ji} - \sum_{j>i} t_{ij}\right) \wedge\left(\bigwedge_{i,j}0 \leq t_{ij} \leq 1\right).$$ Eliminate the $t_{ij}$. Then $\phi$ holds if and only if $(x_1, \ldots, x_n)$ is in the Minkowski sum of the $\binom{n}{2}$ vectors $e_i - e_j$. This Minkowski sum is a permutahedron with one defining equality and $2^{n}-2$ defining inequalities.

The number of variables $\binom{n}{2}+n$, number of atomic formulas $n^2$ and largest number of terms in one atomic formula $n$ are all polynomial in $n$, but $2^n-2$ is not.

Still thinking about if I can beat $O(\mathrm{poly}(n^t, m))$ or get double exponential.

Example of the above: Let $n=4$. Then $\phi$ is the quantified conjunction of the $4^2$ atomic formulas: $$x_1 = -t_{12}-t_{13}-t_{14}$$ $$x_2 = t_{12}-t_{23}-t_{24}$$ $$x_3 = t_{13} + t_{23} - t_{34}$$ $$x_4 = t_{14} + t_{24} + t_{34}$$ $$0 \le t_{12} \le 1,\ \ 0 \le t_{13} \le 1,\ \ 0 \le t_{14} \le 1$$ $$0 \le t_{23} \le 1,\ \ 0 \le t_{24} \le 1,\ \ 0 \le t_{34} \le 1$$

And $\phi$ holds iff the conjunction of the following $2^4-1$ atomic formulas holds: $$x_1 + x_2 + x_3 + x_4 = 0$$ $$-2 \le \ \ \ x_2 \ \ \ \le 1$$ $$-1 \le \ \ \ x_3 \ \ \ \le 2$$ $$\ \ 0 \le \ \ \ x_4 \ \ \ \le 3$$ $$-2 \le \ \ x_2 + x_3 \ \ \le 2$$ $$-1 \le \ \ x_2 + x_4 \ \ \le 3$$ $$\ \ 0 \le \ \ x_3 + x_4 \ \ \le 4$$ $$\ \ 0 \le x_2 + x_3 + x_4 \le 3$$

Improve this answer
$\endgroup$
16
  • $\begingroup$ How many quantifiers (sorry $t$ and $t_{ij}$ confusing)? $\endgroup$
    – VS.
    Commented Oct 2, 2019 at 21:36
  • $\begingroup$ $\binom{n}{2}$ quantifiers. There is one $\exists t_{ij}$ for each $1 \leq i < j \leq n$. $\endgroup$
    – David E Speyer
    Commented Oct 2, 2019 at 23:47
  • 1
    $\begingroup$ Thanks for the clarification. I hope my edit is helpful. $\endgroup$
    – user44143
    Commented Oct 4, 2019 at 18:06
  • 1
    $\begingroup$ @VS., no. You can check that the inequality $x_2 \le 1$ is required by finding a 4-tuple with $x_2>1$ that satisfies all the other inequalities but does not satisfy the original formula. Similarly you can check that all the other inequalities are required, and there is no way to produce a list of exponentially-many inequalities in polynomial time. Meanwhile, since this was “just one query”, I will not comment further. $\endgroup$
    – user44143
    Commented Oct 6, 2019 at 8:34
  • 1
    $\begingroup$ @VS Yes. And I realized a few weeks ago that there is a much simpler example, though you might think of it as cheating. Consider $3n$ variables $x_i$, $y_i$, $z_i$, with the formula $0 \leq x_i \wedge 0 \leq y_i \wedge \sum x_i + \sum y_i = 1 \wedge z_i = x_i - y_i$. If you eliminate the $x_i$ and $y_i$, then the possible $z_i$ is the region in $\mathbb{R}^n$ given by $\sum |z_i| \leq n$. If we are supposed to express this in the language $+$, $-$, $\leq$ without an absolute value symbol, and without adding extra variables, I think it takes a formula of exponential length. $\endgroup$
    – David E Speyer
    Commented Nov 22, 2019 at 16:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .