I would like to know whether the following problem is decidable.



> 
> Given the following system in $x \in [0,1]^n$
> 
> 
> $$x^T Q\_i x + r\_i = 0 \mbox{ for } i = 1, ..., k$$
> 
> 
> $$x^T Q\_j x + r\_j \neq 0 \mbox{ for } j = k+1, ..., t$$
> 
> 
> where $r\_i, r\_j \in [0,1]$ are rational constants and $Q\_i, Q\_j$ are symmetric indefinite $n \times n$ matrices, decide whether this system is feasible.
> 
> 
> 


According to me (after a series of transformations and added slack variables), the decidability problem above is equivalent to asking whether the global maximum of $q\_j^T x$ (a linear term) can be found, subject to non-linear, non-convex quadratic constraints


$$x^T Q\_i x + q\_i^T x + r\_i \leq 0 \mbox{ for } i = 1, ..., u$$


where $x$, $r\_i$ and $Q\_i$ have the same form as before (but are not identical), $q\_i$ is a column vector of length $n$, and $q\_i^T$ is the transpose of $q\_i$.


The latter formulation of the problem can be viewed as a Quadratically Constrained Quadratic Program (QCQP), except that the objective function is linear. And the constraints are, in general, non-linear.
Also note that the latter problem is posed as a decision problem, not purely an optimization problem.


Does either one of these problems have a decidability result?



Is the feasibility of a system of non-convex quadratic equations and inequations decidable?
For any fixed $n,k,t$, the feasibility question is a first-order formula in the language of real-closed fields; it would have the components of $x$ as existentially quantified variables and the $r$'s and the entries of the $Q$'s as free variables. Tarski's quantifier elimination theorem for real-closed fields converts this to a propositional combination of equations and inequalities for the free variables. The quantifier-elimination is algorithmic. So as long as the components of the $Q$'s are given in such a way that you can algorithmically do arithmetic with them, the feasibility question is decidable.


