# Lower bound for polyhedral real quantifier elimination

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))$$.

• 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. – Matt F. Sep 29 '19 at 15:38
• @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? – VS. Oct 5 '19 at 19:35
• 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$. – Matt F. Oct 5 '19 at 19:51
• 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$? – VS. Oct 5 '19 at 19:52
• write down an example, and see what you get when you remove the innermost quantifier or two! – Matt F. Oct 5 '19 at 20:02

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_{ji} 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$$

• How many quantifiers (sorry $t$ and $t_{ij}$ confusing)? – VS. Oct 2 '19 at 21:36
• $\binom{n}{2}$ quantifiers. There is one $\exists t_{ij}$ for each $1 \leq i < j \leq n$. – David E Speyer Oct 2 '19 at 23:47
• Thanks for the clarification. I hope my edit is helpful. – Matt F. Oct 4 '19 at 18:06
• @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. – Matt F. Oct 6 '19 at 8:34
• @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. – David E Speyer Nov 22 '19 at 16:21