The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational efort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.
The cylindrical algebraic decomposition (CAD) method enables reasoning about formulas in real
algebra and is implemented in various tools for quantifier elimination like QEPCAD [
The CAD method decomposes the real space into a finite number of connected sets (called cells) such
that the input set of polynomials have invariant sign in each cell. Although such a decomposition allows
for reasoning about the formula, it is usually finer than needed for the task at hand. Algorithms like
NLSAT [
More specifically, the CAD algorithm iteratively computes projection polynomials to eliminate variable
by variable. These consist of resultants, discriminants, and (leading) coeficients which are selected to
maintain the delineability of the polynomials, a property which allows for work at a sample point to
be generalized to a wider cell. The single cell construction [
This paper investigates when we can go further and leave out leading coeficients from the projection.
Towards this goal, in prior theoretical work, we proposed to relax delineability to projective
delineability [
We introduce key background following [
Let N, N>0, Q, and R denote the sets of all natural (incl. 0), positive integer, rational, and real numbers respectively. For , ∈ N with < , we define [..] = {, . . . , } and [] = [1..]. For , ∈ N>0, ≤ and ∈ R, we denote by the -th component of and by [] the vector (1, . . . , ). Let , : → and let < be a total order on and ∼∈ {<, =, ̸=} . We write ∼ on if () ∼ () for all ∈ . Note that ̸= on is not “not = on ”.
We work with the variables 1, . . . , with ∈ N>0 under a fixed ordering 1 ≺ 2 ≺ ... ≺ . A polynomial is built from a set of variables and numbers from Q using addition and multiplication. We use Q[1, . . . , ] to denote multivariate polynomials in those variables. A polynomial is of level if is the largest variable in with non-zero coeficient.
Let ∈ [] and , ∈ Q[1, . . . , ] of level . For ∈ [] and = (1, . . . , ) ∈ R we write (, +1, . . . , ) for the polynomial after substituting 1, . . . , for 1, . . . , in and indicating the remaining free variables in . We use rroots() ⊆ R to denote the set of real roots of , deg () to denote the degree of in , coeff () for the set of coeficients of in , ldcf () for the leading coeficient of in , disc () to denote the discriminant of with respect to , and res (, ) to denote the resultant of and with respect to . Let ∈ R−1 , then is nullified on if (, ) = 0.
A constraint ∼ 0 compares a polynomial ∈ Q[1, . . . , ] to zero using a relation symbol ∼∈ {=, ̸=, <, >, ≤, ≥} , and has solution set { ∈ R | () ∼ 0} . A subset of R for some ∈ [] is called semi-algebraic if it is the solution set of a Boolean combination of polynomial constraints. A cell is a non-empty connected subset of R for some ∈ []. A cell is called simply connected if any loop in can be continuously contracted to a point. A polynomial ∈ Q[1, . . . , ] is sign-invariant on a set ⊆ R if the sign of () is the same for all ∈ .
Given , ∈ N>0 with < , we define the projection of a set ⊆ R onto R by [] = {(1, . . . , ) | ∃+1, . . . , . (1, . . . , ) ∈ }. Given a cell ⊆ R , ∈ [] and continuous functions , : → R, we define the sets × = {(, ()) | ∈ } and × (, ) = {(, +1) | ∈ , +1 ∈ ( (), ())} ( × (−∞, ), × (, +∞) analogously).
If ⊆ R is open, a function : → R is analytic if each component of has a multiple power
series representation around each point of . An -dimensional analytic submanifold of R is a
nonempty subset ⊆ R locally parametrized by coordinates through analytic functions : ⊆ R → R.
A function between analytic manifolds and ′ is analytic if locally it has an expression in (analytic)
coordinates which is analytic (see also [
The single cell construction [
Definition 2.1 (Delineability [
The are called real root functions of on . The sets × are called sections of over .
Analytic delineability is similar, but is a connected analytic submanifold of R and the real root functions are analytic.
The following gives a projection to obtain a cell where a polynomial is delineable. Theorem 2.1 (Delineability of a Polynomial [18, Thm. 2], [4, Thm. 3.1]). Let ∈ N, ⊆ R be a connected analytic submanifold, ∈ Q[1, . . . , +1] of level + 1. Assume that is not nullified at any point in , disc+1 () is not the zero polynomial and is order-invariant on , and ldcf+1 () is sign-invariant on . Then is analytically delineable on and is order-invariant on its sections over . Note that the discriminant of an irreducible polynomial is not the zero polynomial; in our algorithm, we replace each polynomial by its irreducible factors.
Root Orderings. Once we can describe the roots of individual polynomials by ordered root functions on the underlying cell, we can reason about intersections of graphs of root functions from diferent polynomials, e.g. ensure that two root functions remain in the same order on the underlying cell. Theorem 2.2 (Lifting of Pairs of Polynomials [21, Thm. A.1]). Let ∈ N, ⊆ R be a connected analytic submanifold, ∈ , and 1, 2 ∈ Q[1, . . . , +1] of level + 1. Assume 1 and 2 are analytically delineable on and res+1 (1, 2) is not the zero polynomial and is order-invariant on . Let 1, 2 : → R be real root functions of 1 and 2 on respectively, and ∼∈ {<, =} such that 1() ∼ 2(). Then 1 ∼ 2 on .
Note that the resultant of two coprime (and irreducible) polynomials is not the zero polynomial.
To maintain that two real root functions 1 and 2 stay in the same order on , we could also exploit
transitivity using another root function 3, e.g. 1 < 3 on and 3 < 2 on implies 1 < 2 on .
The work in [
Single Cell Construction. Given a set of polynomials ⊆ Q[ 1, . . . , ] and a sample ∈ R, we
compute and sort the real roots of ([−1] , ), ∈ . We determine the greatest root ℓ ∈ R below
(or equal to) and the smallest root ∈ R above (or equal to) . If they do not exist, we use −∞
and +∞ respectively. We now aim to describe the bounds of the cell ′ ⊆ R to be constructed by
root functions of some polynomials in ; for that, we assume that all polynomials in are delineable
on the underlying cell = [′−1] . Let ℓ and be real root functions of polynomials in such that
ℓ([−1] ) = ℓ and ([−1] ) = . The bounds on are described by the symbolic interval ( ℓ, )
(whose bounds depend on 1, . . . , −1 ) if ℓ([−1] ) < ([−1] ) or ℓ if = ℓ = . Now, we use
root orderings to make sure that ℓ < on (if applicable) and each ∈ is sign-invariant in
× ( ℓ, ) resp. × ℓ:
Theorem 2.3 (Root Ordering for Sign Invariance [
• If ℓ < on , and for each real root function of on it holds ∼ ℓ on for some ∼∈ {<, =} or ∼ on for some ∼∈ {<, =}; then is sign-invariant on × ( ℓ, ). • If for each real root function of on it holds ∼ on for some ∼∈ {<, =} ; then is sign-invariant on × (−∞, ). • If for each real root function of on it holds ∼ ℓ on for some ∼∈ {<, =} ; then is sign-invariant on × ( ℓ, +∞). • If for each real root function of on it holds either < ℓ on , or ℓ < on , or = ℓ on ; then is sign-invariant on × ℓ.
• If there is no real root function of on ; then is sign-invariant on × R.
The single cell construction is given in Algorithm 1. In Algorithm 1, we determine witnesses for the
real root functions of a polynomial of level on (the underlying cell to be constructed). Given some
∈ N>0, an indexed root is a partial function root, : R → R that maps ∈ R−1 to the -th real root
of (, ) if it exists. Given a cell ⊆ R −1 where is delineable, then root, coincides with the root
function from the above definition on . We thus can evaluate the function computationally by real
root isolation. Beginning from Algorithm 1, we compute projection polynomials whose order-invariance
on the underlying cell = I1 × · · · × I −1 (computed in the following iterations) maintain the desired
properties of the polynomials in . In Algorithm 1 the algorithm might fail, as McCallum’s projection
operator cannot reason about cells where a polynomial is nullified [
Example 2.1. Consider the polynomials 1 = 0.51 + 0.5 − 2, 2 = 21 + 22 − 1 , 3 = 0.51 − 0.5 − 2, 4 = − 12 − 0.75 as depicted in Figure 1, along with the sample point = (0.25, −0.7) and a cell as constructed using Algorithm 1.
Algorithm 1: single_cell_construction( ,)
Input : finite ⊆ Q[ 1, . . . , ], ∈ R
Output : Symbolic intervals I1, . . . , I for 1, . . . , describing a sign-invariant cell for containing 1 foreach = , . . . , 1 do 2 := { ∈ | is of level }, := ∖ 3 determine the set of indexed roots Θ = { 1, . . . , } of all ∈ that are defined at [−1] such that := ∪ {res (, ′) | (root,, root′,′ ) ∈ ⪯} choose ⪯ ⊆ Θ 2 s.t. its reflexive and transitive closure ⪯ is a partial order on Θ with ℓ ⪯ (if I = ( ℓ, )) and ensures sign-invariance of each ∈ by Theorem 2.3 // Theorem 2.2 p4 2 p1 x p3
p2 p5 p7 p6 x1 p7 p5
The algorithm adds coeficients and discriminants to guarantee delineability of these polynomials; in this case, we add 5 = disc2 (2) and 6 = ldcf2 (4) (the others are trivial). Further, as the cell is described by I2 = (root22,1, root32,1) on level 2 we aim to maintain root42,1 < root22,1 on , root22,1 < root32,1 on , root32,1 < root12,1 on , and root32,1 < root22,2 on . We thus add the corresponding resultants, of which only 7 = res2 (2, 3) is non-trivial. On level 1, we determine I1 = (root61,1, root51,2) as describing the interval.
We now summarize the theory of projective delineability introduced in [
Real Projective Line. Roughly speaking, the real projective line P is defined by adding a single point ∞ to the real line, so P = R ∪ {∞}. We can add more structure to P or visualize it by using alternative definitions: identifying the real number with the line = and ∞ with = 0, we see that the real projective line P is the set of lines of R2 passing through the origin. Such a line is determined by 3
1 (− 1+22 , − 1+22 ) = (, ) (, 1) 2 any of its non-zero vectors (, ) ∈ R2 or by any of its non-zero multiples, so if we denote by ( : ) the set (equivalence class) of such vectors, we have P = {( : ) : (, ) ∈ R2 ∖ {(0, 0)}}. This set identifies with R ∪ {∞} by mapping ( : ) to if ̸= 0 and to ∞ otherwise. Finally, P identifies with a circle (as an analytic manifold). Possible identifications are visualized in Figure 2.
As P identifies with a circle, we cannot use a linear order on P; however, P has a cyclic ordering that extends the usual order on R, as intuitively given in Figure 2. For distinct 1, 2, 3 ∈ P, we use [1, 2, 3] to denote that “after 1, one reaches 2 before 3” in that cyclic ordering on P. We use [1, . . . , ] for > 3 to denote ∀ < ′ < ′′ ∈ []. [ , ′ , ′′ ].
Projective Roots. The introduction of the projective line enables us to handle roots at infinity of (univariate) polynomials, and their multiplicities (see [19, Defn. 2, 3 and 5]): if ∈ Q[] has degree less than or equal to ∈ N, we associate with the homogeneous bivariate polynomial () (also called a binary form of degree ) defined by ()(, ) = ( ). The concepts of roots and multiplicities are well-defined for binary forms, and we thus import them for polynomials: ( : ) ∈ P is a projective root of multiplicity of with respect to if (, ) is a root of () with multiplicity .
The set of projective roots of (with respect to ) splits into the real roots on the one hand and the root at infinity on the other hand (see [19, Lemmas 2 and 3]): ( : ) ∈ P is a projective root of of multiplicity w.r.t. if and only if either ̸= 0 and is a real root of multiplicity or = 0 and = − deg().
Projective Delineability. We finally formalize the notion of projective delineability, by transferring the concept of projective roots to multivariate polynomials.
Definition 3.1 (Projective Delineability [19, Defn. 11]). Let ∈ N, ⊆ R be a cell, and ∈ Q[1, . . . , +1] ∖ {0}. The polynomial is called projectively delineable on if there exist continuous functions 1, . . . , : → P (for ∈ N) such that: • for any point in , the values of 1, . . . , are distinct; • the projective roots of the univariate polynomial (, +1) with respect to deg+1 () are 1(), . . . , () for all ∈ ; and • there exist constants 1, . . . , ∈ N>0 such that for all ∈ and all ∈ [], the multiplicity of the root () of (, +1) w.r.t. deg+1 () is .
The are called projective root functions of on . The cells × , ∈ [] are called projective -sections over .
Analytic projective delineability is similar, but is a connected analytic submanifold of R and the projective root functions are analytic.
x1 (a) Variety of in R2.
(b) Variety of in R×P . The black line marks the points at ∞.
In particular, the first condition means the function values as points around the unit circle maintain a cyclic ordering. Figure 3 illustrates an example of a polynomial that is projectively delineable.
The central theorem for this work states that order-invariance of the discriminant plus nonnullification is enough to guarantee projective delineability, with no need to maintain the sign-invariance of the leading coeficient. Note that the theorem requires the underlying cell to be simply connected, which is stronger than connectedness. This assumption is always met for locally cylindrical cells, since they are homeomorphic to open cubes of Euclidean spaces [3, Proposition 5.3] (which are simply connected).
Theorem 3.1 (Projective Delineability [19, Thm. 2]). Let ∈ N, ⊆ R be a simply connected analytic submanifold, and ∈ [1, . . . , +1] of level +1. If is not nullified on any point in and disc+1 () is not the zero polynomial and is order-invariant on , then is analytically projectively delineable on and is order-invariant in each projective -section over .
Delineability is guaranteed by projective delineability plus sign-invariance of the leading coeficient. Lemma 3.1 (Delineability and Projective Delineability [19, Cor. 1]). Let ∈ N>0, ⊆ R be connected, and ∈ Q[1, . . . , +1] of level + 1. Assume that is projectively delineable on , and ldcf+1 () is sign-invariant on . Then is delineable on .
The definition of projective delineability is equivalent to delineability over cells where the polynomial does not have any roots. In those cases, we can guarantee delineability without sign-invariance of the leading coeficient.
Lemma 3.2. Let ∈ N>0, ⊆ R , ∈ , and ∈ Q[1, . . . , +1] of level + 1. If is projectively delineable on , ldcf+1 ()() ̸= 0, and rroots((, +1)) = ∅, then is delineable on . Proof. Let 1, . . . , be the projective -sections over . If ldcf+1 ()() ̸= 0, then it holds deg+1 ((, +1)) = deg+1 (), thus the projective roots (, +1) are all real. Thus { 1(), . . . , ()} = rroots((, +1)) = ∅, and it follows = 0. It follows that (, +1) ̸= 0 for all ∈ , and thus is delineable on .
Root Orderings. As single cell construction relies on root orderings, we give the analogous statement for projective delineability. Note that in contrast to Theorem 2.2, we can only ensure that two root functions are disjoint or equal.
Theorem 3.2 (Lifting of Pairs of Polynomials [19, Theorem 3]). Let ∈ N, ⊆ R be a connected analytic submanifold, ∈ , and 1, 2 ∈ Q[1, . . . , +1] of level + 1. Assume 1 and 2 are analytically 2 x 2 1 x1 (a) The cell which we aim to construct. projectively delineable on and res+1 (1, 2) is not the zero polynomial and is order-invariant on . Let 1, 2 : → P be real projective root functions of 1 and 2 respectively, and ∼∈ {=, ̸=} such that 1() ∼ 2(). Then 1 ∼ 2 on . 4. Projective Delineability in Single Cell Construction We motivate the use of projective delineability by considering Example 2.1 again.
Example 4.1. The singularity of 4 (witnessed by its leading coeficient) was a boundary to the cell in Figure 1, but crossing that boundary does not change the sign of any input polynomial. Figure 4a shows the cell that we aim to construct instead: if we detect that the singularity of 4 does not afect the cell, we can omit the leading coeficient of 4 and build the enlarged version.
For this reasoning, we view the roots of the polynomials in the projective real line, as depicted in Figure 4b, where intuitively −∞ and +∞ are identified with the same point ∞. Above the singularity of 4, the two distinct root functions of 4 coincide at the point ∞, and thus can be described as a unique real projective root function of 4. The order-invariance of the discriminant of 4 ensures that the variety of 4 can be described using such projective root functions (Theorem 3.1). Now, by adding the resultant of 2 and 4, we ensure that the mentioned root function does not intersect the circle, and thus does not enter the cell (Theorem 3.2). By projective delineability of 4, we know that there are no other roots (Definition 3.1), and we thus can omit the leading coeficient from our projection polynomials.
We modify the single cell construction algorithm as follows. We still describe the cell boundaries using real root functions, as we can encode them using indexed roots which we can evaluate in a straightforward way. Thus, their defining polynomials are still required to be delineable. For the other polynomials, however, we only maintain projective delineability, and hence allow their roots to go through the point at ∞. We thus need to adapt Theorem 2.3, as a root function may not stay below (above) the lower (upper) bound even if it does not cross it by going through ∞.
Theorem 4.1 (Projective Root “Ordering” for Sign Invariance). Let ∈ N, ⊆ R be connected, ∈ , and , ℓ, ∈ Q[1, . . . , +1] of level + 1. Assume that is projectively delineable on , ℓ, are delineable on . Let ℓ, : → R be real root functions of ℓ and on respectively. • If ℓ < on , and for each projective root function of on either = ℓ on , = on , or ℓ ̸= ̸= on and [ ℓ(), (), ()]; then is sign-invariant on × ( ℓ, ). • If for each projective root function of on either = on , or ∞ ̸= ̸= on and [∞, (), ()]; then is sign-invariant on × (−∞, ).
(a) Resultant with bounds.
(b) Resultants computed anyway. (c) Cell defined by single polynomial. (d) Exploiting transitivity. (e) Adding the leading coeficient.
(f) Combining the previous two ideas.
• If for each projective root function of on either = ℓ on , or ℓ ̸= ̸= ∞ on and [(), ℓ(), ∞]; then is sign-invariant on × ( ℓ, +∞). • If for each projective root function of on either ̸= ℓ on , or = ℓ on ; then is sign-invariant on × ℓ.
• If there is no projective root function of on ; then is sign-invariant on × R.
Example 4.2. This theorem only allows to omit leading coeficients if the interval is bounded in both directions (otherwise we need the leading coeficient for preventing crossing ∞) and the resultant of the polynomial with the polynomials defining the lower and upper bound are computed: e.g. we can omit the leading coeficient of blue polynomial in Figure 5a (which we would add for its delineability in the classical setting) by additionally adding the resultant of the blue and red polynomial (which is not added in the classical setting). The trade-of may not be attractive; but if the polynomial has a root below and above the cell at the current sample point (e.g. Figure 5b), or if both bounds are defined by the same polynomial (e.g. Figure 5c), this would not require additional resultants.
The single cell construction allows for flexibility for diferent sets of resultants to maintain signinvariance by exploiting the transitivity of root orderings. In the projective real line, there is only a cyclic ordering. The following insight transfers the idea to the new setting.
Lemma 4.1 (Transitive Projective Root “Ordering”). Let ∈ N, ⊆ R be connected, ∈ , 1, 2, 3, 4 : → P be continuous. Assume that [ 1(), 2(), 3(), 4()] and 1 ̸= 2 ̸= 3 ̸= 4 ̸= 1 on . Then 1 ̸= 3 on .
Example 4.3. Consider a projective root (as depicted in blue in Figures 5d to 5f) that is below the symbolic interval at the current sample point. Preventing the root from crossing the lower bound is analogous to the case of regular delineability. However, we now also need to prevent it to cross the upper bound; for that, we now have three options. (1) We compute a chain of resultants that maintain a cyclic ordering of the given root, the upper bound and some roots in between (in the cyclic sense), exploiting Theorem 3.2 (in Figure 5d, by adding the resultants of the blue with the purple and magenta polynomials respectively, its root is trapped between the other; additionally, we add the resultant of the purple with the red one, and of the magenta with the green). (2) We add the leading coeficient of the defining polynomial to the projection, avoiding the intersection of the root with ∞, thus making it delineable using Lemma 3.1 (see Figure 5e). (3) We mix the two approaches, e.g. for some polynomial in the chain maintaining the cyclic ordering, we add its leading coeficient to avoid crossing ∞ (in Figure 5f, like (1) the blue root is trapped between the magenta and purple, however, instead of the resultant of the purple and red polynomials, we add the leading coeficient of the purple).
To summarize, we replace Lines 9 to 14 of Algorithm 1 by Algorithm 2. We maintain projective delineability for each polynomial (Algorithm 2) using Theorem 3.1, and delineability using Lemma 3.1 for polynomials defining the bounds (Algorithm 2) and for polynomials without roots (Algorithm 2) where we make use of the optimization by Lemma 3.2 to omit leading coeficients. In Algorithm 2, we determine a relation for maintaining sign-invariance of polynomials (Theorem 4.1), where we may exploit transitivity (using Lemma 4.1), now maintaining a cyclic ordering. The relation involves ∞ to enable the choice of adding leading coeficients (Algorithm 2) using Lemma 3.1 instead of resultants (Algorithm 2) using Theorem 3.2.
We now elaborate how me make determine the ordering in Algorithm 2, exploiting the options
elaborated in Example 4.3. [
We implemented our single cell construction algorithm based on the proof system described in [
We conduct our experiments on Intel®Xeon®8468 Sapphire CPUs with 2.1 GHz per core, testing upon the SMT-LIB QF_NRA benchmark set [22] which contains 12 154 instances. We use a time limit of Algorithm 2: Modifications of single_cell_construction 9 foreach ∈ do 10 if ([−1] , ) = 0 then return FAIL 11 := ∪ {} for some ∈ coeff () such that () ̸= 0 12 := ∪ {disc ()} 13 := ∪ {ldcf (ℓ), ldcf ()} where ℓ, define I 14 foreach ∈ s.t. rroots(([−1] , )) = ∅ and ldcf () ̸= 0 do 15 := ∪ {ldcf ()} // proj. delineability, Theorem 3.1 // del., Lemma 3.1
// Lemma 3.2 // delineability, Lemma 3.1 16 choose symmetric ̸≈ ⊆ (Θ ∪ {∞}) 2 that ensures ℓ ̸= (if I = ( ℓ, )) and sign-invariance of each ∈ by
Theorem 4.1, using “transitivity” by Lemma 4.1 17 := ∪ {res (, ′) | (root,, root′,′ ) ∈ ̸≈} // Theorem 3.2 18 := ∪ {ldcf () | (root,, ∞) ∈ ̸≈} // Lemma 3.1 60 seconds and a memory limit of 4 gigabytes. The code, instructions for reproducing and raw results are available at: https://doi.org/10.5281/zenodo.14900915.
Overall Results. The number of solved instances is reported in Table 1, showing that the use of
projective delineability does not greatly afect which problems are tractable within the time limit. The
actual running times are depicted in Figure 6a: they show similar performance of the modified and
baseline versions on the majority of instances, but significantly diferent behaviour on some instances.
The diferences largely even out over the whole benchmark set (a typical picture for changes to the
projection heuristics in our experience). Nevertheless, it is clear that many instances do benefit from
projective delineability. Identifying a criterion to predict whether the optimization pays of a priori is
desirable (a machine learning based approach may be possible [
In the remainder of this section we compare the behaviour of BC and BC-PD variants to better understand these results.
Number of Applications. The results may suggest that the optimization from projective delineability is only applied in very rare cases, but this is not the case. Considering the instances solved by BC-PD: in total, the leading coeficient can be omitted for 307 822 polynomials, while for 826 795 polynomials, the optimization cannot be applied as the cell is unbounded in some direction, and for 4 089 polynomials, the optimization cannot be applied as it does not have a root on both sides of the bounds, or we did not ifnd an appropriate resultant that may replace the leading coeficient. The optimization is thus applied in a substantial 37% of the cases. However, we also need to add a coeficient for each polynomial to ensure its non-nullification: if we add the leading coeficient, this sufices in most of the cases. Still, if it is omitted, we may choose another coeficient which is potentially simpler (e.g. of lower degree, fewer variables, etc) that the leading coeficient. We thus investigate whether this choice has an impact on another metric.
Quality of Cells. A good indicator for the quality of the generated cells is their size, which may be indirectly measured by the number of cells constructed (Figure 6b). By leaving out leading coeficients, we also hope to decrease the number of projection polynomials (Figure 6c). By choosing “simpler” coeficients than the leading coeficients (in terms of a lower degree), we aim to reduce the degree of the computed polynomials (not depicted in Figure 6 as there is no visible diference between the variants) and indirectly the number of computed roots (Figure 6d). However, all these measures do not seem to difer significantly in aggregate between the baseline and modified variants. An explanation could be that the (degree of the) leading coeficients do not carry much weight, or that the alternative coeficients are not much simpler.
Role of Projection Polynomials. To address the latter hypothesis, we compare the impact of the diferent projection polynomials (resultants, discriminants, and (leading) coeficients). On the 10 157 instances solved by BC-PD, of the time spent on algebraic computations, 55% is spent on computing discriminants and 5% is spent on computing resultants, and almost no time is spent on computing coeficients. Regarding the polynomials with a maximum total degree of the ones occurring in an
solved by no variant solved by BC/LDB but not by BC-PD/LDB-PB solved by BC-PD/LDB-PB but not by BC/LDB solved by both variants
BC
LDB D P BC2000 0 ⊥
0 D CP-15k B 0 0 0 20 40 BC instance, in 15% of the instances, that polynomial is a discriminant, in 30% of the instances, that polynomial is a resultant, and in only 3% of the instances, that polynomial is a coeficient. Both measures show that the coeficients have a minor impact on the complexity of the projection.
We provided a first application for the notion of projective delineability recently introduced in [
Our experimental evaluation shows the resulting optimization is applied in many cases, however, these do not translate to significant improvements in terms of running times or quality of intermediate results, as other projection polynomials play a greater role for the computational efort. That is the case when viewing the dataset as a whole: we have found many individual instances that benefit from the optimisation bringing further the future research question of how to recognise this in advance. Also in future work, further symbiotic optimizations may lead to practical improvements, such as reducing the amount of coeficients required for maintaining non-nullification of polynomials.
No generative AI was used.