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?
