=Paper=
{{Paper
|id=Vol-3273/paper5
|storemode=property
|title=Equational Constraints, the Lazard Projection and the Curtain Problem (short paper)
|pdfUrl=https://ceur-ws.org/Vol-3273/paper5.pdf
|volume=Vol-3273
|authors=Akshar S. Nair,James H. Davenport,Gregory Sankaran
|dblpUrl=https://dblp.org/rec/conf/scsquare/NairDS21
}}
==Equational Constraints, the Lazard Projection and the Curtain Problem (short paper)==
https://ceur-ws.org/Vol-3273/paper5.pdf
Equational Constraints, the Lazard Projection and the
Curtain Problem
Akshar S. Nair1 , James H. Davenport1,2 and Gregory Sankaran2
1
University of Bath, Faculty of Science, Department of Computer Science, Bath UK
2
University of Bath, Faculty of Science, Department of Mathematical Sciences, Bath UK
Abstract
Cylindrical Algebraic Decomposition was introduced by Collins in 1975, to help understand and analyse
the real algebraic geometry of a system of polynomials. Nine years later, McCallum’s thesis introduced a
cheaper algorithm, but it could have problems when polynomials, input or generated, vanished identically
(nullified) over a set. Several people have built on McCallum’s work to improve the algorithm further
when there are equational constraints. Lazard’s approach, which was justified in 2019, avoids the
nullification problem. The first author investigated translating these equational constraint methods to
the Lazard projection. Nullification reappears along subsets called curtains. In this paper we summarise
the work done by the first author under the supervision of the other authors for his PhD on propagating
the work by Lazard and Brown-McCallum to exploit equational constraints with the help of curtains.
Keywords
Lazard Projection, Cylindrical Algebraic Decomposition, Equational Constraint, Nullification, Curtains
1. Introduction
Cylindrical Algebraic Decomposition (CAD) is a tool for studying real semi-algebraic sets
algorithmically. It was introduced by Collins [1] in the context of quantifier elimination, so
the precise choice of variables, and their order, matter, and “generic changes of coordinate”
are not legitimate. We fix coordinates 𝑥1 , . . . , 𝑥𝑛 and regard R𝑘 as always having coordinates
𝑥1 , . . . , 𝑥𝑘 . A CAD is a decomposition of a semi-algebraic set 𝑋 ⊆ R𝑛 (for any 𝑛) into semi-
algebraic sets (also known as cells) homeomorphic to R𝑚 , where 0 ≤ 𝑚 ≤ 𝑛, such that the
projections of any two cells onto the first 𝑘 coordinates are either the same or disjoint. We
use “QFF” as an abbreviation for “Quantifier-Free Formula”, i.e. a Boolean combination of
polynomial equalities and inequalities.
Various real-world problems can be reduced to a system of polynomial equalities and inequal-
ities. Often these problems are in the form of a quantifier elimination problem. An example of
this is the piano mover’s problem [2], [3, §2.8]. There are several specialised algorithms in this
area, but CAD is considered one of the most effective methods for quantifier elimination.
CAD algorithms based on [1] consist of three main phases. The first is repeated application
of the projection operator, which takes as input a set of polynomials in 𝑚 variables and outputs
a set of polynomials in 𝑚 − 1 variables. This operator is used recursively (eliminating variables
with respect to our pre-defined order) until the set of polynomials is in the first variable
6𝑡ℎ International Workshop on Satisfiability Checking and Symbolic Computation, 19–20 Aug 2021, College Station U.S.
© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
only. The second phase consists of decomposing R1 into cells determined by the projected
polynomials. The third phase lifts cells recursively from R𝑚 to R𝑚+1 whilst preserving certain
properties. Table 1 describes the various projection operators investigated in [3]. The reductions
in coefficients considered in projections doesn’t affect the asymptotics, but is of substantial
importance in practice, as the gain multiplies at each projection.
Table 1
Projection Operators in [3]
Projection McCallum (1985b) Lazard (1994/2016) Brown-McCallum (2020)
Leading Coefficients Yes Yes Yes
Trailing Coefficients Yes Yes Sometimes
Middle Coefficients Yes No No
Discriminant Yes Yes Yes
Resultant Yes Yes Yes
Collins’ original algorithm has bad complexity. McCallum reduced the complexity by switch-
ing from sign-invariant CADs to order-invariant CADs. McCallum’s improved projection
operator is defined as follows.
Definition 1. Let 𝐴 be a finite squarefree basis in R[𝑥1 , . . . , 𝑥𝑛 ] with 𝑟 ≥ 2. Then McCallum’s
projection operator P(𝐴) consists of the following polynomials:
• The set of coefficients of all elements of 𝐴.
• The set of discriminants of all elements of 𝐴.
• The set of all cross resultants of the elements of 𝐴 (avoiding the trivial resultants res(𝑓, 𝑓 )).
McCallum’s algorithm, however, introduced a new problem. Since McCallum’s method is
based on the calculating the order of a polynomial, the moment a polynomial (input constraint
or projected) nullifies, the algorithm will detect failure.
1.1. McCallum with equational constraints
Before we look at the improvements, let us first recall the definition of a variety and an equational
constraint.
Definition 2. A (real) variety is a subset of R𝑘 which is the zero set of one or more polynomials,
i.e. {(𝑥1 , . . . 𝑥𝑘 ) ∈ R𝑘 : 𝑓1 (𝑥1 , . . . 𝑥𝑘 ) = 𝑓2 (𝑥1 , . . . 𝑥𝑘 ) = · · · 𝑓𝑙 (𝑥1 , . . . 𝑥𝑘 ) = 0}. We write 𝑉𝑓
for {(𝑥1 , . . . 𝑥𝑘 ) ∈ R𝑘 : 𝑓 (𝑥1 , . . . 𝑥𝑘 ) = 0}
Definition 3. [4] 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
equational constraint is visible in the formula, i.e. the formula Φ is (𝑓 = 0) ∧ Φ′ , we say the
constraint is syntactically explicit.
Example 1 (Equational constraints).
(𝑓 2 ≤ 0) ∧ Φ′ is an explicit equational constraint, but not syntactically explicit. Furthermore the
𝑓 2 may not be an explicit square.
(𝑓 ≥ 0) ∧ (𝑓 ≤ 0) ∧ Φ′ does not contain an explicit equational constraint.
Although implicit and explicit ECs have the same logical status, in practice only the syntacti-
cally explicit ECs will be known to us and therefore be exploitable: see also [4].
The main idea behind exploiting syntactically explicit equational constraints is that if the
input formula is of the form (𝑓 = 0) ∧ Φ′ , then to find solutions of the formula it is sufficient
to decompose the hypersurface described by 𝑓 = 0 rather than the whole of R𝑛 . In practice 𝑓
may factor, and in what follows 𝐸 is the set of factors of 𝑓 .
Definition 4 (Single Equational Constraint). [5] Let 𝐴 be a set of pairwise relatively prime
polynomials in R[𝑥1 , . . . , 𝑥𝑛 ] with 𝑛 ≥ 2 and let 𝐸 ⊂ 𝐴. McCallum’s restricted projection
operator P𝐸 (𝐴) is defined as follows:
P𝐸 (𝐴) = P(𝐸) ∪ {res𝑥𝑛 (𝑓, 𝑔) | 𝑓 ∈ 𝐸, 𝑔 ∈ 𝐴 ∖ 𝐸}. (1)
[5] showed that, if we have an equational constraint 𝑓 = 0 involving 𝑥𝑛 , it suffices to use
P𝐸 (𝐴) to eliminate 𝑥𝑛 , then proceed as usual to eliminate down to 𝑥1 , then lift back to an
order-invariant decomposition of R𝑛−1 , which can then be lifted to a decomposition of R𝑛 such
that the input polynomials are sign-invariant on 𝑉𝑓 . This improved on the complexity of [9]
since it uses significantly fewer polynomials, which also results in the creation of fewer cells.
However, this algorithm fails if the EC nullifies anywhere, or if nullification causes a problem
with the lift to R𝑛−1 . The second drawback to this method is that this projection operator
cannot be used recursively. This is because this method lifts an order-invariant decomposition
to a sign-invariant decomposition.
In 2001 [6], McCallum suggested a further extension of his method from [5], to support
multiple equational constraints, i.e. (𝑓1 = 0) ∧ (𝑓2 = 0) ∧ · · · ∧ Φ′ . The new projection operator
supporting this extension is defined as follows. We designate one of the equational constraints,
say 𝑓 = 0, as the appropriate constraint at this level, and in what follows 𝐸 is the set of factors
of 𝑓 .
Definition 5 (Multiple Equational Constraints). [6] Let 𝐴 be a set of pairwise relatively prime
polynomials in R[𝑥1 , . . . , 𝑥𝑛 ] with 𝑛 ≥ 2 and let 𝐸 ⊂ 𝐴. McCallum’s semi-restricted projection
operator P*𝐸 (𝐴) is defined as follows:
P*𝐸 (𝐴) = P(𝐴) ∖ res(𝐴 ∖ 𝐸, 𝐴 ∖ 𝐸). (2)
Note that P*𝐸 (𝐴) includes the discriminants of 𝐴 ∖ 𝐸, which P𝐸 (𝐴) does not.
This operator can be used recursively as it lifts order invariance to order invariance. However,
because it uses order invariance, it can still fail because of nullification.
2. Lazard Projection and Lifting
This method, adjusting the lifted polynomials when nullification occurred, was introduced in
[8].
Definition 6. Let 𝑣, 𝑤 ∈ Z𝑛 . We say that 𝑣 = (𝑣1 , . . . , 𝑣𝑛 ) ≥𝑙𝑒𝑥 (𝑤1 , . . . , 𝑤𝑛 ) = 𝑤 if and
only if either 𝑣 = 𝑤 or there is an 𝑖 ≤ 𝑛 such that 𝑣𝑖 > 𝑤𝑖 and 𝑣𝑘 = 𝑤𝑘 for all 𝑘 in the range
1 ≤ 𝑘 < 𝑖.
Definition 7. [7, Definition 2.4] Let 𝑛 ≥ 1 and suppose that 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] is non-zero and
𝛼 = (𝛼1 , . . . , 𝛼𝑛 ) ∈ R𝑛 . The lex-least valuation 𝜈𝛼 (𝑓 ) at 𝛼 is the least (with respect to ≥𝑙𝑒𝑥 )
element 𝑣 = (𝑣1 , . . . , 𝑣𝑛 ) ∈ N𝑛 such that 𝑓 expanded about 𝛼 has the term
𝑐(𝑥1 − 𝛼1 )𝑣1 · · · (𝑥𝑛 − 𝛼𝑛 )𝑣𝑛 ,
where 𝑐 ̸= 0.
Definition 8. [7] Let 𝑛 ≥ 2, and suppose that 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] is non-zero and that 𝛽 ∈ R𝑛−1 .
The Lazard residue 𝑓𝛽 ∈ R[𝑥𝑛 ] of 𝑓 at 𝛽, and the lex-least semi-valuation 𝜈𝛽′ (𝑓 ) = (𝜈1 , . . . , 𝜈𝑛−1 )
of 𝑓 above 𝛽, are defined to be the result of Algorithm 1.
Algorithm 1 Lazard residue
Input: 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] and 𝛽 ∈ R𝑛−1 .
Output: Lazard residue 𝑓𝛽 and lex-least valuation of 𝑓 above 𝛽.
1: 𝑓𝛽 ← 𝑓
2: for 𝑖 ← 1 to 𝑛 − 1 do
3: 𝜈𝑖 ← greatest integer 𝜈 such that (𝑥𝑖 − 𝛽𝑖 )𝜈 |𝑓𝛽 .
4: 𝑓𝛽 ← 𝑓𝛽 /(𝑥𝑖 − 𝛽𝑖 )𝜈𝑖 .
5: 𝑓𝛽 ← 𝑓𝛽 (𝛽𝑖 , 𝑥𝑖+1 , . . . , 𝑥𝑛 )
6: end for
7: return 𝑓𝛽 , (𝜈1 , . . . , 𝜈𝑛−1 )
Definition 9. [7, Definition 2.10] Let 𝑆 be a connected subset of R𝑛−1 and 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ].
We say that 𝑓 is Lazard delineable on 𝑆 if all the following hold.
i) The lex-least semi-valuation of 𝑓 at 𝛽 is the same for each point 𝛽 ∈ 𝑆.
ii) There exist finitely many (possibly zero) continuous functions 𝜃𝑖 : 𝑆 → R, such that for all
𝛽 ∈ 𝑆, 𝜃1 (𝛽) < . . . < 𝜃𝑘 (𝛽), and the set of real roots of 𝑓𝛽 is {𝜃1 (𝛽), . . . , 𝜃𝑘 (𝛽)}.
iii) If 𝑘 = 0, then for all 𝛽 ∈ 𝑆 the set of real roots of 𝑓𝛽 is empty. If 𝑘 ≥ 1, then there exist
positive integers 𝑚1 , . . . , 𝑚𝑘 such that, for all 𝛽 ∈ 𝑆 and for all 1 ≤ 𝑖 ≤ 𝑘, 𝑚𝑖 is the
multiplicity of 𝜃𝑖 (𝛽) as a root of 𝑓𝛽 .
With the definition of delineability, we are able to define Lazard sections and sectors.
Definition 10. [7, Definition 2.10] Let 𝑓 be Lazard delineable on 𝑆 ⊆ R𝑛−1 .
i) The graphs 𝜃𝑖 are called Lazard sections and 𝑚𝑖 is the associated multiplicity of 𝜃𝑖 .
ii) The regions between consecutive Lazard sections1 are called Lazard sectors.
1
Including the conventional “sections” 𝜃0 = −∞ and 𝜃𝑘+1 = +∞.
To combine Lazard’s method with [5], the following definition is introduced in [3].
Definition 11. Let 𝐴 be a finite set of irreducible polynomials in R[𝑥1 , . . . , 𝑥𝑛 ] with 𝑛 ≥ 2
and let 𝐸 be a subset of 𝐴. The modified Lazard projection operator PL𝐸 (𝐴) is the subset of
R[𝑥1 , . . . , 𝑥𝑛−1 ] consisting of the following polynomials:
• All leading coefficients of the elements of 𝐸.
• All trailing coefficients of the elements of 𝐸.
• All discriminants of the elements of 𝐸.
• All resultants of pairs of distinct elements of 𝐸.
• All resultants res𝑥𝑛 (𝑓, 𝑔) where 𝑓 ∈ 𝐸 and 𝑔 ∈ 𝐴 ∖ 𝐸.
We can also define it as follows:
PL𝐸 (𝐴) = PL(𝐸) ∪ {res𝑥𝑛 (𝑓, 𝑔) | 𝑓 ∈ 𝐸, 𝑔 ∈ 𝐴 ∖ 𝐸}.
3. Curtains
Lazard [8, justified in [7]] removed the nullification limitation by decomposing according to
the lex-least valuation, rather than the order valuation used in [9]. This in effect allows us to
identify the nullifying factors and disregard them in the lifting phase. The first author’s thesis
[3] (see also [10]) shows how to adapt these methods so as to exploit equational constraints:
however, nullification then reappears as a problem, in a different guise. To understand this we
shift attention to the geometric loci where nullification occurs, which we call curtains.
Definition 12. A variety 𝐶 ⊆ R𝑛 is called a curtain if, whenever (𝑥, 𝑥𝑛 ) ∈ 𝐶, then (𝑥, 𝑦) ∈ 𝐶
for all 𝑦 ∈ R.
In other words, 𝐶 is a curtain if it is a union of fibres of R𝑛 → R𝑛−1 , i.e. is 𝐶
ˆ × R for a
variety 𝐶 ⊂ R
ˆ 𝑛−1 .
Definition 13. Suppose 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] and 𝑆 ⊆ R𝑛−1 . We say that 𝑉𝑓 (or 𝑓 ) has a curtain
at 𝑆 if for all (𝛼1 , . . . , 𝛼𝑛−1 ) ∈ 𝑆 and for all 𝑦 ∈ R we have 𝑓 (𝛼1 , . . . , 𝛼𝑛−1 , 𝑦) = 0. We call 𝑆
the base of the curtain.
For a hypersurface 𝑉𝑓 there are two types of curtain.
Definition 14. Let 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] and suppose that 𝐶 is a curtain contained in 𝑉𝑓 . Then 𝐶
is called an explicit curtain if 𝑓 factorises as 𝑓 = 𝑔ℎ, where 𝑔 ∈ R[𝑥1 , . . . , 𝑥𝑛−1 ] and 𝐶 = {𝑥 ∈
R𝑛 | 𝑔(𝑥) = 0} ⊂ R𝑛 . In this case the base of the curtain is given by 𝑔 = 0 in R𝑛−1 . Otherwise
𝐶 is called an implicit curtain.
Note that, if 𝐶 is an explicit curtain, it is possible that ℎ itself has a curtain, explicit or implicit,
which may include some or all of 𝐶. Explicit curtains arise when 𝑓 has non-trivial content,
an obstacle already noted in [11, 12], but implicit curtains are also a challenge, and are not so
easily detected.
Example 2 (Curtains). See Figure 1.
• Explicit Curtain: 𝑓 (𝑥, 𝑦, 𝑧) = 𝑥𝑦 2 − 𝑦 2 − 𝑥𝑧 + 𝑧 = (𝑥 − 1)(𝑦 2 − 𝑧), curtain at (1, 𝑦, 𝑧).
The curtain can be seen in Figure 1a as the sheet given by 𝑥 = 1.
• Implicit Curtain: 𝑓 (𝑥, 𝑦, 𝑧) = 𝑥2 + 𝑦𝑧, curtain at (0, 0, 𝑧). This can be seen in Figure 1b,
where the blue line represents the curtain: 𝑥 = 𝑦 = 0.
(a) Surface with an Explicit Curtain (b) Surface with an Implicit Curtain
Figure 1: Different types of curtains
To deal with curtains in the lifting phase with equational constraints, we first need to be able
to identify where curtains occur. Our process for doing so relies on the following lemma, which
establishes a relationship between curtains and the lex-least valuation.
Lemma 1. Let 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] and 𝛼 ∈ R𝑛−1 . Then 𝜈𝛼′ (𝑓 ) ̸= 0 if and only if there is a curtain
above 𝛼.
Definition 15. Let 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ] and 𝛼 ∈ R𝑛−1 . We say that 𝑓 has a point curtain at 𝛼 if
• 𝑓 (𝛼, 𝑦) = 0 for all 𝑦 ∈ R, and
• there exists a Euclidean open neighbourhood 𝑈 ⊂ R𝑛−1 of 𝛼 such there exists no 𝛽 ∈ 𝑈 ∖{𝛼}
such that 𝑓 (𝛽, 𝑦) = 0 for all 𝑦 ∈ R.
Nair [3, Ch. 6–7] shows that point curtains do not disrupt the lifting phase in Lazard’s
algorithm. Algorithm 2 describes how point curtains are detected during lifting.
Algorithm 2 Detecting and Classifying Curtains
(𝐵, 𝐵 ′ ) ← 𝑃 𝐶(𝑓, 𝐼, 𝑆, 𝑛)
Input = Set of indices 𝐼, set of sample points 𝑆 with respect to the indices 𝐼 which correspond
to the CAD cells in R𝑛−1 , equational constraint 𝑓 ∈ R[𝑥1 , . . . , 𝑥𝑛 ].
Output = 𝐵, 𝐵 ′ , where 𝐵 is the set of sample points that are point curtains and 𝐵 ′ is the set of
sample points that are in curtains (but not point curtains).
1: 𝐵 ← Empty list.
2: 𝐵 ′ ← Empty list.
3: for 𝛼 ∈ 𝑆 do
4: if 𝜈𝛼′ (𝑓 ) ̸= 0 then
5: Check if the nearest 1-cell neighbours have zero valuation.
6: If all neighbours are zero valuation add 𝛼 to 𝐵; otherwise add it to 𝐵 ′ .
7: end if
8: end for
9: return (𝐵,𝐵 ′ ).
4. Complexity analysis
Simple time-step complexity analysis is not sufficient to compare the various projection operators
that have been proposed. We use the (𝑚, 𝑑)-property introduced by McCallum [9, Section 6.1]
and improved by England et al. [4]. We also modify these definitions and methods to account
for the effect of equational constraints.
Definition 16. [9, Section 6.1] A set of polynomials has the (𝑚, 𝑑)-property if it can be partitioned
into 𝑚 sets, such that the maximum∏︀ (in each variable) degree of the product of each set is less than
or equal to d: that is max𝑖 deg𝑥𝑖 𝑓 ∈𝑆 𝑓 ≤ 𝑑.
When projecting with equational constraints we need to use an enhanced version of the (𝑚, 𝑑)-
property, so that any statement made about projection operators using equational constraints
can be used recursively.
Definition 17. [3, Chapter 8] Let 𝐴 be a set of polynomial factors of a family of polynomial
constraints. We say that 𝐴 has the (𝑚, 𝑑)𝑘 -property if 𝐴 can be written as the union of 𝑚 sets
each of combined maximum degree ≤ 𝑑 and each of the first 𝑘 sets consist of the factors of a single
equational constraint.
The outcome of the complexity analysis carried out in [3] is summarised in Table 2. If the set
of inputs has the (𝑚, 𝑑)-property then the set of projected polynomials after projection has the
(𝑀, 2𝑑2 )-property, with 𝑀 as in Table 2.
This shows that, if we have only one equational constraint, the “Single EC” methods are
better. However, if we have multiple equational constraints, the “Multiple EC” methods are
better: for projections with two (or more) equational constraints, the number of polynomials
in 𝑛 − 2 variables is 𝑂(𝑚4 ) for the original methods, 𝑂(𝑚2 ) for the “Single EC” methods and
𝑂(𝑚) for the “multiple EC” methods.
Table 2
Growth of polynomials in CAD
Base Theory by Constraints Original Single EC Multiple EC
⌊︁ ⌋︁
(𝑚+1)2 ⌊︀ 5𝑚+4 ⌋︀ ⌊︀ 11𝑚 ⌋︀
McCallum [5, 6] 2 4 4
⌊︁ 2
⌋︁
(𝑚+1) ⌊︀ 5𝑚+3 ⌋︀ ⌊︀ 9𝑚−1 ⌋︀
Lazard [3] 2 4 4
𝑚(𝑚+1) ⌊︀ 5𝑚+2 ⌋︀ ⌊︀ 9𝑚−2 ⌋︀
Brown-McCallum From [3] 2 4 4
5. Conclusion and Some Future Work
There have been various improvements to the implementations of CAD algorithms to further
decrease the space and time complexity. In this abstract we have given a brief account of the
work done by Nair et al. in [10, 3] on what caused the problems for propagating equational
constraints and how to circumvent them. See Table 2 for a summary of the effect on the number
of polynomials.
There are several avenues one can take to extend this work. Some implementation of the
Lazard-based algorithms has been done in [13] (and there are some useful points in [14]).
However, an implementation of the modified Brown-McCallum algorithm [15] for equational
constraints is yet to be done. Such an implementation would work with curtains.
Exploring how curtains can be detected prior to the projection phases is still an open question.
Such an algorithm would be extremely helpful, as it could be used to eliminate bad candidates
for designated equational constraints.
Finally there is the important and completely open question of whether the lex-least valuation
is the best choice for computing valuation-invariant CADs. Are there other valuations that
could deal with curtains in the input constraints more appropriately? If so, can they be used to
take advantage of equational constraints?
References
[1] G. Collins, Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decom-
position, in: Proceedings 2nd. GI Conference Automata Theory & Formal Languages, 1975,
pp. 134–183.
[2] D. Wilson, R. Bradford, J. Davenport, M. England, A “Piano Movers” Problem Reformulated,
Technical Report CSBU-2013-03 Department of Computer Science University of Bath, 2013.
[3] A. Nair, Curtains in Cylindrical Algebraic Decomposition, Ph.D. thesis, Uni-
versity of Bath, 2021. URL: https://researchportal.bath.ac.uk/en/studentTheses/
curtains-in-cylindrical-algebraic-decomposition.
[4] M. England, R. Bradford, J. Davenport, Cylindrical Algebraic Decomposition with Equa-
tional Constraints, in: J. Davenport, M. England, A. Griggio, T. Sturm, C. Tinelli (Eds.),
Symbolic Computation and Satisfiability Checking: special issue of Journal of Symbolic
Computation, volume 100, 2020, pp. 38–71.
[5] S. McCallum, On Projection in CAD-Based Quantifier Elimination with Equational Con-
straints, in: S. Dooley (Ed.), Proceedings ISSAC ’99, 1999, pp. 145–149.
[6] S. McCallum, On Propagation of Equational Constraints in CAD-Based Quantifier Elimi-
nation, in: B. Mourrain (Ed.), Proceedings ISSAC 2001, 2001, pp. 223–230.
[7] S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard’s method for CAD
construction, J. Symbolic Comp. 92 (2019) 52–69.
[8] D. Lazard, An Improved Projection Operator for Cylindrical Algebraic Decomposition, in:
C. Bajaj (Ed.), Proceedings Algebraic Geometry and its Applications: Collections of Papers
from Shreeram S. Abhyankar’s 60th Birthday Conference, 1994, pp. 467–476.
[9] S. McCallum, An Improved Projection Operation for Cylindrical Algebraic Decomposition,
Technical Report 578, Computer Science University Wisconsin at Madison, 1985. URL:
https://minds.wisconsin.edu/bitstream/handle/1793/58594/TR578.pdf?sequence=1.
[10] S. McCallum, A. Nair, J. Davenport, G. Sankaran, The CAD Conundrum: Lex-Least vs
Order, in: Proceedings 2020 22nd International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing, 2021, pp. 32–35.
[11] M. England, J. Davenport, The Complexity of Cylindrical Algebraic Decomposition
with Respect to Polynomial Degree, in: V. Gerdt, W. Koepf, W. Seiler, E. Vorozhtsov
(Eds.), Proceedings CASC 2016, volume 9890 of Springer Lecture Notes in Computer Science,
Springer, 2016, pp. 172–192. doi:10.1007/978-3-319-45641-6_12.
[12] J. Davenport, M. England, Need Polynomial Systems be Doubly-exponential?, in: G.-M.
Greuel, T. Koch, P. Paule, A. Sommese (Eds.), International Congress on Mathematical
Software ICMS 2016, volume 9725 of Springer Lecture Notes in Computer Science, 2016, pp.
157–164.
[13] Z. Tonks, Poly-algorithmic Techniques in Real Quantifier Elimination, Ph.D. the-
sis, University of Bath, 2021. URL: https://researchportal.bath.ac.uk/en/studentTheses/
poly-algorithmic-techniques-in-real-quantifier-elimination.
[14] G. Kremer, J. Brandt, Implementing arithmetic over algebraic numbers: A tutorial for
Lazard’s lifting scheme in CAD, 23rd International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing (SYNASC 2021) (2021) 4–10.
[15] C. Brown, S. McCallum, Enhancements to Lazard’s Method for Cylindrical Algebraic De-
composition, in: F. Boulier, M. England, T. Sadykov, E. Vorozhtsov (Eds.), Computer Algebra
in Scientific Computing CASC 2020, volume 12291 of Springer Lecture Notes in Computer
Science, 2020, pp. 129–149. doi:https://doi.org/10.1007/978-3-030-60026-6_8.