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

Is the system

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

feasible, where $x$ is a column vector of length $n$, $x^T$ is the transpose of $x$, $r_i$ and $r_j$ are rational constants in [0,1], and $Q_i$ and $Q_j$ are symmetric indefinite $n \times n$ matrices. Vector $x$ is the $n$ unknowns and they are in [0,1].

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?