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?


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.

  • $\begingroup$ My comment/response is too long to fit here, so i posted a new question: Is the first-order theory (with =) of real numbers with addition and multiplication complete and decidable? $\endgroup$ – Gavin Jun 20 '13 at 12:09
  • 1
    $\begingroup$ Gavin, yes, it is. That is exactly a consequence of Tarski's theorem. $\endgroup$ – Joel David Hamkins Jun 20 '13 at 12:44
  • $\begingroup$ Completeness is automatic, since the first-order theory of any single structure is always complete. Decidability follows from Tarski's theorem. $\endgroup$ – Andreas Blass Jun 20 '13 at 15:00

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.