I have a quantified convex program of the form that I need to solve

$$\exists(x_{1,1},\dots,x_{1,n})\in\mathbb R^n\quad\forall(x_{2,1},\dots,x_{2,n})\in\mathbb R^n$$ $$\vdots$$ $$\exists(x_{2t-1,1},\dots,x_{2t-1,n})\in\mathbb R^n\quad\forall(x_{2t,1},\dots,x_{2t,n})\in\mathbb R^n$$ $$\phi_1(x_{1,1},\dots,x_{2t,n})\leq a_1\wedge\dots\wedge\phi_r(x_{1,1},\dots,x_{2t,n})\leq a_r$$ where $\phi_1,\dots,\phi_r$ are either linear degree $d=1$ or quadratic degree $d=2$ convex polynomials with $O(n)$ terms each with all polynomial coefficients and $a_1,\dots,a_r$ in $\mathbb Z$ and having at most $m$ bits each.

I feel quantifier elimination over reals will help here. However how to go about it is unclear.

  1. Does quantifier elimination tell anything about the time complexity of the program and if so what is the complexity and is it possible to use quantifier elimination to reduce the number of quantifications and if so how does the parameters change?

  2. Is it in $\Sigma_{k}$ in the polynomial hierarchy where $k=O(t)$ and independent of $m,n,r$?

  • 1
    $\begingroup$ Fully general quantifier elimination has doubly-exponential complexity on the number of quantifiers (sciencedirect.com/science/article/pii/S074771718880004X), so clearly you need to use your assumptions on the degree of your polynomials and their convexity. $\endgroup$ – Nell Mar 23 '19 at 18:02
  • 1
    $\begingroup$ why do you call this a “program”? you are not optimising anything here. $\endgroup$ – Dima Pasechnik Mar 24 '19 at 10:28
  • $\begingroup$ @Nell If it is doubly exponential only in number of quantifiers then why does degree matter? $\endgroup$ – VS. Mar 30 '19 at 21:27
  • $\begingroup$ The two dependencies (doubly exponential in the number of quantifiers, and at least exponential in the degree) are intertwined in cylindrical decomposition (i.e., it's not as if they were two terms that were added). $\endgroup$ – Nell Mar 31 '19 at 1:43
  • $\begingroup$ @Nell Thank you the paper is not clear to me. Would you know roughly what the complexity should be here for both $d=1$ and $d=2$? $\endgroup$ – VS. Mar 31 '19 at 2:37

it appears that one can eliminate one block of quantified variables in such a quadratic case faster, for fixed $r$, than in general, see e.g. https://arxiv.org/abs/0708.3522, but the result will have degrees going up. Thus for $t>1$ it appears to be rather useless, one could just use the general bound with the same effect.

| cite | improve this answer | |
  • $\begingroup$ 'one can eliminate one block of quantified variables in such a quadratic case faster' section please? $\endgroup$ – VS. Mar 24 '19 at 10:56
  • $\begingroup$ Well, I meant to say that technique used there, which is an extension of A. I. Barvinok. Feasibility testing for systems of real quadratic equations. Discrete Comput. Geom., 10(1):1–13, 1993. and arxiv.org/abs/cs/0403008) ought to work. $\endgroup$ – Dima Pasechnik Mar 24 '19 at 23:02
  • $\begingroup$ Since you are an author perhaps you could be little less cryptic in your remark. How does the technique help and what degrees does it give? $\endgroup$ – VS. Mar 25 '19 at 2:12
  • $\begingroup$ eliminating an $\exists$ block boils down to solving systems of inequalities, parametric w.r.t. to the remaining variables. (But it's a long story, how quantifier elimination works...) $\endgroup$ – Dima Pasechnik Mar 25 '19 at 8:08
  • $\begingroup$ 'it appears that one can eliminate one block of quantified variables in such a quadratic case faster, for fixed r' indicates you know the correct rate. Perhaps at least comment that and the theorem you are indicating in the paper? $\endgroup$ – VS. Mar 25 '19 at 10:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.