We consider two methods for CADs, one due to McCallum and one due to Lazard. The former uses order invariant CADs and has been modi ed, by McCallum himself, so as to take advantage of equational constraints. Lazard's method uses lex-least invariant CADs and is in general faster. In this paper, we start to modify Lazard's method so as to exploit equational constraints. Our algorithm takes in a lex-least invariant CAD of Rn 1 as input and outputs a sign invariant CAD of a subvariety of Rn: consequently, it cannot be used recursively, but only for xn, the rst variable to be projected. In the further steps of the projection phase, we use Lazard's original projection operator. Nonetheless, reducing the output in the rst step has a domino e ect throughout the remaining steps, which signi cantly reduces the complexity. The long-term goal is to nd a general projection operator that takes advantage of the equality constraint and can be used recursively, and this operator gives an important rst step in that direction.
A Cylindrical Algebraic Decomposition (CAD) is a decomposition of a semi-algebraic set S Rn (for any n) into semi-algebraic sets (also known as cells) homeomorphic to Rm, where 1 m n, such that the projection of any two cells onto the rst k coordinates is either the same or disjoint. We generally want the cells to have some property relative to some given set of input polynomials. For example, we might require sign-invariance, i.e. the sign of each input polynomial (often referred to as a constraint) is constant on each cell. Many algorithms for CAD consist of the following three phases.
Projection phase: This phase consists of reducing the number of variables of the polynomial constraints (using a function known as the projection operator) until it has reached polynomials in one variable (R[x1]). The variable ordering is important: we choose x1 > x2 > : : : > xn, i.e. the rst variable eliminated is xn.
Base phase: Decompose R1 according to speci cations of the required CAD. Each cell is given a sample point, which is used for tracking cells in the lifting phase.
Lifting phase: This phase consists of decomposing higher dimensional spaces using the sample points and the projection polynomials in that dimension, until S is decomposed. Example 1 Let us look at the decomposition of S = R2 with respect to the input polynomial: x2 + y2 1.
S3 (0; 0)
S1
S2 S1 = fx2 + y2 1 > 0g; S2 = fx2 + y2 1 = 0g; S3 = fx2 + y2 1 < 0g
get R and ( 1; 1) respectively. These have non-empty intersection but are not the same. To decompose S cylindrically (with ordering x > y), we take:
S1;1
S2;3 S2;2 S2;1
S3;5 S3;2
S3;1 S3;3 (0; 0)
S4;2 S3;4
S4;3
S5;1
S4;1
S2;3 = fx = S3;2 = fx2 + y2 1; y > 0g; 1 = 0 ^ 1 > x >
1 ^ y < 0g; S3;4 = fx2 + y2 1 = 0 ^ 1 > x >
1 ^ y > 0g; S4;3 = fx = 1; y > 0g: S1;1 = fx < S2;1 = fx = S3;1 = fx2 + y2 S3;3 = fx2 + y2 S3;5 = fx2 + y2 S4;1 = fx = 1; y < 0g; 1g; 1; y < 0g; 1 > 0 ^ 1 > x >
S5;1 = fx > 1g;
S2;2 = fx =
1; y = 0g; 1 ^ y < 0g; 1 < 0 ^ 1 > x > 1 > 0 ^ 1 > x > 1g; 1 ^ y > 0g;
S4;2 = fx = 1; y = 0g;
The rst CAD algorithm, that of Collins [
If S is contained in a subvariety it is clearly wasteful to compute a decomposition of Rn. To make this idea more precise, we need some terminology.
standard boolean operators ^; _ and :. The atoms are statements about signs of polynomials f 2 R[x1; : : : ; xn] of the form f 0 where 2 f=; <; >g (and by combination also f ; ; 6=g). Strictly speaking we need only the relation <, but this form is more convenient because of the next de nition.
a QFF. If it is an atom of the formula, it is said to be explicit; if not, then it is implicit. If the constraint is visibly an equality one from the formula, i.e. the formula is f = 0 ^ 0, we say the constraint is syntactically explicit.
Although implicit and explicit ECs have the same logical status, in practice only the syntactically explicit ECs will be known to us and therefore be available to be exploited.
1. The formula f = 0 ^ g > 0 has an explicit EC f = 0. 2. The formula f = 0 _ g = 0 has no explicit EC, however the equation f g = 0 is an implicit
EC.
g = 0.
0 also has no explicit EC, but it has two implicit EC: f = 0 and 4. The formula f = 0 _ f 2 + g2 0 logically implies f = 0, and the equation is an atom of the formula which makes f = 0 an explicit EC according to the de nition. However, it is not a syntactically explicit EC. As the logical deduction is semantic rather than syntactic, the
De nition 3 Let A be a set of polynomials in R[x1; : : : ; xn] and P : R[x1; : : : ; xn] Rn ! a
function to some set . If C Rn is a cell and P (f; ) is independent of 2 C for every f 2 A,
then A is called P -invariant over that cell. If this is true for all the cells of a decomposition, we
say the decomposition is P -invariant. Common P are sign [
ECs were rst exploited in 1999 by McCallum in [
Because the output is not order-invariant the algorithm is not recursive. Later, McCallum [
In 1994, Lazard [
In this paper, we modify Lazard's process so as to exploit a single equational constraint. The
result is similar to the projection operator of [
Our improvement is that we only need to compute Lazard's projection operator on the equational constraints. The only additional polynomials are the resultants between the equational and non-equational constraints. This is a considerable improvement over Collins' projection operator and McCallum's modi cations, as the projection set in our case is signi cantly smaller. This will be further discussed in Section 4. 2
In order to understand lex-least valuation, let us recall lexicographic order lex on Nn, where n 1. We say that v = (v1; : : : ; vn) lex (w1; : : : ; wn) = w if and only if either v = w or there exists an i n such that vi > wi and vk = wk for all k in the range 1 k < i. De nition 4 [8, De nition 2.4] Let n 1 and suppose that f 2 R[x1; : : : ; xn] is non-zero and = ( 1; : : : ; n) 2 Rn. The lex-least valuation (f ) at is the least (with respect to lex) element v = (v1; : : : ; vn) 2 Nn such that f expanded about has the term c(x1 1)v1 (xn n)vn ; where c 6= 0.
Note that (f ) = (0; : : : ; 0) if and only if f ( ) 6= 0. The lex-least valuation is referred to as
the Lazard valuation in [
Example 3 If n = 1 and f (x1) = x31 2x21 + x1, then 0(f ) = 1 and 1(f ) = 2. If n = 2 and f (x1; x2) = x1(x2 1)2, then (0;0)(f ) = (1; 0), (2;1)(f ) = (0; 2) and (0;1)(f ) = (1; 2).
The following are the important properties of the lex-least valuation, taken from [8, Section 3]. Proposition 1 (Valuation) R[x1; : : : ; xn] and 2 Rn, then is a valuation: that is, if f and g are non-zero elements of (f g) = (f ) + (g) and (f + g) lex minf (f ); (g)g.
Proposition 2 (Upper semicontinuity) Let f be a nonzero element of R[x1; : : : ; xn] and let a 2 Rn. Then there exists an open neighbourhood V Rn of a, such that b(f ) lex a(f ) for all b 2 V .
Proof. Suppose that f g is lex-least invariant, say vb(f g) = v for all b 2 S, so vb(g) = v Choose a 2 S then by Proposition 2 the set S+ = fb 2 S j vb(f ) lex va(f )g is open. But vb(f ).
S = fb 2 S j vb(f ) lex va(f )g = fb 2 S j v vb(g) lex v va(g)g = fb 2 S j vb(g) lex va(g)g is also open. Hence S+ \ S = fb 2 S j vb(f ) = va(f )g is open, for any a 2 S, so the function b 7! vb(f ) is a continuous function from S to Zn. As S is connected, this function is constant, i.e. f is lex-least invariant. The other implication is trivial.
De nition 5 [
the result of Algorithm 1: Algorithm 1 Lazard residue
f 1: f 2: for i 3: i 4: f 5: f 6: end for 7: return f ; ( 1; : : : ; n 1) 1 to n 1 do greatest integer f =(xi i) i . f ( i; xi+1; : : : ; xn) such that (xi
i) jf .
The value of ( 1; : : : ; n 1) 2 Zn 1 is called the lex-least valuation of f above 2 Rn 1 (not to be confused with the lex-least valuation at 2 Rn, de ned in De nition 4). We denote it by N (f ). Notice that if b = ( ; bn) 2 Rn then b(f ) = (N (f ); n) for some integer n: in other words, N (f ) consists of the rst n 1 coordinates of the valuation of f at any point above .
Rn 1 and f 2 R[x1; : : : ; xn]. We say that f is Lazard i) The lex-least valuation of f above is the same for each point
i) The graphs i are called Lazard sections and mi is the associated multiplicity of these sections. ii) The regions between consecutive Lazard sections1 are called Lazard sectors. 1Including 0 =
1 and k+1 = +1.
For later use, we propose some geometric terminology to describe the conditions under which
a polynomial is nulli ed in the terminology of [
De nition 8 A variety C all y 2 R.
Rn is called a curtain if, whenever (x; xn) 2 C, then (x; y) 2 C for
invariant in each Lazard section and sector of f over S.
Proof. We know that N (f ), the lex-least valuation of f above , for all 2 S, is invariant, meaning that for 2 Rn in the sections of f over S, the rst n 1 coordinates of (f ) agree with N (f ). Consider a section given by with associated multiplicity m, and = ( ; ( )) the point of this section above . Then the last coordinate of (f ) is m, and hence f is lex-least invariant in every section of f over S. It is also invariant on sectors because there the last component of the valuation is just 0.
Remark 2 We can use Algorithm 1 to compute the lex-least valuation of f at 2 Rn. After the loop is nished, we proceed to the rst step of the loop and perform it for i = n and the n-tuple
3
This section contains details of Lazard's original projection operator used to obtain a lex-least invariant CAD.
De nition 10 [8, de nition 2.1] Let A be a nite set of irreducible polynomials in R[x1; : : : ; xn] with n 2. The Lazard projection PL(A) is a subset of R[x1; : : : ; xn 1] composed of the following polynomials.
i) All leading coe cients of the elements of A. ii) All trailing coe cients of the elements of A. iii) All discriminants of the elements of A. iv) All resultants of pairs of distinct elements of A.
Experimentally this projection operator gives a more e cient CAD, in practice and on
average [
McCallum et al. [
denote the discriminant, leading coe cient and trailing coe cient (i.e. the coe cient of x0n) of f respectively, and suppose that each of these polynomials is not identically zero (as elements of
In summary, Theorem 1 says that if PL(A) is lex-least invariant over a section S, then all polynomials in A are Lazard delineable over S. This implies that the projection operator can be used inductively, and this makes it possible to provide a lex-least invariant CAD. 4
This section focuses on the main claim of this paper. We rst de ne our modi cation of Lazard's
projection operator. This projection operator reduces the projection set in the rst phase, where
there is an EC in the QFF. This is similar to McCallum's modi cation in [
A, and de ne
PLE (A) = PL(E) [ fresxn (f; g) j f 2 E; g 2 A n Eg:
xn. Let S be a connected subset of Rn 1. Suppose that f is Lazard delineable on a connected submanifold S Rn 1, in which R = resxn (f; g) is lex-least invariant and that f does not have a curtain on S. Then g is sign-invariant in each section of f over S.
Proof. Let be a section of f over S, given by the map : S ! R. Since g is a continuous function it is enough to show that g is sign-invariant in a euclidean neighbourhood in of an arbitrary point 2 . We may take to be the origin, and we may also assume that g( ) = 0, since otherwise g is sign-invariant in a neighbourhood of in Rn, and in particular in a neighbourhood in .
Now, by the de nition of , we have (0; : : : ; 0) = 0 and also f (0; : : : ; 0) = 0.
Suppose that xn = 0 has multiplicity m 6= 0 as a root of f (0; : : : ; 0; xn) = 0. This implies
that f (0; : : : ; 0; xn) = q(xn) xnm where q(0) 6= 0. Therefore, by Hensel's Lemma (as in
[
Since q(0; : : : ; 0) 6= 0 in N1, there exist > 0 and an open neighbourhood N2 of the origin in Rn 1, such that q(x1; : : : ; xn) 6= 0 for all (x1; : : : ; xn) 2 N2 ( ; ). Since is continuous, we can shrink N2 to get (x1; : : : ; xn 1) 2 ( ; ) for all (x1; : : : ; xr 1) 2 N2. In essence the subsection of (of f over N2) lies in N2 ( ; ). If 0 2 S \ N2 then, since f is Lazard delineable, ( 0; ( 0))(f ) = (f ).
On the other hand, (h) = (0; : : : ; m). Since f = q h and f is Lazard delineable in S \ N2, this implies that ( 0; ( 0))(h) = (0; : : : ; m).
Denote by P the resultant of h and g with respect to xn. As in the proof of [5, Theorem 2.2] we have R = Q P for some suitable formal power series Q in the rst n 1 variables. We also have P = 0 at since h and g both vanish there, so (P ) is non-zero. By assumption R is lex-least invariant in the region N2, so P is lex-least invariant in N2 (by Proposition 3).
Since h = 0 in \ (N2 ( ; )) \ and P is lex-least invariant in N2, we see that g = 0 in \ (N2 ( ; )) which is a euclidean neighbourhood of in . Thus g is sign-invariant in , which implies that it is sign-invariant in S.
degrees in xn, where n 2. Let E be a subset of A. Let S be a connected submanifold of Rn 1.
vanishes identically above S (i.e. has a curtain) or is Lazard delineable on S. The sections over
This follows directly from Theorem 1 and Theorem 2.
Theorem 3 does come with its aws, similar to McCallum's single equational constraint [
The main requirement for Theorem 3 to work is that the Equational Constraint in the input
QFF must not have curtains. This is super cially similar to the \no nulli cation" requirements
of [
1. It only applies to the EC, not to the other polynomials involved.
2. Because we ae using Lazard lifting, rather than that of [
The other limiting factor for this projection is that it cannot be used recursively because it outputs a sign-invariant CAD, rather than a lex-least invariant CAD. This limits us to using the modi ed projection operator PLE (A) only in the rst step of the projection phase, and Lazard's projection operator PL(A) for the subsequent steps. Despite these drawbacks, reducing the output of the rst step in the projection phase has a domino e ect on further steps.
McCallum's projection operator in [