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
[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.
has been defined to describe the class of computational problems that may be translated into equivalent sentences of this form.
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.
As Tarski showed, this theory can be described by an axiom schema and a decision procedure that is complete and effective: for every fully quantified and grammatical sentence, either the sentence or its negation (but not both) can be derived from the axioms.
is a quantifier-free formula involving equalities and inequalities of real polynomials.
The decision problem for the existential theory of the reals is the algorithmic problem of testing whether a given sentence belongs to this theory; equivalently, for strings that pass the basic syntactical checks (they use the correct symbols with the correct syntax, and have no unquantified variables) it is the problem of testing whether the sentence is a true statement about the real numbers.
[1] In determining the time complexity of algorithms for the decision problem for the existential theory of the reals, it is important to have a measure of the size of the input.
The simplest measure of this type is the length of a sentence: that is, the number of symbols it contains.
[5] However, in order to achieve a more precise analysis of the behavior of algorithms for this problem, it is convenient to break down the input size into several variables, separating out the number of variables to be quantified, the number of polynomials within the sentence, and the degree of these polynomials.
Because the golden ratio is not transcendental, this is a true sentence, and belongs to the existential theory of the reals.
The answer to the decision problem for the existential theory of the reals, given this sentence as input, is the Boolean value true.
The inequality of arithmetic and geometric means states that, for every two non-negative numbers
As stated above, it is a first-order sentence about the real numbers, but one with universal rather than existential quantifiers, and one that uses extra symbols for division, square roots, and the number 2 that are not allowed in the first-order theory of the reals.
However, by squaring both sides it can be transformed into the following existential statement that can be interpreted as asking whether the inequality has any counterexamples: The answer to the decision problem for the existential theory of the reals, given this sentence as input, is the Boolean value false: there are no counterexamples.
Therefore, this sentence does not belong to the existential theory of the reals, despite being of the correct grammatical form.
Alfred Tarski's method of quantifier elimination (1948) showed the existential theory of the reals (and more generally the first order theory of the reals) to be algorithmically solvable, but without an elementary bound on its complexity.
[9][6] The method of cylindrical algebraic decomposition, by George E. Collins (1975), improved the time dependence to doubly exponential,[9][10] of the form
is the number of bits needed to represent the coefficients in the sentence whose value is to be determined,
[8] By 1988, Dima Grigoriev and Nicolai Vorobjov had shown the complexity to be exponential in a polynomial of
and in a sequence of papers published in 1992 James Renegar improved this to a singly exponential dependence on
In the meantime, in 1988, John Canny described another algorithm that also has exponential time dependence, but only polynomial space complexity; that is, he showed that the problem could be solved in PSPACE.
[2][9] The asymptotic computational complexity of these algorithms may be misleading, because in practice they can only be run on inputs of very small size.
In a 1991 comparison, Hoon Hong estimated that Collins' doubly exponential procedure would be able to solve a problem whose size is described by setting all the above parameters to 2, in less than a second, whereas the algorithms of Grigoriev, Vorbjov, and Renegar would instead take more than a million years.
[8] In 1993, Joos, Roy, and Solernó suggested that it should be possible to make small modifications to the exponential-time procedures to make them faster in practice than cylindrical algebraic decision, as well as faster in theory.
For instance, although the crossing number of a graph (the minimum number of crossings in a drawing with arbitrarily curved edges) may be determined in NP, it is complete for the existential theory of the reals to determine whether there exists a drawing achieving a given bound on the rectilinear crossing number (the minimum number of pairs of edges that cross in any drawing with edges drawn as straight line segments in the plane).
[21] Other complete problems for the existential theory of the reals include: Based on this, the complexity class
has been defined as the set of problems having a polynomial-time many-one reduction to the existential theory of the reals.