Equational Constraints, the Lazard Projection and the Curtain Problem

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

• eol>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 semialgebraic 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 efective 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 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 coeficients considered in projections doesn’t afect the asymptotics, but is of substantial importance in practice, as the gain multiplies at each projection.

Collins’ original algorithm has bad complexity. McCallum reduced the complexity by switching 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 ≥

projection operator P() consists of the following polynomials: 2. Then McCallum’s • The set of coeficients 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 suficient 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 (, ) | ∈ , ∈ ∖ }.

[5] showed that, if we have an equational constraint = 0 involving , it sufices 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( ∖ , ∖ ).

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. (1) (2)

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 ← 3: ← 4: ← 5: ← 6: end for 7: return , ( 1, . . . , − 1) 1 to − 1 do greatest integer such that ( − ) | . /( − ) .

( , +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. 1Including 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 coeficients of the elements of . • All trailing coeficients 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

Definition 12. for all ∈ R.

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 efect 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 diferent guise. To understand this we shift attention to the geometric loci where nullification occurs, which we call curtains.

A variety ⊆ R is called a curtain if, whenever (, ) ∈ , then (, ) ∈ 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

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 ⊂ such that (, ) = 0 for all ∈ R.

R− 1 of such there exists no ∈ ∖{ }

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 suficient 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 efect 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 (, 22)-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.

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 efect 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?

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 Constraints, in: S. Dooley (Ed.), Proceedings ISSAC ’99, 1999, pp. 145–149. [6] S. McCallum, On Propagation of Equational Constraints in CAD-Based Quantifier Elimination, 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. thesis, 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 Decomposition, 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.

References

[1] G. Collins , Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition , 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 , University 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 Equational Constraints , in: J. Davenport , M. England , A. Griggio , T. Sturm , C. Tinelli (Eds.),