«Cylindrical Algebraic Sub-Decompositions D. J. Wilson · R. J. Bradford · J. H. Davenport · M. England Received: 22 October 2013 / Revised: 4 April ...»
Math.Comput.Sci. (2014) 8:263–288
Mathematics in Computer Science
Cylindrical Algebraic Sub-Decompositions
D. J. Wilson · R. J. Bradford ·
J. H. Davenport · M. England
Received: 22 October 2013 / Revised: 4 April 2014 / Accepted: 13 April 2014 / Published online: 13 June 2014
© The Author(s) 2014. This article is published with open access at Springerlink.com
Cylindrical algebraic decompositions (CADs) are a key tool in real algebraic geometry, used primarily for eliminating quantiﬁers over the reals and studying semi-algebraic sets. In this paper we introduce cylindrical algebraic sub-decompositions (sub-CADs), which are subsets of CADs containing all the information needed to specify a solution for a given problem. We deﬁne two new types of sub-CAD: variety sub-CADs which are those cells in a CAD lying on a designated variety; and layered sub-CADs which have only those cells of dimension higher than a speciﬁed value. We present algorithms to produce these and describe how the two approaches may be combined with each other and the recent theory of truth-table invariant CAD. We give a complexity analysis showing that these techniques can offer substantial theoretical savings, which is supported by experimentation using an implementation in Maple.
Keywords Cylindrical algebraic decomposition · Real algebraic geometry · Equational constraints · Symbolic computation · Computer algebra Mathematics Subject Classiﬁcation (2010) 68W30 (Symbolic Computation and Algebraic Computation) D. J. Wilson · R. J. Bradford · J. H. Davenport · M. England (B) Department of Computer Science, University of Bath, Bath BA2 7AY, UK e-mail: M.England@bath.ac.uk D. J. Wilson e-mail: D.J.Wilson@bath.ac.uk R. J. Bradford e-mail: R.J.Bradford@bath.ac.uk J. H. Davenport e-mail: J.H.Davenport@bath.ac.uk 264 D. J. Wilson et al.
1.1 Motivation A cylindrical algebraic decomposition (CAD) is a decomposition of Rn into cells arranged cylindrically (meaning the projections of any pair of cells onto the ﬁrst k coordinates are either equal or disjoint) each of which is a semialgebraic set (and so may be described by polynomial relations). They are traditionally produced sign-invariant with respect to a list of polynomials meaning each polynomial has constant sign on each cell. CAD was introduced by Collins , and has become a key tool in real algebraic geometry for studying semi-algebraic sets and eliminating quantiﬁers over the reals. Other applications include robot motion planning , parametric optimisation , epidemic modelling , theorem proving  and programming with complex functions .
CAD usually produces far more information than required to solve the underlying problem. Often a problem will be represented by a formula and we thus require a CAD such that the formula has constant truth value on each cell.
This can be achieved by building a CAD sign-invariant for the polynomials in the formula, but that may introduce cell divisions not relevant to the formula itself. Many techniques have been developed to try and mitigate this, some of which we discuss later. However, even then algorithms may produce thousands of superﬂuous cells which are not part of the solution set. The key focus of this paper is the development of methods to return a subset of a CAD sufﬁcient to solve a given problem. We show that such subsets can often be identiﬁed from the structure of the problem, motivating the following new deﬁnitions.
Deﬁnition 1 Let D be a CAD of Rn (represented as a set of cells). Then a subset E ⊆ D is a cylindrical algebraic sub-decomposition (sub-CAD).
Let F ⊂ Q[x1,..., xn ]. If D is a sign-invariant CAD for F then E is a sign-invariant sub-CAD. We deﬁne sub-CADs with other invariance properties in an analogous manner, such as truth-invariance for a Tarski formula ϕ(x1,..., xn ). If D is a truth-invariant CAD for ϕ and E contains all cells of where ϕ is satisﬁed then we say that E is a ϕ-sufﬁcient sub-CAD.
As an example of when sub-CADs may be applicable, consider quantiﬁer elimination, the original motivation for CAD. Given a quantiﬁed formula ϕ we want to derive an equivalent quantiﬁer-free formula. For a formula over the reals this is achieved by constructing a sign-invariant CAD for the polynomials in ϕ and testing the truth of ϕ at a sample point of each cell. This is sufﬁcient to draw a conclusion for the whole cell due to sign-invariance and thus an equivalent quantiﬁer free formula can be created from the algebraic description of the cells on which ϕ is true.
Such an application makes no use of the cells on which ϕ is false and so a ϕ-sufﬁcient sub-CAD is appropriate.
Of course, for a given problem we would like the smallest possible ϕ-sufﬁcient sub-CAD. It is not usually possible to pre-identify this, but we have developed techniques which restrict the output of the CAD algorithm to provide subCADs sufﬁcient for certain general classes of problems. These will offer savings on any subsequent computations on the cells (such as evaluating polynomials or formulae) and in some cases also offer substantial savings in the CAD construction itself. We will introduce these techniques and demonstrate how they can be combined with each other and additional existing CAD theory, but ﬁrst remind the reader of the necessary background theory.
1.2 Background to CAD
Collins’ original algorithm is described in . While there have been many improvements and reﬁnements to this algorithm the structure has remained largely the same. In the ﬁrst phase, projection, a projection operator is repeatedly applied to a set of polynomials, each time producing another set in one fewer variables. Together these sets contain the projection polynomials. These are then used in the second phase, lifting, to build the CAD incrementally. First R is decomposed into cells: points corresponding to the real roots of the univariate polynomials, and the open intervals deﬁned by them. Then R2 is decomposed by repeating this process over each cell using the bivariate polynomials (evaluated at a sample point). The output for each cell consists of sections (where a polynomial Cylindrical Algebraic Sub-Decompositions 265 vanishes) and sectors (the regions between). Together these form a stack over the cell, and taking the union of these stacks gives the CAD of R2. This is repeated until a CAD of Rn is produced. To conclude that the CAD is sign-invariant we need delineability. A polynomial is delineable over a cell if the portion of its zero set over that cell consists of disjoint sections. Then a set of polynomials is delineable over a cell if each is delineable and the sections of different polynomials over the cell are either identical or disjoint. The projection operator used must ensure that over each cell of a sign-invariant CAD for the projection polynomials in r variables, the polynomials in r + 1 variables are delineable.
All cells include a cell index and a sample point. The index is an n-tuple of positive integers that corresponds to the location of the cell relative to the rest of the CAD. Cells are numbered in each stack during the lifting stage (from most negative to most positive), with sectors having odd numbers and sections having even numbers. Therefore the dimension of a given cell can be easily determined from its index: simply the number of odd indices in the n-tuple.
Our algorithms in this paper will produce sub-CADs that are index-consistent, meaning a cell in a sub-CAD will have the same index as it would in the full CAD. Further, we will assume that cells are stored lexicographically by index.
Important developments to CAD include: reﬁnements to the projection operator [7,28,33], reducing the number of projection polynomials and hence cells; partial CAD , where the structure of the input formula is used to simplify the lifting stage; the theories of equational constraints and truth-table invariance [4,34] where the presence of equalities in the input further reﬁnes the projection operator; the use of certiﬁed numerics in the lifting phase [29,41]; and CAD via triangular decomposition  which constructs a decomposition of complex space and reﬁnes this to a CAD.
Constructing a CAD is doubly exponential in the number of variables . While none of the improvements described above (or introduced in this paper) circumvent this they do make a great impact on the practicality of using CAD. Note that CAD can depend heavily on the variable ordering used (from linear to doubly-exponential ). In this paper we work with polynomials in Q[x] with the variables x = x1,..., xn in ascending order (so we ﬁrst project with respect to xn and continue until we reach univariate polynomials in x1 ). The main variable of a polynomial (mvar) is the greatest variable present with respect to the ordering. Heuristics to assist with selecting a variable ordering (and other choices) were discussed in [6,23] and are equally applicable to sub-CADs.
1.3 New Contributions
In Sect. 2 we present new algorithms to produce sub-CADs, as well as surveying the literature to identify other examples of sub-CADs. To the best of our knowledge the concept of a sub-CAD has never been formalised and uniﬁed before.
We start in Sect. 2.1 by deﬁning a Variety sub-CAD (V-sub-CAD). This idea combines the ideas of: equational constraints , where the presence of an equation implied by the input formula improves the projection operator;
and partial CAD , where the logical structure of the input allows one to truncate the lifting process when the truth value can already be ascertained. We observe that if the input formula contains an equational constraint then all valid cells must lie on the variety it deﬁnes and hence it is unnecessary to produce cells not on this variety.
In Sect. 2.2 we deﬁne a Layered sub-CAD (L-sub-CAD) as the cells in a CAD of a speciﬁc dimension or higher. It has been noted previously that a problem involving only strict inequalities would require only the cells in a CAD of full-dimension [31,40]. We generalise this idea and explain when it may be of use, for example to solve problems whose solution sets are of known dimension or in applications like robot motion planning where only cells of certain dimensions are of use.
These new ideas improve the practicality of using CAD and their effect can be increased by combining them, as discussed in Sect. 3.1. For example, consider formulae of the form f = 0 ∧ ϕ where ϕ involves only strict inequalities. Then a Layered Variety sub-CAD (LV-sub-CAD) can provide the cells of full dimension on the variety and thus the generic families of solutions.
266 D. J. Wilson et al.
These new ideas may also be combined with many existing aspects of CAD theory. It is of course sensible to combine the restricted output of a variety CAD with the theory of reduced projection with respect to an equational constraint. However, it is also possible to combine with the projection operator for truth-table invariant CAD (TTICAD) recently presented in . A TTICAD is one for which each cell is truth invariant for a list of formulae, utilising equational constraints in the individual formulae to reduce the number of projection polynomials. We discuss when and how truth-table-invariant sub-CADs can be produced in Sect. 3.2. In Sect. 5.2 we examine a problem where a LV-sub-TTICAD can be used to identify almost all the solutions (the set of missing solutions has measure zero). This approach produces 88 % fewer cells than using TTICAD alone and takes seconds rather than minutes (while trying to tackle the problem with a traditional CAD is infeasible). This and two other case studies demonstrating the beneﬁt of the new algorithms are presented in Sect. 5.
In Sect. 4 we give a complexity analysis of certain sub-CADs. Although none of the new theory allows us to avoid the doubly exponential nature of CAD they do allow for improved asymptotic bounds. The improvement is n n−1 a drop in the constant term of the double exponent, and we note that 22 = O(22 ) so such savings can have a substantial effect. This is reﬂected by experimental results in Sect. 5 where substantial increases in efﬁciency due to sub-CAD technology are demonstrated.
We aim to return only those cells necessary to solve the problem at hand: a φ-sufﬁcient sub-CAD. However, trying to identify the minimal φ-sufﬁcient sub-CAD for a problem would mean essentially solving the problem itself and so we instead explain how to identify sets of valid or invalid cells during the lifting stage at minimal cost. Indeed, the two new approaches to sub-CAD we present require only simple checks on cell-dimensions (easily obtained via the cell-index). We present theory and algorithms for variety and layered sub-CADs in Sects. 2.1 and 2.2, and then in Sect. 2.3 we put our work into context by surveying the CAD literature for relevance to sub-CADs.
2.1 Variety Sub-CADs
Recall the deﬁnition of an equational constraint.
Deﬁnition 2 Let ϕ be a Tarski formula. An equational constraint is an equation, f = 0, logically implied by ϕ.
Equational constraints may be given explicitly (as in f = 0∧φ), or implicitly (as f 1 f 2 = 0 is in ( f 1 = 0∧φ1 )∨( f 2 = 0∧φ2 )). The presence of an equational constraint can be utilised in the ﬁrst projection stage by reﬁning the projection operator  and also in the ﬁnal lifting stage by reducing the amount of polynomials used to construct the stacks . If more than one equational constraint is present then further savings may be possible [13,35]. We restrict ourselves to a single equational constraint, and if multiple equational constraints are present we assume that one has been designated.
Deﬁnition 3 Let ϕ be a Tarski formula with equational constraint f = 0. A truth-invariant sub-CAD for ϕ consisting only of cells lying in the variety deﬁned by f = 0 is a Variety sub-CAD (V-sub-CAD).