Cylindrical Algebraic Decomposition (CAD) by projection and lifting requires many iterated univariate resultants. It has been observed that these often factor, but to date this has not been used to optimise implementations of CAD. We continue the investigation into such factorisations, writing in the specific context of SC2. 8th International Workshop on Satisfiability Checking and Symbolic Computation, July 28, 2023, Tromsø, Norway, Collocated with ISSAC 2023 $ masjhd@bath.ac.uk (J. H. Davenport); Matthew.England@coventry.ac.uk (M. England) https://people.bath.ac.uk/masjhd (J. H. Davenport); https://matthewengland.coventry.domains (M. England) 0000-0002-3982-7545 (J. H. Davenport); 0000-0001-5729-3420 (M. England) © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CPWrEooUrckResehdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g CEUR Workshop Proceedings (CEUR-WS.org)
The resultant of two polynomials is a polynomial formed of their coeficients that is equal to
zero if and only if the two original polynomials have a common root. Resultants are a widely
used tool in symbolic computation, and in satisfiability checking over non-linear arithmetic.
In particular, they are a key ingredient of Cylindrical Algebraic Decomposition (CAD) [
[1, pp. 177–178] suggests that iterated resultants, where there are “common ancestors” tend
to factor. This was apparently responded to by van der Waerden in a letter [
The purpose of this paper is to look at the connections of results on such factorisations with
Cylindrical Algebraic Decomposition (CAD) [
For CAD, we assume that we are constructing a CAD for a specific Boolean formula Φ , rather than just a set of polynomials. For CAC, we again assume we are looking for SAT/UNSAT for a specific Boolean formula Φ .
We are grateful to [
Now consider the case in which we have homogeneous polynomials in the same number
of variables. Let 1, . . ., be generic homogeneous forms in 1, . . ., of positive total
degrees 1, . . ., . That is, every possible coeficient of each is a distinct indeterminate, and
the set of all such indeterminate coeficients is denoted by . Let denote the ideal of inertia
forms for 1, . . ., . Proofs of the following two propositions may be found in [
Proposition 2. [10, Proposition 6] The vanishing of for particular 1, . . ., with coeficients in a field is necessary and suficient for the existence of a non-trivial zero of the system 1 = 0, . . ., = 0 in some extension of .
The above considerations also lead to the notion of a resultant of non-homogeneous
polynomials in − 1 variables. For a given non-homogeneous (1, . . ., − 1) over of total
degree d, we may write = + − 1 + · · · + 0, where the are homogeneous of degree .
Then is known as the leading form of . Recall that the homogenization (1, . . ., ) of
is defined by = + − 1 + · · · + 0 . Let 1, . . ., be particular non-homogeneous
polynomials in 1, . . ., − 1 over of positive total degrees , and with leading forms , .
We set res(1, . . ., ) = res(1, . . ., ) , where is the homogenization of . Then we have
the following (see proof in [
Proposition 3. [10, Proposition 7] The vanishing of res(1, . . ., ) is necessary and suficient for either the forms , to have a common nontrivial zero over an extension of , or the polynomials to have a common zero over an extension of .
Observe that the common zeros of the correspond to the afine solutions of the system, whereas the nontrivial common zeros of the leading forms correspond to the projective solutions on the hyperplane at infinity.
Consider these polynomials: = 2 + 2 + + − 1, = − 2 + 2 + 2 − 1, ℎ = 2 + + .
Under variable ordering ≻ ≻ we may calculate the iterated resultant: res(res(, ), res(, ℎ)) = 58 + 167 + 146 − 124 −
83 + 32 + 2 25 −
⏟ = (︀ 53 + 62 − 3 − 2︀) (︀ 2 + + 1)︀ (︀ 2 + − 1 ︀) spurio⏞us genu⏞ine We define the meaning of the labels below. An alternative computational path may have calculated similarly
res(res(, ), res(, ℎ)) = The final choice would have been to calculate, 58 + 167 + 186 + 85 − 54 −
83 − = (︀ 2 + + 1)︀ (︀ 2 + − 1︀) (︀ 54 + 63 + 2 − 1︀) .
22 + 1 genu⏞ine ⏟ spurio⏞us res(res(, ℎ), res(, ℎ)) = = 24 + 43 + 22 − 2 2 ︀( 2 + + 1)︀ (︀ 2 + − 1︀) .
⏟
genu⏞ine ⏟ ⏟ Up to constants (3) divides (2) and (1), but this need not happen in general. What does happen in general is that, if we consider a Gröbner Basis,
Basisplex(, , ℎ) = {︀ 4 + 23 + 2 − 1, − , 2 + + }︀ , then we see that the basis polynomial in only divides all three iterated resultants and in fact is res(, , ℎ) in the sense of §2. In this example, it is also (3), but again this need not happen in
The labels above are made in regards to the roots of the tagged resultant factors. The roots of general. the part we have labelled as “genuine” are
{ : ∃∃ (, , ) = (, , ) = ℎ(, , ) = 0}, whereas the roots of the part we have labelled as “spurious” are
{ : ∃ (∃1 (, , 1) = (, , 1) = 0 ∧ ∃2 ̸= 1 (, , 2) = ℎ(, , 2) = 0)} . They are “spurious” in the sense that they do not go on to form true triple roots. Nevertheless, they are values above which the topology changes, so they cannot always be discarded. Note that §2 implies that there is always a neat factorisation (over Z if that was the original ring) into “genuine” versus “spurious”. . (1) (2) (3) (4) (5) (6) res(res(, ), res(, ℎ)) = (2 − 1)2, res(res(, ), res(, ℎ)) = (2 − 1)4, res(res(ℎ, ), res(, ℎ)) = (2 − 1)4, and
Basisplex(x,y,z)(, , ℎ) = {︀ 2 − 1, 2 + + , − ︀} .
I.e. no spurious roots were uncovered with this ordering. The question of CAD variable ordering
is well studied and known to greatly efect the complexity of CAD both in practice [
What happens if we take the variables in a diferent order? In ordering ≻ ≻ we have: (7) (8) (9) (10) (12)
This section is not a complete classification on when spurious factors may be discarded, but it is a start.
McCallum [
But since 1 = 0 and 2 = 0, we know that res (1, 2) = 0 also. Hence all the res (1, ) are equational constraints in 1, . . . , − 1. Thus the next projection is
res− 1 (res (1, 2), res (1, )), res− 1 (res (1, 2), disc ()) and numerous discriminants.
In this case, we are only interested in the genuine zeros, as away from these the formula will be uniformly false and thus further refinement is unnecessary. So we can replace (12) by res(1, 2, ).
If the have degree in each , then the equivalent of (12) after eliminations (i.e.
eliminating all equational constraints) has degree (︀ (2)2 )︀ (doubly exponential), whereas
res(1, . . . , ) has degree (︀ )︀ (the Bézout bound). We note that [
Though it would have to be proved, it seems very likely that the same conclusions would
apply to equational constraints with the Lazard projection [
Φ ≡ 1 = 0 ∧ 2 = 0 ∧ · · · = 0 ∧ Φ( +1, . . . , ).
(11)
In CAC [
We would need to work this through precisely with an implementation of CAC, which has yet to be done.
In the examples above the factors were marked as “spurious” or “genuine” via manual analysis to see if the roots of the factors led to common zeros or not. Are there alternatives to such manual detection?
We note that in some cases we can discard factors with based on their degree, when this breaches the Bézout Bound on the true multivariate resultant. I.e., if res(res(, ), res(, ℎ)) has an irreducible factor of degree > 3, it must be spurious and can be discarded. Since it is common for CAD implementation to factor polynomials, this is a cheap, if incomplete, test. Example 1. For example, the following three 3-variable polynomials were created randomly in Maple to have total degree 5: = − 3423 − 205 + 722 − 433 + 63 + 16, = 134 − 274 − 212 + 30 − 42 − 81, ℎ = − 654 + 135 + 303 + 173 + 25 + 78.
Then ((, ), (, ℎ)) factors into a constant times two irreducible polynomials: one of degree 378 and the other of degree 89. With no further computation we can identify the first as spurious since its degree is greater than 53 = 125. The second could be genuine, or be another spurious factor: we may check manually that it is indeed genuine.
In an example where we have multiple factors below the bound we could work through them in turn keeping count of the sum of degrees of genuine factors as we uncover then, in each case reducing the degree bound accordingly for any further factors to be investigated as genuine.
There is much to be done to develop these ideas.
1. In §4.1, we have only looked at the resultants, not the discriminants, and indeed only at resultants of resultants. Undoubtedly something similar can be said about, for example res(res(, ), disc( )), (13) but we have not explored this fully yet. We observe that, in the case of the polynomials from Example 1, (13) is a perfect square, and this seems to be true in general. We would need a complete solution for resultants of discriminants, discriminants of resultants and discriminants of discriminants in order to need to remove the caveat in italics towards the end of §4.1. 2. As stated in §4.2, the “genuine parts of resultants” idea would need to be worked through an implementation of CAC. 3. If we look at (3), we see that this polynomial, which is the “genuine” part, factors further, and one factor has no real roots. Hence this factor can be discarded, though there is not much benefit, since we are at the univariate phase. Nevertheless, this shows that even the “genuine” part may still be overkill for real geometry. Can we a) detect that a factor of a resultant etc. has no real components; and b) use this to further reduce the polynomials? Furthermore, c) can we make any meaningful statement about the complexity implications of this?
Both authors are supported by the UK’s EPSRC, via the DEWCAD Project, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition; grant numbers EP/T015713/1 and EP/T015748/1.
We are also grateful to Gregory Sankaran and Ali Uncu for many useful conversations.