Existential theory of the reals

In mathematical logic, computational complexity theory, and computer science, the existential theory of the reals is the set of all true sentences of the form $${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),}$$ where the variables ${\displaystyle X_{i}}$ are interpreted as having real number values, and where ${\displaystyle F(X_{1},\dots X_{n})}$ is a quantifier-free formula involving equalities and inequalities of real polynomials. A sentence of this form is true if it is possible to find values for all of the variables that, when substituted into formula ${\displaystyle F}$, make it become true.^[1]

The decision problem for the existential theory of the reals is the problem of finding an algorithm that decides, for each such sentence, whether it is true or false. Equivalently, it is the problem of testing whether a given semialgebraic set is non-empty.^[1] This decision problem is NP-hard and lies in PSPACE,^[2] giving it significantly lower complexity than Alfred Tarski's quantifier elimination procedure for deciding statements in the first-order theory of the reals without the restriction to existential quantifiers.^[1] However, in practice, general methods for the first-order theory remain the preferred choice for solving these problems.^[3]

The complexity class ${\displaystyle \exists \mathbb {R} }$ has been defined to describe the class of computational problems that may be translated into equivalent sentences of this form. In structural complexity theory, it lies between NP and PSPACE. Many natural problems in geometric graph theory, especially problems of recognizing geometric intersection graphs and straightening the edges of graph drawings with crossings, belong to ${\displaystyle \exists \mathbb {R} }$, and are complete for this class. Here, completeness means that there exists a translation in the reverse direction, from an arbitrary sentence over the reals into an equivalent instance of the given problem.^[4]