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.