Quantifier Elimination and Cylindrical Algebraic Decomposition

This chapter provides a brief introduction to the primary topic of these proceedings and some indication of the subject’s importance.

The CAD (cylindrical algebraic decomposition) method and its application to QE (quantifier elimination) for ERA (elementary real algebra) was announced by the author in 1973 at Carnegie Mellon University (Collins 1973b). In the twenty years since then several very important improvements have been made to the method which, together with a very large increase in available computational power, have made it possible to solve in seconds or minutes some interesting problems. In the following we survey these improvements and present some of these problems with their solutions.

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.

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.

Lower bounds are established on the computational complexity of the decision problem and on the inherent lengths of proofs for two classical decidable theories of logic: the first-order theory of the real numbers under addition, and Presburger arithmetic — the first-order theory of addition on the natural numbers. There is a fixed constant c > 0 such that for every (nondeterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2 ^cn steps. In the case of Presburger arithmetic, the corresponding bound is \({2^{{2^{cn}}}}\). These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized.

Given a set of r-variate integral polynomials, a cylindrical algebraic decomposition (cad) of euclidean r-space E ^r partitions E ^r into connected subsets compatible with the zeros of the polynomials. By “compatible with the zeros of the polynomials” we mean that on each subset of E ^r , each of the polynomials either vanishes everywhere or nowhere. For example, consider the bivariate polynomial

In Part I of the present paper we defined cylindrical algebraic decompositions (cad’s), and described an algorithm for cad construction. In Part II we give an algorithm that provides information about the topological structure of a cad of the plane. Informally, two disjoint cells in E ^r , r ≥ 1, are adjacent if they touch each other; formally, they are adjacent if their union is connected. In a picture of a cad, eg Fig. 2 of Part I, it is obvious to the eye which pairs of cells are adjacent. However, the cad algorithm of Part I does not actually produce this information, nor did the original version of that algorithm in (Collins 1975).

The cylindrical algebraic decomposition (CAD) of Collins (1975) provides a potentially powerful method for solving many important mathematical problems, provided that the required amount of computation can be sufficiently reduced. An important component of the CAD method is the projection operation. Given a set A of r-variate polynomials, the projection operation produces a certain set P of (r − l)-variate polynomials such that a CAD of r-dimensional space for A can be constructed from a CAD of (r − 1)-dimensional space for P. The CAD algorithm begins by applying the projection operation repeatedly, beginning with the input polynomials, until univariate polynomials are obtained. This process is called the projection phase.

Since Tarski (1951) gave the first quantifier elimination algorithm for real closed fields, various improvements and new methods have been devised and analyzed (Arnon 1981, 1988b; Ben-Or et al. 1986; Böge 1980; Buchberger and Hong 1991; Canny 1988; Cohen 1969; Collins 1975; Collins and Hong 1991; Fitchas et al. 1990a; Grigor’ev 1988; Grigor’ev and Vorobjov 1988; Heintz et al. 1989a; Holthusen 1974; Hong 1989, 1990a, 1990b, 1991a, 1991b, 1991c; Johnson 1991; Langemyr 1990; Lazard 1990; McCallum 1984; Renegar 1992a, 1992b, 1992c; Seidenberg 1954).

This paper concerns recent progress on the computational complexity of decision methods and quantifier elimination methods for the first order theory of the reals. The paper begins with a quick introduction of terminology followed by a short survey of some complexity highlights. We then discuss ideas leading to the most (theoretically) efficient algorithms known. The discussion is necessarily simplistic as a rigorous development of the algorithms forces one to consider a myriad of details.

A key component of the cylindrical algebraic decomposition (cad) algorithm is the projection (or elimination) operation: the projection of a set A of r-variate integral polynomials, where r ≥ 2 is defined to be a certain set PROJ(A) of (r − l)-variate integral polynomials. The property of the map PROJ of particular relevance to the cad algorithm is that, for any finite set A of r-variate integral polynomials, where r ≥ 2, if S is any connected subset of (r − 1)-dimensional real space ℝ^(r−1) in which every element of PROJ(A) is invariant in sign then the portion of the zero set of the product of those elements of A which do not vanish identically on S that lies in the cylinder S × ℝ over S consists of a number (possibly 0) of disjoint “layers” (or sections) over S in each of which every element of A is sign-invariant: that is, A is “delineable” on S. It follows from this property that, for any finite set A of r-variate integral polynomials, r ≥ 2, any decomposition of ℝ^(r−1) into connected regions such that every polynomial in PROJ (A) is invariant in sign throughout every region can be extended to a decomposition of ℝ ^r (consisting of the union of all of the above-mentioned layers and the regions in between successive layers, for each region of ℝ^(r−1) such that every polynomial in A is invariant in sign throughout every region of ℝ ^r .

This paper summarizes results obtained in the author’s Ph.D. thesis (Johnson 1991). Improved maximum computing time bounds are obtained for isolating the real roots of an integral polynomial. In addition to the theoretical results a systematic study was initiated comparing algorithms based on Sturm sequences, the derivative sequence, and Descartes’ rule of signs. The algorithm with the best theoretical computing time bound is the coefficient sign variation method, an algorithm based on Descartes’ rule of signs. Moreover, the coefficient sign variation method typically outperforms the other algorithms in practice; however, we exhibit classes of input polynomials for which each algorithm is superior.

The real root counting problem is one of the main computational problems in Real Algebraic Geometry. It is the following: Let \(\mathbb{D}\) be an ordered domain and \(\mathbb{B}\) a real closed field containing \(\mathbb{D}\). Find algorithms which for every P ∈ \(\mathbb{D}\) [x] compute the number of roots of P in \(\mathbb{B}\). More precisely we shall study the following problem.

Since the late eighties, the Macaulay matrix has recently received renewed attention in the field of quantifier elimination. Grigor’ev (1988) and Renegar (1992a, 1992b, 1992c) made it a central tool in their study of the complexity of quantifier elimination. They developed algorithms which have better complexities than Collins’ quantifier elimination algorithm based on the CAD (Collins 1975), but until now Collins’ CAD is much faster in practice.

In this paper, we give a new method for computing two variants of resultants, namely the trace resultants and the slope resultants. These two variants were introduced in (Hong 1993d) while devising quantifier elimination algorithms for a certain fragment of the elementary theory of the reals, where the input formulas are required to contain at least one quadratic polynomial equation. Hong (1993d) also gave a method for computing these two variant resultants. The method is based on expanding certain determinants whose entries come directly from the coefficients of the involved polynomials. In this paper, we provide a theoretical computing time analysis of the method. More importantly, we give a new and faster method, as well as modular algorithms for the computation of the variant resultants.

We consider s polynomials P₁,…,P _s in k < s variables with coefficients in an ordered domain A contained in a real closed field R, each of degree at most d. We present a new algorithm which computes a point in each connected component of each non-empty sign condition over P₁,…,P _s . The output is the set of points together with the sign condition at each point. The algorithm uses s(s/k) ^k d ^{O (k)} arithmetic operations in A. The algorithm is nearly optimal in the sense that the size of the output can be as large as s(O(sd/k)) ^k .

There are many interesting problems which can be expressed in the language of elementary algebra, or in one of its extensions, but which do not really depend on the coordinate system, and in which the variables can be restricted to an arbitrarily small neighborhood of some point. It seems that it ought to be possible to use cylindrical decomposition techniques to solve such problems, taking advantage of their special features. This article attempts to do this, but many unsolved problems remain.

The main problem in Computational Real Algebraic Geometry is the development of efficient Quantifier Elimination algorithms. It is well known (Davenport and Heintz 1988) that the general problem of quantifier elimination cannot be solved in polynomial time. Therefore the only way to attack this problem is to consider specific cases where efficient algorithms can be applied. By efficient we do not mean “polynomial time”. Instead we are looking for algorithms, methods and criteria that can be used to solve specific quantifier elimination problems involving low degree polynomials in a reasonable amount of time. This strategy has already been investigated by Hong (1993d) for formulas with quadratic polynomial constraints and by Heintz, Roy, and Solernó (1993) for specific inputs for which the general Quantifier Elimination algorithm presented in (Heintz et al. 1990) is efficient.

Quantifier elimination for the elementary formal theory of real numbers is a fascinating area of research at the intersection of various field of mathematics and computer science, such as mathematical logic, commutative algebra and algebraic geometry, computer algebra, computational geometry and complexity theory. Originally the method of quantifier elimination was invented (among others by Th. Skolem) in mathematical logic as a technical tool for solving the decision problem for a formalized mathematical theory. For the elementary formal theory of real numbers (or more accurately of real closed fields) such a quantifier elimination procedure was established in the 1930s by A. Tarski, using an extension of Sturm’s theorem of the 1830s for counting the number of real zeros of a univariate polynomial in a given interval. Since then an abundance of new decision and quantifier elimination methods for this theory with variations and optimizations has been published with the aim both of establishing the theoretical complexity of the problem and of finding methods that are of practical importance (see Arnon 1988a and the discussion and references in Renegar 1992a, 1992b, 1992c for a comparison of these methods). For sub-problems such as elimination of quantifiers with respect to variables, that are linearly or quadratically restricted, specialized methods have been developed with good success (see Weispfenning 1988; Loos and Weispfenning 1993; Hong 1992d; Weispfenning 1997).