ALGORITHMS IN REAL ALGEBRAIC GEOMETRY: A SURVEY <s> Quantifier elimination and related problems <s> A centrifugal pump for use in pumping hot liquids under pressure. A rotatable shaft, having an impeller at its lower end, is positioned along the axis of a generally cylindrical pump casing. The pump casing has a suction nozzle at its lower end, and a discharge nozzle near the upper end. A cylindrical outer shell surrounds the shaft within the casing, and a flange on the outer shell is secured to the top of the casing. A cylindrical inner shell is positioned inside the outer shell, surrounding the shaft, and a space is formed between the inner shell and the outer shell. The space provides an effective thermal barrier to protect the shaft. A bearing assembly for the shaft is secured to the inner shell, and a cooler is positioned between the bearing assembly and the impeller, thereby protecting the bearing assembly from the heat of the fluid being circulated by the pump. Seals are inserted within the inner shell above the bearing assembly, and these seals confine the high-pressure liquid within the pump. <s> BIB001 </s> ALGORITHMS IN REAL ALGEBRAIC GEOMETRY: A SURVEY <s> Quantifier elimination and related problems <s> Tarski in 1948, (Tarski 1951) published a quantifier elimination method for the elementary theory of real closed fields (which he had discovered in 1930). As noted by Tarski, any quantifier elimination method for this theory also provides a decision method, which enables one to decide whether any sentence of the theory is true or false. Since many important and difficult mathematical problems can be expressed in this theory, any computationally feasible quantifier elimination algorithm would be of utmost significance. <s> BIB002 </s> ALGORITHMS IN REAL ALGEBRAIC GEOMETRY: A SURVEY <s> Quantifier elimination and related problems <s> In this paper we apply for the first time a new method for multivariate equation solving which was developed in \cite{gh1}, \cite{gh2}, \cite{gh3} for complex root determination to the {\em real} case. Our main result concerns the problem of finding at least one representative point for each connected component of a real compact and smooth hypersurface. The basic algorithm of \cite{gh1}, \cite{gh2}, \cite{gh3} yields a new method for symbolically solving zero-dimensional polynomial equation systems over the complex numbers. One feature of central importance of this algorithm is the use of a problem--adapted data type represented by the data structures arithmetic network and straight-line program (arithmetic circuit). The algorithm finds the complex solutions of any affine zero-dimensional equation system in non-uniform sequential time that is {\em polynomial} in the length of the input (given in straight--line program representation) and an adequately defined {\em geometric degree of the equation system}. Replacing the notion of geometric degree of the given polynomial equation system by a suitably defined {\em real (or complex) degree} of certain polar varieties associated to the input equation of the real hypersurface under consideration, we are able to find for each connected component of the hypersurface a representative point (this point will be given in a suitable encoding). The input equation is supposed to be given by a straight-line program and the (sequential time) complexity of the algorithm is polynomial in the input length and the degree of the polar varieties mentioned above. <s> BIB003 </s> ALGORITHMS IN REAL ALGEBRAIC GEOMETRY: A SURVEY <s> Quantifier elimination and related problems <s> By a decision method for a class K of sentence (or other expressions) is meant a method by means of which, given any sentence θ, one can always decide in a finite number of steps whether θ is in K; by a decision problem for a class K we mean the problem of finding a decision method for K. A decision method must be like a recipe, which tells one what to do at each steps so that no intelligence is required to follow it; and the method can be applied by anyone so long as he is able to read and follow directions. <s> BIB004 </s> ALGORITHMS IN REAL ALGEBRAIC GEOMETRY: A SURVEY <s> Quantifier elimination and related problems <s> Algebraically Closed Fields.- Real Closed Fields.- Semi-Algebraic Sets.- Algebra.- Decomposition of Semi-Algebraic Sets.- Elements of Topology.- Quantitative Semi-algebraic Geometry.- Complexity of Basic Algorithms.- Cauchy Index and Applications.- Real Roots.- Cylindrical Decomposition Algorithm.- Polynomial System Solving.- Existential Theory of the Reals.- Quantifier Elimination.- Computing Roadmaps and Connected Components of Algebraic Sets.- Computing Roadmaps and Connected Components of Semi-algebraic Sets. <s> BIB005
We begin appropriately with the first algorithm (in the modern sense) in real algebraic geometry which is a starting point of the subject. 2.1. The Tarski-Seidenberg Theorem and effective quantifier elimination. , and Φ(Y ) a first-order formula given by where is a block of k i variables with 1≤i≤ω k i = k, and F (P 1 , . . . , P s ) is a quantifier-free Boolean formula with atomic predicates of the form sign( . . , X BIB003 )) = σ where σ ∈ {0, 1, −1}. (Letting Π denote the partition of the blocks of variables X 1 , . . . , X k into the ω blocks of sizes k 1 , . . . , k ω , we call a formula such as Φ, having the block structure specified by Π to be a (P, Π)-formula.) The Tarski-Seidenberg theorem states that Theorem 2.1. BIB004 There exists a quantifier-free formula, Ψ(Y ), such that for any y ∈ R , Φ(y) is true if and only if Ψ(y) is true. The quantifier elimination problem is to algorithmically construct such a formula. 2.1.1. Algorithm arising from Tarski's proof. Tarski's proof BIB004 of the existence of quantifier elimination in the theory of the reals was effective and was based on Sturm's theorem for counting real roots of polynomials in one variable with real coefficients used in a parametric way. A modern treatment of this proof can be found in BIB005 Chapter 2] . The complexity of this procedure was not formally analysed in Tarski's paper. However, the algorithm eliminates one variable at a time using a parametrized version of Euclidean remainder sequence, and as a result the number and degrees of the polynomials in the remaining variables grow rather fast, and it is not possible to bound the complexity of the algorithm by any function which is a tower of exponents (in the input parameters) of a fixed height, which implies that the complexity of Tarski's algorithm is not elementary recursive. An elementary recursive algorithm for the General Decision Problem was found later by Monk  . 2.1.2. Cylindrical Algebraic Decomposition. One fundamental technique for computing topological invariants of semi-algebraic sets is through Cylindrical Algebraic Decomposition. Even though the mathematical ideas behind cylindrical algebraic decomposition were known before (see for example BIB001 ), Collins BIB002 BIB002 was the first to apply cylindrical algebraic decomposition in the setting of algorithmic semialgebraic geometry. Schwartz and Sharir  realized its importance in trying to solve the motion planning problem in robotics, as well as computing topological properties of semi-algebraic sets. Similar ideas leading to doubly exponential algorithms was also developed by Wüthrich  .