Existential theory of the reals

In mathematical logic, a theory is a formal language consisting of a set of sentences written using a fixed set of symbols. The first-order theory of real closed fields has the following symbols: The existential theory of the reals is the fragment of the first-order theory consisting of sentences in which all the quantifiers are existential and they appear before any of the other symbols. That is, it is the set of all true sentences of the form \exists X_1 \cdots \exists X_n \, F(X_1,\dots, X_n), where F(X_1,\dots X_n) 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. The set of n-tuples of real numbers (X_1,\dots X_n) for which F(X_1,\dots X_n) is true is called a semialgebraic set, so the decision problem for the existential theory of the reals can equivalently be rephrased as testing whether a given semialgebraic set is nonempty. 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. 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. ==Examples==

The golden ratio \varphi may be defined as the root of the polynomial x^2-x-1. This polynomial has two roots, only one of which (the golden ratio) is greater than one. Thus, the existence of the golden ratio may be expressed by the sentence \exists X_1( X_1 > 1 \wedge X_1\times X_1 - X_1 - 1 = 0). 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 x and y, the following inequality holds: \frac{x+y}{2} \ge \sqrt{xy}. 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: :\exists X_1 \exists X_2 \bigl( X_1\ge 0\wedge X_2\ge 0\wedge (X_1+X_2)\times (X_1+X_2) 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. ==Algorithms==

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. The method of cylindrical algebraic decomposition, by George E. Collins (1975), improved the time dependence to doubly exponential, of the form L^3 (md)^{2^{O(n)}} where L is the number of bits needed to represent the coefficients in the sentence whose value is to be determined, m is the number of polynomials in the sentence, d is their total degree, and n is the number of variables. By 1988, Dima Grigoriev and Nicolai Vorobjov had shown the complexity to be exponential in a polynomial of n, L(md)^{n^2} and in a sequence of papers published in 1992 James Renegar improved this to a singly exponential dependence L\log L\log\log L(md)^{O(n)}. 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. However, as of 2009, it was still the case that general methods for the first-order theory of the reals remained superior in practice to the singly exponential algorithms specialized to the existential theory of the reals. ==Complete problems==

Several problems in computational complexity and geometric graph theory may be classified as complete for the existential theory of the reals. That is, every problem in the existential theory of the reals has a polynomial-time many-one reduction to an instance of one of these problems, and in turn these problems are reducible to the existential theory of the reals. recognition of unit disk graphs, and recognition of intersection graphs of convex sets in the plane. It is also complete for the existential theory of the reals to test whether a given graph can be drawn in the plane with straight line edges and with a given set of edge pairs as its crossings, or equivalently, whether a curved drawing with crossings can be straightened in a way that preserves its crossings. Other complete problems for the existential theory of the reals include: • the art gallery problem of finding the smallest number of points from which all points of a given polygon are visible. • training neural networks. • the packing problem of deciding whether a given set of polygons can fit in a given square container. • recognition of unit distance graphs, and testing whether the dimension or Euclidean dimension of a graph is at most a given value. • stretchability of pseudolines (that is, given a family of curves in the plane, determining whether they are homeomorphic to a line arrangement); • both weak and strong satisfiability of geometric quantum logic in any fixed dimension >2; • Model checking interval Markov chains with respect to unambiguous automata. • the algorithmic Steinitz problem (given a lattice, determine whether it is the face lattice of a convex polytope), even when restricted to 4-dimensional polytopes; • realization spaces of arrangements of certain convex bodies • various properties of Nash equilibria of multi-player games • embedding a given abstract complex of triangles and quadrilaterals into three-dimensional Euclidean space; • embedding multiple graphs on a shared vertex set into the plane so that all the graphs are drawn without crossings; • determining the minimum slope number of a non-crossing drawing of a planar graph; • recognizing graphs that can be drawn with all crossings at right angles; • the partial evaluation problem for the MATLANG+eigen matrix query language. • the low-rank matrix completion problem. Based on this, the complexity class \exists \mathbb{R} has been defined as the set of problems having a polynomial-time many-one reduction to the existential theory of the reals. ==See also==