CAD Adjacency Computation Using Validated Numerics
Adam Strzebonski

TL;DR
This paper introduces an algorithm that computes cell adjacencies in cylindrical algebraic decomposition using validated numerics, enabling efficient topological analysis and applications like visualization and path planning.
Contribution
The paper presents a novel validated numerics-based algorithm for cell adjacency computation in CAD, achieving efficiency comparable to CAD construction without adjacency info.
Findings
Algorithm successfully computes cell adjacencies in CAD.
Implementation demonstrates practical efficiency.
Empirical data supports effectiveness of the method.
Abstract
We present an algorithm for computation of cell adjacencies for well-based cylindrical algebraic decomposition. Cell adjacency information can be used to compute topological operations e.g. closure, boundary, connected components, and topological properties e.g. homology groups. Other applications include visualization and path planning. Our algorithm determines cell adjacency information using validated numerical methods similar to those used in CAD construction, thus computing CAD with adjacency information in time comparable to that of computing CAD without adjacency information. We report on implementation of the algorithm and present empirical data.
| Ex # | |||||||
|---|---|---|---|---|---|---|---|
| Ex # | |||||||
|---|---|---|---|---|---|---|---|
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Numerical Analysis Techniques · Computational Geometry and Mesh Generation · Polynomial and algebraic computation
CAD Adjacency Computation Using Validated Numerics
Adam Strzeboński
Wolfram Research Inc., 100 Trade Centre Drive, Champaign, IL 61820, U.S.A.
(Date: April 21, 2017)
Abstract.
We present an algorithm for computation of cell adjacencies for well-based cylindrical algebraic decomposition. Cell adjacency information can be used to compute topological operations e.g. closure, boundary, connected components, and topological properties e.g. homology groups. Other applications include visualization and path planning. Our algorithm determines cell adjacency information using validated numerical methods similar to those used in CAD construction, thus computing CAD with adjacency information in time comparable to that of computing CAD without adjacency information. We report on implementation of the algorithm and present empirical data.
1. Introduction
A semialgebraic set is a subset of which is a solution set of a system of polynomial equations and inequalities. Computation with semialgebraic sets is one of the core subjects in computer algebra and real algebraic geometry. A variety of algorithms have been developed for real system solving, satisfiability checking, quantifier elimination, optimization and other basic problems concerning semialgebraic sets [7, 3, 5, 9, 10, 11, 13, 19, 24, 25]. Every semialgebraic set can be represented as a finite union of disjoint cells bounded by graphs of semialgebraic functions. The Cylindrical Algebraic Decomposition (CAD) algorithm [7, 5, 21] can be used to compute a cell decomposition of any semialgebraic set presented by a quantified system of polynomial equations and inequalities. Alternative methods of computing cell decompositions are given in [6, 22, 23]. For solving certain problems, for instance computing topological properties or visualization, it is not sufficient to know a cell decomposition of the set, but it is also necessary to know how the cells are connected together.
Example 1**.**
The CAD algorithm applied to the equation gives four one-dimensional cells and three zero-dimensional cells shown in Figure 1.1. To find the connected components of the solution set it is sufficient to know which one-dimensional cells are adjacent to which zero-dimensional cells.
Several algorithms for computing cell adjacencies have been developed. The algorithm given in [20] computes cell adjacencies for CAD that are well-based. A CAD is well-based if none of the polynomials whose roots appear in cell description vanishes identically at any point. This is a somewhat stronger condition than well-orientedness required for the McCallum projection [15], nevertheless a large portion of examples that appear in practice satisfies the condition. In a well-based CAD all cell adjacencies can be determined from adjacencies between cells whose dimensions differ by one. In all CADs are well-based. Algorithm for computing cell adjacencies in arbitrary CADs in has been given in [1]. For determining cell adjacencies [20] proposes methods based on fractional power series representations of polynomial roots. Another method, given in [16], computes adjacencies between a zero-dimensional cell and one-dimensional cells by analyzing intersections of the one dimensional cells with sides of a suitable box around the zero-dimensional cell. For an alternative method of computing connectivity properties of semialgebraic sets see [4, 2, 3, 8].
In this paper we present a new algorithm which computes cell adjacencies for well-based CAD. The algorithm uses validated numerical methods similar to those used in [21] for construction of CAD cell sample points. The method is based on computation of approximations of polynomial roots and increasing the precision of computations until validation criteria are satisfied. Unlike the previously known algorithms, it does not require polynomial computations over algebraic number fields or computation with fractional power series representations of polynomial roots. Also, unlike the CAD construction algorithm given in [21], the algorithm never needs to revert to exact algebraic number computations. We have implemented the algorithm as an extension to the CAD implementation in Mathematica. Empirical results show that computation of CAD with cell adjacency data takes time comparable to computation of CAD without cell adjacency data.
The general idea of the algorithm is as follows. It starts, similarly as the CAD algorithm, with computing a sample point in each cell in for all . The sample point of a cell in extends the sample point of the projection of the cell on . Then for each pair of adjacent CAD cells and in with the algorithm constructs a point that is “sufficiently close” to the sample point of . Here “sufficiently close” means that computing approximations of roots of projection polynomials at and is sufficient to identify which roots over tend to which roots over and to continue the construction to pairs of adjacent CAD cells in . The construction gives all pairs of adjacent cells in whose dimensions differ by one. For well-based CAD this is sufficient to determine all cell adjacencies.
2. Preliminaries
A system of polynomial equations and inequalities in variables is a formula
[TABLE]
where , and each is one of or .
A subset of is semialgebraic if it is a solution set of a system of polynomial equations and inequalities.
A quantified system of real polynomial equations and inequalities in free variables and quantified variables is a formula
[TABLE]
Where is or , and is a system of real polynomial equations and inequalities in .
By Tarski’s theorem (see [24]), solution sets of quantified systems of real polynomial equations and inequalities are semialgebraic.
Notation 2**.**
For , let denote a -tuple of real numbers and let denote a -tuple of variables.
Every semialgebraic set can be represented as a finite union of disjoint cells (see [12]), defined recursively as follows.
- (1)
A cell in is a point or an open interval. 2. (2)
A cell in has one of the two forms
[TABLE]
where is a cell in , is a continuous semialgebraic function, and and are continuous semialgebraic functions, , or , and on .
For a cell let , for , denote the projection of on . A finite collection of cells in is cylindrically arranged if for any and any and are either disjoint or identical.
A *cylindrical algebraic decomposition (CAD) of *is a finite collection of pairwise disjoint cylindrically arranged cells in such that .
Let be a finite set of polynomials. A CAD of* *is *P-invariant *if each element of has a constant sign on each cell of .
Let * be a semialgebraic set. A CAD of *is consistent with if for some .
Let . and are adjacent if and is connected.
For a semialgebraic set presented by a quantified system of polynomial equations and inequalities (2.1), the CAD algorithm can be used to find a CAD of consistent with . The CAD is represented by a cylindrical algebraic formula (CAF). A CAF describes each cell by giving explicit semialgebraic function bounds and the Boolean structure of a CAF reflects the cylindrical arrangement of cells. Before we give a formal definition of a CAF, let us first introduce some terminology.
Let and let , where . A semialgebraic function given by the defining polynomial and a root number is the function
[TABLE]
where is the -th real root of . The function is defined for those values of for which has at least real roots. The real roots are ordered by the increasing value and counted with multiplicities. A real algebraic number given by a defining polynomial and a root number is the -th real root of .
Let be a connected subset of . The function is* regular* on if it is continuous on , for all , and there exists* * such that for any is a root of of multiplicity .
The polynomial is degree-invariant on if there exists* * such that for all .
A set of polynomials is delineable on if all elements of are degree-invariant on and for
[TABLE]
where are disjoint regular semialgebraic functions and for and are either disjoint or equal. Functions are root functions of over .
Let be delineable on , let be all root functions of elements of over , and let and . For , the -th -section over is the set
[TABLE]
For , the -th -sector over is the set
[TABLE]
-stack over is the set of all -sections and -sectors over .
A formula is an algebraic constraint with bounds if it is a level- equational or inequality constraint with defined as follows.* *
- (1)
A level- equational constraint has the form , where is a real algebraic number, and . 2. (2)
A level- inequality constraint has the form , where and are real algebraic numbers, , or , and . 3. (3)
A level- equational constraint has the form , where is a semialgebraic function, and . 4. (4)
A level- inequality constraint has the form , where and are semialgebraic functions, , or , and .
A level- algebraic constraint is regular on a connected set if all elements of are regular on and, if is an inequality constraint, on .
Definition 3**.**
An atomic cylindrical algebraic formula (CAF) in has the form , where is a level- algebraic constraint for and is regular on the solution set of for .
Level- cylindrical formulas* in are defined recursively as follows*
- (1)
A level-* cylindrical formula is or a disjunction of level- algebraic constraints.* 2. (2)
A level-* cylindrical formula, with , is or has the form*
[TABLE]
where are level-* algebraic constraints and are level- cylindrical formulas.*
A cylindrical algebraic formula (CAF) is a level- cylindrical formula such that distributing conjunction over disjunction in gives
[TABLE]
*where each is an atomic CAF. Let denote the solution set of and let . The *bound polynomials of is a finite set which consists of all polynomials such that for some and a level- algebraic constraint that appears in .
Note that is a cell and is a finite collection of pairwise disjoint cylindrically arranged cells.
For a CAF in , let denote the CAF in obtained from by removing all level- subformulas. Then
[TABLE]
Following the terminology of [20], we define a well-based CAF as follows.
Definition 4**.**
A CAF is well-based if * is a -invariant CAD of and for any if then for any is not identically zero.*
In a CAD corresponding to a well-based CAF a closure of a cell is a union of cells and the only cells from other stacks adjacent to a given section are sections defined by the same polynomial. Moreover, any two adjacent cells have different dimensions and are connected through a chain of adjacent cells with dimensions increasing by one, and hence to determine all cell adjacencies it is sufficient to find all pairs of adjacent cells whose dimensions differ by one. These properties, stated precisely in Proposition 5, are essential for our algorithm.
Proposition 5**.**
Let be a well-based CAF.
- (1)
If then there exits cells such that . 2. (2)
Let be a section
[TABLE]
and let be a cell adjacent to with . Then either is equal to a section
[TABLE]
for some , or for any
[TABLE]
or for any
[TABLE] 3. (3)
Let be adjacent cells such that and . Then and if then there exist cells such that and for .
Proof.
Part is Lemma 1 of [20]. To prove first note that, by , . By Lemma 2 of [20], there exists a unique continuous function extending . Moreover, is either infinite or a root of . Since is delineable on and is connected, either is a root of on , or on , or on .
We will prove by induction on . Note that by it is sufficient to find cells such that and and are adjacent for . If then dimensions of any pair of adjacent cells differ by one, hence is true. To prove for we will use induction on . If then is true. Suppose . Let and , where and . If is a section, then, by Lemma 2 of [20], there exists a continuous function such that and is infinite or a root of an element of . In this case set . Similarly, if is a sector, then, by Lemma 2 of [20], there exists continuous functions such that and and are infinite or roots of elements of . Since , . Suppose first that . Since , is a section and is a sector. If , where or , then is finite on , is adjacent to , and is adjacent to . Since , is true. Otherwise, let be the sector directly below . Then , and hence is adjacent to . Again, since , is true. Now suppose that . is well-based, hence, by the inductive hypothesis on , there exist cells such that and for . Let and . Then . Since is adjacent to , there exist a sequence such that and . Put . Then . The set
[TABLE]
is a union of a finite number of cells, , and . Hence, there exists a cell such that contains infinitely many elements of the sequence . Therefore, is adjacent to both and . Since and , is true by the inductive hypothesis on . ∎
For a given semialgebraic set a well-based CAF such that is consistent with may not exist in a given system of coordinates. However, as shown in [20], there always exists a linear change of variables after which a well-based CAF such that is consistent with does exist.
Example 6**.**
If is the real solution set of then a well-based CAF such that is consistent with does not exist for any order of variables. A CAD computed using McCallum’s projection operator [14] includes cells
[TABLE]
* is not a union of cells, since , and section is adjacent to a sector from a different stack. After the linear change of variables is transformed to the solution set of . The following CAF is well-based and is consistent with the transformed .*
[TABLE]
where
[TABLE]
3. Root isolation algorithms
In this section we describe root isolation algorithms we will use in the algorithm computing cell adjacencies. Let us first introduce some notations and subalgorithms.
Let denote a disk in the complex plane, let denote the set of dyadic rational numbers, and let denote the set of discs in the complex plane with dyadic Gaussian rational centers and dyadic rational radii. For a disc , let and denote the center and the radius of , let and denote the minimum and maximum of absolute values of elements of , let denote the disc that consists of complex conjugates of elements of , and let and . When we refer to interval arithmetic operations we mean circular complex interval (disc) arithmetic (see e.g. [18]).
Proposition 7**.**
There exists an algorithm (ApproximateRoots) that takes as input a polynomial
[TABLE]
and and outputs such that for any polynomial
[TABLE]
and any there exits such that if and, for all ,
[TABLE]
then, after a suitable reordering of roots, for all .
Proof.
The algorithm described in [17] satisfies Proposition 7. ∎
Let us now describe a subalgorithm computing roots of polynomials with complex disc coefficients. The algorithm is based on the following proposition ([21], Proposition 4.1).
Proposition 8**.**
Let be a polynomial of degree , , , and let . Suppose that
[TABLE]
Then has exactly roots, multiplicities counted, in the disc .
The following is an extended version of Algorithm 4.2 from [21]. The key difference is that this version does not assume that the leading coefficient does not contain zero and provides a lower bound on the absolute value of roots that tend to infinity when the leading coefficients that contain zero vanish.
Algorithm 9**.**
*(IntervalRoots)
Input: .
Output: , positive integers , and a positive radius , such that for any and any the polynomial has exactly roots in the disc , multiplicities counted, and has no roots in . Moreover, for any , , and . The other possible output is .*
- (1)
If for all return . Otherwise let be the maximal such that . 2. (2)
Put
[TABLE]
If
[TABLE]
return . 3. (3)
Set , where for , and set
[TABLE] 4. (4)
Compute . 5. (5)
Let . For each and use complex disc arithmetic to compute . 6. (6)
For each let be the smallest such that and
[TABLE]
If there is no satisfying the condition return . 7. (7)
Find the connected components of the union of . Let be the sets of indices corresponding to the connected components. 8. (8)
For each , let . If for some return . Otherwise pick with the minimal value of , and set . 9. (9)
If for some return . 10. (10)
Return , , and .
To show correctness of Algorithm 9, suppose that the algorithm returned , , and . Let and . By Proposition 8, and because the algorithm did not fail in step , has exactly roots in . The condition in step and Proposition 8 imply that has exactly roots in the disc . Since the algorithm did not fail in step , , and hence has no roots in . Step guarantees that for any , . Step ensures that .
Computation of sample points in CAD cells requires a representation of vectors with algebraic number coordinates. The following gives a recursive definition of root isolation data and of representation of real algebraic vectors. Note that root isolation data provides information about roots of not only at , but also in a neighbourhood of (point of the definition). This property is crucial for computing cell adjacencies.
Definition 10**.**
* is root isolation data for at if*
- (1)
, , and , 2. (2)
* has a root of multiplicity in , for , and has no other roots,* 3. (3)
for any , 4. (4)
for any and if then , 5. (5)
if is the isolating disc of for , and then has exactly roots in , multiplicities counted, and has no roots in .
A real algebraic vector is represented by
[TABLE]
where
- •
* represents the real algebraic vector ,*
- •
* is a defining polynomial of ,*
- •
* is an isolating disc of ,*
- •
* is** root isolation data for at , for some , and .*
Define .
To complete the recursive definition let be the representation of the only element of .
We will say that is a refinement of if , ,* and for , and is a refinement of .*
For any and , we will use notation and .
Remark 11**.**
A refinement of a refinement of is a refinement of .
Proof.
With notations from Definition 10, let
[TABLE]
and**
[TABLE]
By induction, it suffices to show and for . follows from and .* * and implies that , and contain the same root of . Then * implies *. ∎
The algorithms we introduce next take a working precision argument. A working precision is a positive integer. One can think of it as the number of bits in floating-point numbers used in a numeric approximation algorithm. However, we will not attach any specific meaning to the working precision argument. Instead our algorithms will satisfy certain properties as tends to infinity. For instance, if we say that a certain quantity in the output of an algorithm tends to zero as tends to infinity, it means that for any there exists such that if the working precision then the algorithm will produce an output with .
Let be a real algebraic vector and let
[TABLE]
be such that does not vanish identically. We will now describe an algorithm , with , which finds the root isolation data of at and the real roots of . The algorithm uses two subalgorithms and that will be defined recursively in terms of . Given
[TABLE]
and a working precision computes a refinement of such that as tends to infinity tends to zero. decides whether is zero for a given .
Algorithm 12**.**
*()
Input: Real algebraic vector , where , , such that does not vanish identically, and a working precision .
Output: Root isolation data of at , a refinement of , and real algebraic vectors such that , for , are all the real roots of , and as tends to infinity tends to zero.*
- (1)
Let . Find such that and
[TABLE]
using if . Set . 2. (2)
Compute the principal subresultant coefficients of and with respect to . 3. (3)
Find the largest integer such that
[TABLE]
using if . 4. (4)
Set and . 5. (5)
If compute and let be the isolating discs of in . 6. (6)
For
- (a)
if compute such that and , 2. (b)
else compute using interval arithmetic. 7. (7)
Compute . 8. (8)
If double and go to step . 9. (9)
Let . If or the conditions and of Definition 10 are not satisfied, double and go to step . 10. (10)
Let be the set of indices for which . For let and . 11. (11)
Return , , and .
Proof.
To prove termination of the Algorithm 12 we need to show that for sufficiently large the call to IntervalRoots in step succeeds and gives a result with . The specification of the algorithm implies that as tends to infinity tends to zero. Hence also tends to zero. Therefore, as tends to infinity, tends to and and tend to for all . In particular, for sufficiently large , iff , and hence in step of IntervalRoots is the same as computed in step of Algorithm 12. Since
[TABLE]
tends to infinity and
[TABLE]
tends to a finite constant, the call to IntervalRoots does not fail in in step for sufficiently large . Let be the roots of , each repeated as many times as its multiplicity. Let be the roots computed in step of IntervalRoots. The specification of ApproximateRoots implies that, as tends to infinity, after a suitable reordering of roots, tends to for each . Hence for computed in step of IntervalRoots tends to and tends to zero. Therefore, and tend to . Hence, if is the multiplicity of ,
[TABLE]
tends to zero and
[TABLE]
is bounded away from zero for sufficiently large . Therefore, for sufficiently large , the condition in step of IntervalRoots is satisfied by . Note that if is closer to than to other roots of then the condition cannot be satisfied by any . Otherwise, by Proposition 8, would have exactly roots in which is impossible since if then contains no roots of and else contains at least roots of . Hence, for sufficiently large , step does not fail and for each. Since tends to zero for , for sufficiently large , and intersect iff , and hence step of IntervalRoots does not fail. Since tends to infinity, for sufficiently large , step of IntervalRoots does not fail and the whole algorithm succeeds. Since, for sufficiently large , the discs returned by IntervalRoots correspond to distinct roots of , in step of Algorithm 12. Since tends to zero for and tends to infinity, for sufficiently large , we have for any and
[TABLE]
Therefore for any and if is the root of in then either and or and . Hence for sufficiently large , the conditions and of Definition 10 are satisfied and the algorithm terminates.
Proposition 4.3 of [21] and correctness of Algorithm 9 imply that satisfy the conditions , , and of Definition 10, and the conditions and are ensured by step of Algorithm 12. Step selects all isolating discs that intersect the real line, hence are all the real roots of .
To show that tends to zero as tends to infinity, note that , we have already shown that tends to zero for as tends to infinity, and since is computed by with working precision , tends to zero as tends to infinity. ∎
Remark 13**.**
If in step of Algorithm 12 then
[TABLE]
does not have multiple roots and computing the principal subresultant coefficients is not necessary. Hence instead of computing the principal subresultant coefficients in step it is sufficient to compute them only when the algorithm reaches step for the first time and .
To complete the description of Algorithm 12 let us now define the subalgorithms and .
Algorithm 14**.**
*()
Input: Real algebraic vector , where , and a working precision .
Output: A refinement of such that as tends to infinity tends to zero.*
- (1)
Let ,
[TABLE]
and . Set and . 2. (2)
Compute
[TABLE]
where . 3. (3)
If no reordering of indices in yields* and for , double and go to .* 4. (4)
Let be such that the isolating disk of is . Return .
Since tends to zero as tends to infinity, for sufficiently large the condition in step is satisfied for pairs and containing the same root of , and hence the algorithm terminates. Correctness of Algorithm 12 and the condition in step guarantee that is a refinement of and as tends to infinity tends to zero.
Algorithm 15**.**
*()
Input: Real algebraic vector , where , and .
Output: if and otherwise.*
- (1)
Let ,
[TABLE]
and . Set , , and set an initial value of working precision (e.g. to precision that was used to compute ). 2. (2)
Compute . Let . Set . 3. (3)
Compute . 4. (4)
If intersects the isolating disc of for more than one , double and go to step . 5. (5)
Let be the only index for which intersects the isolating disc of . Let , and . 6. (6)
If return otherwise return .
Since as tends to infinity, and tend to zero, for sufficiently large , intersects only the isolating disc of , which proves termination and correctness of the algorithm.
Since is defined for and and are defined for , the recursive definition of the algorithms is complete.
Remark 16**.**
* is defined here in terms of for simplicity of description. In practice, to decide whether*
[TABLE]
we can first evaluate at the isolating discs of using interval arithmetic. If the result does not contain zero then
[TABLE]
Otherwise, we isolate roots of
[TABLE]
and refine isolating discs of roots of
[TABLE]
and roots of until either the isolating disc of does not intersect any isolating discs of roots of or the number of intersecting isolating discs of roots of and agrees with the number of common roots of and computed by finding signs of principal subresultant coefficients of and (see Proposition 4.4 of [21]). When the algorithm is used in CAD construction we also use information about polynomials that are zero at the current point that was collected during the construction (see [21], Section 4.1).
4. Finding cell adjacencies
Let be a well-based CAF in . For simplicity let us assume that , where
[TABLE]
This can be always achieved by multiplying all elements of
[TABLE]
We can also assume that are square-free.
The main algorithm CADAdjacency (Algorithm 18) finds all pairs of adjacent cells such that . By Proposition 5, to determine all cell adjacencies for a well-based CAF it is sufficient to find all pairs of adjacent cells whose dimensions differ by one, hence Algorithm 18 is sufficient to fully solve the cell adjacency problem for well-based CAF.
The algorithm first calls SamplePoints (Algorithm 19), which constructs a sample point in each cell , for , and computes root isolation data for each cell , for . Let us describe the representation of sample points and give the specification of root isolation data. Let be the set of indices such that is a section. For , is a rational number and for , is an algebraic number. To represent sample points we will use combinations of rational vectors and algebraic vectors defined as follows. Let , let , let , where , and let , where . Let be a real algebraic vector and let be a rational vector. By we denote the point such that for and for . Suppose and . Let denote with replaced by for . Then computed by SamplePoints is root isolation data of at .
Next CADAdjacency calls AdjacencyPoints (Algorithm 20) which, for , and for each pair of adjacent cells of with , constructs a point which satisfies the following condition.
Condition 17**.**
If and then
- •
for each if is a root of with isolating disc then ,
- •
if is a rational number between roots of then .
Finally, CADAdjacency returns the pairs of cells for which is defined.
Algorithm 18**.**
*(CADAdjacency)
Input: A well-based CAF in with , where .
Output: The set of all pairs of adjacent cells such that .*
- (1)
Compute . 2. (2)
Compute . 3. (3)
Return the set of all pairs of cells such that is defined.
Algorithm 19**.**
*(SamplePoints)
Input: A well-based CAF in with , where .
Output: and such that*
- •
for and for each cell of , is a sample point in ,
- •
for and for each cell of , is root isolation data for .
- (1)
Set an initial value of working precision. 2. (2)
Compute . We have
[TABLE] 3. (3)
Pick rational numbers such that . 4. (4)
For , let be the -th -section. Set . 5. (5)
For , let be the -th -sector. Set . 6. (6)
For and for each cell of :
- (a)
Let . 2. (b)
Let , , and let be with replaced by for . 3. (c)
Compute . We have
[TABLE] 4. (d)
Set and replace representations of algebraic vectors in for with their refinements that appear in . 5. (e)
Pick rational numbers such that , and let for . 6. (f)
For , let be the -th -section over . Set
[TABLE] 7. (g)
For , let be the -th -sector over . Set
[TABLE] 7. (7)
Return and .
Algorithm 20**.**
*(AdjacencyPoints)
Input: A well-based CAF in with , where , and as in the output of Algorithm 19.
Output: such that for and for each pair of adjacent cells of with , is a point in satisfying Condition 17.*
- (1)
Let be the number of real roots of . For :
- (a)
Let be the -sector. 2. (b)
If let be the -st -section. We have , , and . Let and . Set . 3. (c)
If let be the -th -section. We have
[TABLE]
, and
[TABLE]
Let and . Set . 2. (2)
For and for each non-zero-dimensional cell of :
- (a)
Let and let be the number of real roots of over . For :
- (i)
Let be the -sector over . 2. (ii)
If let be the -st -section over . We have , , and . Let and . Set , where . 3. (iii)
If let be the -th -section over . We have , , and . Let and . Set
[TABLE]
where . 2. (b)
For each cell of adjacent to and such that :
- (i)
Let and let
[TABLE] 2. (ii)
Let be the-sections over , and let be the isolating disc of for . 3. (iii)
Let , , and let be with replaced by for . 4. (iv)
Compute . 5. (v)
For refine the isolating disc of until it is contained in one of or . Let be the -th -section over . If , set , and set . Otherwise if set else set . 6. (vi)
Set and . 7. (vii)
For , let be the -th -sector over . For each -sector over that lies between and put and set . 3. (3)
Return .
Proof.
Let us now prove correctness of Algorithm 18. The working precision set in step of SamplePoints is used in calls to AlgRoots. Since AlgRoots raises precision as needed to reach its goals, is just an initial value and can be set arbitrarily e.g. to the number of bits in a double precision number. Steps - construct sample points is all cells of , starting with sample points in cells of , and then extending them to sample points in one coordinate at a time. An important fact to note is that isolating discs in the representations of already constructed sample points may change during the execution of step . Namely, in step the isolating discs of the coordinates of the sample points for all projections of the cell are replaced with their refinements that were computed in the process of isolating the roots of . In particular, for any cell if then for any and the isolating discs that appear in the representations of any algebraic coordinate in and in are equal. Note however, that after SamplePoints is finished the representations of are fixed.
In step of AdjacencyPoints for each pair of adjacent cells of with the algorithm constructs a point
[TABLE]
such that if and is the isolating disc of then . At the start of each iteration of the loop in step the algorithm has already constructed a point for each pair of adjacent cells of with . The points satisfy Condition 17. Steps and construct points for each pair of adjacent cells of with . It is clear that the constructed points satisfy Condition 17. What we need to show is that the construction will always succeed, pairs of cells for which is constructed are adjacent, and is constructed for every pair of adjacent cells of with . Step constructs for every pair of adjacent cells from a stack over the same cell . Note that in step we have and consists of two intervals, one on each side of , hence we can pick rational numbers with or . If cells and from stacks over different cells and are adjacent and then and must be adjacent and, by Proposition 5, and is a section iff is a section. This shows that step constructs for every pair of adjacent cells of with .
Let us prove that the construction in step will always succeed and pairs of cells for which is constructed are adjacent. With notation of step , let
[TABLE]
and
[TABLE]
Note that and for . Let be with replaced by for . Then is equal to with replaced by for . For let be the isolating disk of in and let be the isolating disk of in the representation of with which was computed. Note that, by Remark 11, the current representation of is a refinement of the representation with which was computed, hence . Hence, and . By the condition of Definition 10, for each either belongs to one of or . Therefore we can refine the isolating disc of so that it is contained in one of or . In the former case the -th -section over is adjacent to the -th -section over , in the latter case the -th -section over tends to infinity whose sign is determined by the sign of . This shows that sections for which is constructed are adjacent. Finally, let and be sectors over and defined in step . Then, by construction in step of SamplePoints, , and since (possibly after reordering of indices), . Moreover, . Since for each either belongs to one of or , the point defined in step belongs to . If is constructed in step then is a sector that lies between sections adjacent to the sections bounding , hence and are adjacent. ∎
5. Empirical Results
An algorithm computing CAD cell adjacencies has been implemented in C, as a part of the kernel of Mathematica. The implementation takes a quantified system of polynomial equations and inequalities and uses Mathematica multi-algorithm implementation of CAD to compute a CAF such that is a CAD of consistent with the solution set of . If is well-based the implementation uses Algorithm 20 to find the cell adjacencies. The implementation is geared towards solving a specified topological problem, e.g. finding the boundary or the connected components of , hence it avoids computing cell adjacencies for cells that are known not to belong to the closure of . The current implementation also works for non-well-based problems in using ideas from [1] to extend Algorithm 20.
The experiments have been conducted on a Linux laptop with a -core GHz Intel Core i7 processor and GB of RAM. The reported CPU time is a total from all cores used. For each example we give three timings. is the computation time of constructing a CAF consistent with the solution set the input system. is the time of refining the CAD to a -invariant CAD of and of constructing sample points in the CAD cells (steps - of Algorithm 20). Our implementation refines the CAD while constructing sample points, which is why we cannot give separate timings. The third timing, is the time of computing cell adjacency information (steps - of Algorithm 20). We also report the dimension of the embedding space, the number of cells in the CAD of , the number of computed pairs of adjacent cells whose dimensions differ by one, and the number of connected components of .
Example 21**.**
Find cell adjacencies for a CAD of the union of two unit balls in
[TABLE]
Note that for the balls have full-dimensional intersection, for they touch at one point, and for they are disjoint.
Example 22**.**
Here we used modified versions of examples from Wilson’s benchmark set [26] (version 4). Of the examples we selected that involved at least variables and we used quantifier-free versions of the examples. In of the examples the system was not well-based and involved more than variables, hence our algorithm did not apply. examples did not finish in seconds. Of the examples for which our implementation succeeded, were well-based and were not well-based and in . On average, took of the total time, took , and took . Five examples with the largest number of cells are given in Table 2. All but the third example are well-based.
Example 23**.**
Here we took the 3D solids that appear in Mathematica SolidData and intersected each of them with the solution set of . All examples were well-based and in all our implementation succeeded. On average, took of the total time, took , and took . The five solids which resulted in the largest number of cells are:
- (1)
Steinmetz 6-solid
[TABLE] 2. (2)
Sphericon
[TABLE] 3. (3)
Steinmetz 4-solid
[TABLE] 4. (4)
Solid capsule
[TABLE] 5. (5)
Reuleaux tetrahedron
[TABLE]
The details are given in Table 3.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] D. S. Arnon, G. E. Collins, and S. Mc Callum. Adjacency algorithm for cylindrical algebraic decomposition of three-dimensional space. J. Symbolic Comp. , 5:163–187, 1988.
- 2[2] S. Basu, R. Pollack, and M. Roy. Computing roadmaps of semi-algebraic sets on a variety. Journal of the AMS , 3:55–82, 1999.
- 3[3] S. Basu, R. Pollack, and M. Roy. Algorithms in real algebraic geometry , volume 10. Springer-Verlag New York Inc, 2006.
- 4[4] J. F. Canny. The Complexity of Robot Motion Planning . MIT Press, Cambridge, MA, USA, 1988.
- 5[5] B. Caviness and J. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition , New York, 1998. Springer Verlag.
- 6[6] C. Chen, M. M. Maza, B. Xia, and L. Yang. Computing cylindrical algebraic decomposition via triangular decomposition. In Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC 2009 , pages 95–102. ACM, 2009.
- 7[7] G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. Lect. Notes Comput. Sci. , 33:134–183, 1975.
- 8[8] M. S. E. Din and E. Schost. A baby steps/giant steps probabilistic algorithm for computing roadmaps in smooth bounded real hypersurface. Discrete and Computational Geometry , 45:181–220, 2011.
