=Paper=
{{Paper
|id=Vol-2460/paper6
|storemode=property
|title=On Benefits of Equality Constraints in Lex-Least Invariant CAD
|pdfUrl=https://ceur-ws.org/Vol-2460/paper6.pdf
|volume=Vol-2460
|authors=Akshar Nair,James Davenport,Gregory Sankaran
|dblpUrl=https://dblp.org/rec/conf/scsquare/NairDS19
}}
==On Benefits of Equality Constraints in Lex-Least Invariant CAD==
https://ceur-ws.org/Vol-2460/paper6.pdf
On Benefits of Equality Constraints in
Lex-Least Invariant CAD (extended abstract)
Akshar Nair James Davenport Gregory Sankaran
University of Bath, Bath, United Kingdom, BA2 7AY.
{asn42,masjhd,masgks}@bath.ac.uk
Abstract
We consider two methods for CADs, one due to Mc-
Callum and one due to Lazard. The former uses or-
der invariant CADs and has been modified, by Mc-
Callum 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 invari-
ant 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 first variable to be
projected. In the further steps of the projection phase,
we use Lazard’s original projection operator. Nonethe-
less, reducing the output in the first step has a domino
effect throughout the remaining steps, which signifi-
cantly reduces the complexity. The long-term goal is to
find a general projection operator that takes advantage
of the equality constraint and can be used recursively,
and this operator gives an important first step in that
direction.
1 Introduction
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 first 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
Copyright c by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 Interna-
tional (CC BY 4.0).
In: J. Abbott, A. Griggio (eds.): Proceedings of the 4th SC-square Workshop, Bern, Switzerland, 10th July 2019,
published at http://ceur-ws.org
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 first variable eliminated is xn .
Base phase: Decompose R1 according to specifications 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 + y 2 − 1.
S1
S3
(0, 0) S2
S1 = {x2 + y 2 − 1 > 0}; S2 = {x2 + y 2 − 1 = 0}; S3 = {x2 + y 2 − 1 < 0}
This is not a cylindrical decomposition of R2 , because when we project S1 and S2 to R1 we
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:
S3,5
S2,3 S4,3
S3,4
S1,1 S5,1
S2,2 S3,3 (0, 0) S4,2
S2,1 S4,1
S3,2
S3,1
S1,1 = {x < −1}, S5,1 = {x > 1},
S2,1 = {x = −1, y < 0}, S2,2 = {x = −1, y = 0}, S2,3 = {x = −1, y > 0},
2 2
S3,1 = {x + y − 1 > 0 ∧ 1 > x > −1 ∧ y < 0}, S3,2 = {x2 + y 2 − 1 = 0 ∧ 1 > x > −1 ∧ y < 0},
S3,3 = {x2 + y 2 − 1 < 0 ∧ 1 > x > −1}, S3,4 = {x2 + y 2 − 1 = 0 ∧ 1 > x > −1 ∧ y > 0},
S3,5 = {x2 + y 2 − 1 > 0 ∧ 1 > x > −1 ∧ y > 0},
S4,1 = {x = 1, y < 0}, S4,2 = {x = 1, y = 0}, S4,3 = {x = 1, y > 0}.
The first CAD algorithm, that of Collins [1], gives sign-invariant CADs and has complexity
2n+O(1)
(2dm)3 when the input consists of m polynomials of at most degree d in n variables [2].
A faster algorithm, using order-invariant CADs, was given by McCallum [4] in 1984: it fails,
however, if one of the input polynomials is nullified, i.e. vanishes identically above some point in
Rn−1 .
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.
Definition 1 A Quantifier Free Tarski Formula (QFF) is made up of atoms connected by the
standard boolean operators ∧, ∨ and ¬. The atoms are statements about signs of polynomials
f ∈ R[x1 , . . . , xn ] of the form f ∼ 0 where ∼∈ {=, <, >} (and by combination also {≥, ≤, 6=}).
Strictly speaking we need only the relation <, but this form is more convenient because of the
next definition.
Definition 2 [2] An Equational Constraint (EC) is a polynomial equation logically implied by
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.
Example 2 [2] Let f and g be two polynomials,
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.
3. The formula f 2 + g 2 ≤ 0 also has no explicit EC, but it has two implicit EC: f = 0 and
g = 0.
4. The formula f = 0 ∨ f 2 + g 2 ≤ 0 logically implies f = 0, and the equation is an atom of the
formula which makes f = 0 an explicit EC according to the definition. However, it is not
a syntactically explicit EC. As the logical deduction is semantic rather than syntactic, the
EC is unlikely to be picked up by a basic input parser and so has more in common with an
implicit EC.
Definition 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 α ∈ C for every f ∈ 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 [1] and order [4].
ECs were first exploited in 1999 by McCallum in [5], which modifies the process of [4] so as to
construct a decomposition of the variety described by the EC rather than a decomposition of
Rn . This method lifts an order-invariant CAD of Rn−1 to a sign-invariant CAD of some variety
in Rn .
Because the output is not order-invariant the algorithm is not recursive. Later, McCallum [6]
gave a modified algorithm that does output an order-invariant CAD. It can be used recursively to
deal with multiple equational constraints, which reduces the complexity significantly in specific
cases.
In 1994, Lazard [3] provided a different approach to constructing a CAD of Rn , in which the
order of a polynomial is replaced by the lex-least valuation (see Definition 4 below). Lazard’s
approach allows a slightly smaller projection operator, because unlike McCallum’s, it does not
require middle coefficients, only leading and trailing ones: also the lifting process is significantly
different. It also handles the cases in which McCallum’s algorithms fail due to nullification, when
a polynomial vanishes identically.
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 [5]. It works well for syntactically explicit ECs:
in other cases, we would resort to using the normal projection operator. Like [5], it cannot be
used inductively, since it outputs a sign-invariant CAD rather than a lex-least valuation-invariant
CAD.
Our improvement is that we only need to compute Lazard’s projection operator on the equa-
tional constraints. The only additional polynomials are the resultants between the equational
and non-equational constraints. This is a considerable improvement over Collins’ projection op-
erator and McCallum’s modifications, as the projection set in our case is significantly smaller.
This will be further discussed in Section 4.
2 Lex-least Valuation
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.
Definition 4 [8, Definition 2.4] Let n ≥ 1 and suppose that f ∈ R[x1 , . . . , xn ] is non-zero and
α = (α1 , . . . , αn ) ∈ Rn . The lex-least valuation να (f ) at α is the least (with respect to ≥lex )
element v = (v1 , . . . , vn ) ∈ 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 [8]. Later we shall also use the Lazard valuation, and some facts about
it, for formal power series rather than polynomials. To justify this requires some technical detail
which we omit here.
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) να is a valuation: that is, if f and g are non-zero elements of
R[x1 , . . . , xn ] and α ∈ Rn , then να (f g) = να (f ) + να (g) and να (f + g) ≥lex min{να (f ), να (g)}.
Proposition 2 (Upper semicontinuity) Let f be a nonzero element of R[x1 , . . . , xn ] and let
a ∈ Rn . Then there exists an open neighbourhood V ⊂ Rn of a, such that νb (f ) ≤lex νa (f ) for
all b ∈ V .
Proposition 3 Let f and g be non-zero elements of R[x1 , . . . , xn ] and let S ⊂ Rn be connected.
Then f g is lex-least invariant in S if and only if f and g are lex-least invariant in S.
Proof. Suppose that f g is lex-least invariant, say vb (f g) = v for all b ∈ S, so vb (g) = v − vb (f ).
Choose a ∈ S then by Proposition 2 the set S+ = {b ∈ S | vb (f ) ≤lex va (f )} is open. But
S− = {b ∈ S | vb (f ) ≥lex va (f )} = {b ∈ S | v − vb (g) ≥lex v − va (g)} = {b ∈ S | vb (g) ≤lex va (g)}
is also open. Hence S+ ∩ S− = {b ∈ S | vb (f ) = va (f )} is open, for any a ∈ 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.
Definition 5 [8] Let n ≥ 2, take a non-zero element f in R[x1 , . . . , xn ] and let β ∈ Rn−1 . The
Lazard residue fβ ∈ R[xn ] of f at β, and the lex-least valuation of f above β are defined to be
the result of Algorithm 1:
Algorithm 1 Lazard residue
1: fβ ← f
2: for i ← 1 to n − 1 do
3: νi ← greatest integer ν such that (xi − βi )ν |fβ .
4: fβ ← fβ /(xi − βi )νi .
5: fβ ← fβ (βi , xi+1 , . . . , xn )
6: end for
7: return fβ , (ν1 , . . . , νn−1 )
The value of (ν1 , . . . , νn−1 ) ∈ Zn−1 is called the lex-least valuation of f above β ∈ Rn−1 (not
to be confused with the lex-least valuation at α ∈ Rn , defined in Definition 4). We denote it by
Nβ (f ). Notice that if b = (β, bn ) ∈ Rn then νb (f ) = (Nβ (f ), νn ) for some integer νn : in other
words, Nβ (f ) consists of the first n − 1 coordinates of the valuation of f at any point above β.
Definition 6 [8, definition 2.10] Let S ⊆ Rn−1 and f ∈ R[x1 , . . . , xn ]. We say that f is Lazard
delineable on S if:
i) The lex-least valuation of f above β is the same for each point β ∈ S.
ii) There exist finitely many continuous functions θi : S → R, such that θ1 < . . . < θk if k > 0
and such that for all β ∈ S, the set of real roots of fβ is {θ1 (β), . . . , θk (β)}.
iii) If k = 0, then the graph of f does not pass over S. If k ≥ 1, then there exist positive integers
m1 , . . . , mk such that, for all β ∈ S and for all 1 ≤ i ≤ k, mi is the multiplicity of θi (β) as
a root of fβ .
Definition 7 [8, Definition 2.10] Let f be Lazard delineable on S ⊆ Rn−1 . Then
i) The graphs θi are called Lazard sections and mi is the associated multiplicity of these sec-
tions.
ii) The regions between consecutive Lazard sections1 are called Lazard sectors.
1 Including θ = −∞ and θ
0 k+1 = +∞.
For later use, we propose some geometric terminology to describe the conditions under which
a polynomial is nullified in the terminology of [5].
Definition 8 A variety C ⊆ Rn is called a curtain if, whenever (x, xn ) ∈ C, then (x, y) ∈ C for
all y ∈ R.
Definition 9 Suppose f ∈ R[x1 , . . . , xn ] and W ⊆ Rn−1 . We say that f has a curtain at W if
for all x ∈ W and y ∈ R we have f (x, y) = 0.
Remark 1 Lazard delineability differs from delineability as in [1] and [5] in two important ways.
First, we require lex-least invariance on the sections. Second, delineability is not defined on
curtains, but Lazard delineability is because the Lazard sections are of fβ rather than f .
Proposition 4 [8, Proposition 2.11] Let f ∈ R[x1 , . . . , xn ] be of positive degree in xn and let
S be a connected subset of Rn−1 . Suppose that f is Lazard delineable on S. Then f is lex-least
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 β ∈ S, is invariant,
meaning that for α ∈ Rn in the sections of f over S, the first 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 α ∈ Rn . After the
loop is finished, we proceed to the first step of the loop and perform it for i = n and the n-tuple
ν1 , . . . , νn is the required valuation.
3 Lex-least Invariance
This section contains details of Lazard’s original projection operator used to obtain a lex-least
invariant CAD.
Definition 10 [8, definition 2.1] Let A be a finite 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 coefficients of the elements of A.
ii) All trailing coefficients 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 efficient CAD, in practice and on av-
erage [7]. This projection operator is fairly large in the event that we have a large number of
polynomials in A. On the other hand, it is smaller than McCallum’s projection operator in [4],
as it only asks for the leading and trailing coefficients, rather than all of them.
McCallum et al. [8] gave a proof for the following theorem. It underpins the use of Lazard’s
projection operator in producing a lex-least invariant CAD.
Theorem 1 [8, Theorem 5.1] Let f ∈ R[x1 , . . . , xn ] be of positive degree in xn . Let D, l and t
denote the discriminant, leading coefficient and trailing coefficient (i.e. the coefficient of x0n ) of
f respectively, and suppose that each of these polynomials is not identically zero (as elements of
R[x]). Let S be a connected submanifold of Rn−1 in which D, l and t are all lex-least invariant.
Then f is Lazard delineable on S, and this implies that f is lex-least invariant in every Lazard
section and sector over S.
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 Modification to Lazard’s Projection Operator
This section focuses on the main claim of this paper. We first define our modification of Lazard’s
projection operator. This projection operator reduces the projection set in the first phase, where
there is an EC in the QFF. This is similar to McCallum’s modification in [5] of his original
operator in [4]. The reason for considering the resultants here is the same: we are performing
the P -invariant CAD on the hypersurface f = 0, rather than Rn .
Definition 11 Let A ⊂ R[x1 , . . . , xn ] be a set of polynomial constraints. Let E ⊆ A, and define
the projection operator PLE (A) as follows:
PLE (A) = PL(E) ∪ {resxn (f, g) | f ∈ E, g ∈ A \ E}.
Remark 3 In practice we will choose E to consist of polynomials occurring in equational con-
straints.
Theorem 2 Let n ≥ 2 and let f, g ∈ R[x1 , . . . , xn ] be of positive degrees in the main variable
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 α ∈ σ. 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 definition of θ, we have θ(0, . . . , 0) = 0 and also f (0, . . . , 0) = 0. Sup-
pose 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 ) · xm n where q̄(0) 6= 0. Therefore, by Hensel’s Lemma (as in
[5]), there exists a euclidean neighbourhood N1 of the origin in Rn and formal power series
q(x1 , . . . , xn ) and h(x1 , . . . , xn ) such that f (x1 , . . . , xn ) = q(x1 , . . . , xn ) · h(x1 , . . . , xn ), where
q(0, . . . , 0, xn ) = q̄(xn ) and h(0, . . . , 0, xn ) = xm
n.
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 ) ∈ N2 × (−, ). Since θ is continuous,
we can shrink N2 to get θ(x1 , . . . , xn−1 ) ∈ (−, ) for all (x1 , . . . , xr−1 ) ∈ N2 . In essence the
subsection of σ (of f over N2 ) lies in N2 × (−, ). If α0 ∈ 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 first 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.
Theorem 3 Let A ⊂ R[x1 , . . . , xn ] be a set of irreducible polynomials in n variables of positive
degrees in xn , where n ≥ 2. Let E be a subset of A. Let S be a connected submanifold of Rn−1 .
Suppose that each element of PLE (A) is lex-least invariant in S. Then each element of E either
vanishes identically above S (i.e. has a curtain) or is Lazard delineable on S. The sections over
S of the elements of E which do not vanish identically on S are pairwise disjoint, each element
of E is lex-least invariant in every such section, and each element of A not in E is sign-invariant
in every such section.
Proof.
This follows directly from Theorem 1 and Theorem 2.
Theorem 3 does come with its flaws, similar to McCallum’s single equational constraint [5].
The method cannot be used recursively as it will output a sign-invariant CAD.
5 Conclusion and Further Research
The main requirement for Theorem 3 to work is that the Equational Constraint in the input
QFF must not have curtains. This is superficially similar to the “no nullification” requirements
of [4, 5, 6], but is less constraining in two ways.
1. It only applies to the EC, not to the other polynomials involved.
2. Because we ae using Lazard lifting, rather than that of [4], this constraint only applies to
xn , and not recursively.
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 modified projection operator PLE (A) only in the first step of the projection phase, and
Lazard’s projection operator PL(A) for the subsequent steps. Despite these drawbacks, reducing
the output of the first step in the projection phase has a domino effect on further steps.
McCallum’s projection operator in [6] shows that it is possible to benefit from having an EC in
the QFF, and provides an order-invariant CAD. By contrast the projection operator in [5] only
provides a sign-invariant CAD. Similarly, we hope to find a projection operator that outputs a
lex-least invariant CAD so that it can be used recursively. This modification would reduce the
complexity of the algorithm significantly.
References
[1] Collins, G.: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decom-
position. In: Proceedings 2nd. GI Conference Automata Theory & Formal Languages. pp.
134–183 (1975)
[2] England, M., Bradford, R., Davenport, J.: Cylindrical Algebraic Decomposition with Equa-
tional Constraints. In: Davenport, J., England, M., Griggio, A., Sturm, T., Tinelli, C. (eds.)
Symbolic Computation and Satisfiability Checking. Journal of Symbolic Computation (to
appear) (2019)
[3] Lazard, D.: An Improved Projection Operator for Cylindrical Algebraic Decomposition. In:
Bajaj, C. (ed.) Proceedings Algebraic Geometry and its Applications: Collections of Papers
from Shreeram S. Abhyankar’s 60th Birthday Conference. pp. 467–476 (1994)
[4] McCallum, S.: An Improved Projection Operation for Cylindrical Algebraic Decomposition.
Ph.D. thesis, University of Wisconsin-Madison Computer Science (1984)
[5] McCallum, S.: On Projection in CAD-Based Quantifier Elimination with Equational Con-
straints. In: Dooley, S. (ed.) Proceedings ISSAC ’99. pp. 145–149 (1999)
[6] McCallum, S.: On Propagation of Equational Constraints in CAD-Based Quantifier Elimi-
nation. In: Mourrain, B. (ed.) Proceedings ISSAC 2001. pp. 223–230 (2001)
[7] McCallum, S., Hong, H.: On Using Lazard’s Projection in CAD Construction. J. Symbolic
Computation 72, 65–81 (2016)
[8] McCallum, S., Parusiński, A., Paunescu, L.: Validity proof of Lazard’s method for CAD
construction. J. Symbolic Comp. 92, 52–69 (2019)