Experience with Heuristics, Benchmarks &
        Standards for Cylindrical Algebraic Decomposition

                                                 Matthew England∗ , and James H. Davenport† ,
                    ∗ Coventry University Faculty of Engineering, Environment and Computing, Coventry, CV1 2JH, U.K.

                                                 Email: Matthew.England@coventry.ac.uk
                                     † University of Bath Department of Computer Science, Bath, BA2 7AY, U.K.

                                                     Email: J.H.Davenport@bath.ac.uk

         Abstract—In the paper which inspired the SC2 project,              we note that the solve procedures in Computer Algebra Sys-
     [E. Ábráham, Building Bridges between Symbolic Computation and       tems are really meta-algorithms: algorithms to select specific
     Satisfiability Checking, Proc. ISSAC ’15, pp. 1–6, ACM, 2015] the      procedures to use based on problem parameters. Although
     author identified the use of sophisticated heuristics as a technique   the individual procedures are usually well documented within
     that the Satisfiability Checking community excels in and from          the scientific literature we are not aware of any publications
     which it is likely the Symbolic Computation community could
                                                                            describing these meta-algorithms.
     learn and prosper. To start this learning process we summarise
     our experience with heuristic development for the computer                 Another topic where Symbolic Computation might benefit
     algebra algorithm Cylindrical Algebraic Decomposition. We also         from experience in Satisfiability Checking is standards and
     propose and discuss standards and benchmarks as another area           benchmarks. Competitions based on these form an integral
     where Symbolic Computation could prosper from Satisfiability
                                                                            part of the Satisfiability Checking community, and may have
     Checking expertise, noting that these have been identified as
     initial actions for the new SC2 community in the CSA project,          contributed to the remarkable progress made in practical al-
     as described in [E. Ábráham et al., SC2 : Satisfiability Checking    gorithms. The lack of a comparable focus for the Symbolic
     meets Symbolic Computation (Project Paper), Intelligent Computer       Computation community was acknowledged in [2]. However,
     Mathematics (LNCS 9761), pp. 28–43, Springer, 2015].                   recent experiments have suggested the benchmarks for non-
                                                                            linear real arithmetic are insufficient and the development of
                               I.    I NTRODUCTION                          new standards and benchmarks for the joint community has
                                                                            been identified as a key SC2 project action in [2, Section 3.3].
         This article is inspired by the SC2 project1 , a new initiative
     to forge a joint community from the existing fields of Symbolic            In the present paper we outline our experience of these
     Computation and Satisfiability Checking. For further details           issues for a single Symbolic Computation algorithm, Cylindri-
     on the project we refer the reader to:                                 cal Algebraic Decomposition (CAD). The aim of the paper is
                                                                            to instigate the learning process from the Satisfiability Check-
         •      [2] which introduced the two fields, describes some         ing community by illustrating the current use of heuristics,
                of the challenges and opportunities from working            benchmarks and standards in (at least one area of) Symbolic
                together, and outlines planned project actions; and         Computation and posing some questions. We start with a
                                                                            summary of the necessary background on CAD in Section II,
         •      [1] the accompanying paper to an invited talk at
                                                                            then survey work with heuristics in CAD in Section III and
                ISSAC 2015 which inspired the creation of the new
                                                                            our experience with standards and benchmarks in Section IV.
                project and community.
                                                                            We finish with conclusions and questions in Section V.
     Within [1] the author outlines the strengths and weaknesses of
     the two communities, writing in the introduction:                            II.   C YLINDRICAL ALGEBRAIC DECOMPOSITION
             “Symbolic Computation is strong in providing pow-              A. Definition
             erful procedures for sets (conjunctions) of arithmetic             A Cylindrical Algebraic Decomposition (CAD) is a decom-
             constraints, but it does not exploit the achievements          position of Rn into cells (connected subsets). By algebraic
             in SMT solving for efficiently handling logical frag-          we mean semi-algebraic: i.e. each cell can be described with
             ments, using heuristics and learning to speed-up the           a finite sequence of polynomial constraints. Finally, the cells
             search for satisfying solutions.”                              are arranged cylindrically, meaning the projections of any
     By heuristic the we mean a practical method to make a choice           pair, with respect to the variable ordering in which the CAD
     which is not guaranteed to be optimal. Although Computer               was created, are either equal or disjoint. We assume variables
     Algebra Systems prize correctness and exact solutions there            labelled according to their ordering (so the projections con-
     is still much scope for the use of heuristics and statistical          sidered are (x1 , . . . , x` ) → (x1 , . . . , xk ) for k < `) with the
     methods in symbolic computation algorithms: both for tuning            highest ordered variable present said to be the main variable.
     how individual algorithm are run and for selecting a particular        Hence CADs can be represented in a tree like format branching
     algorithm to use in the first place. In regards to the latter point,   on the semi-algebraic conditions involving increasing main
                                                                            variable, as in the example below (with the branching from
                                                                                               √
       1 http://www.sc-square.org/                                          right to left; all     indicating the positive root; and the tuples




Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: E. Ábrahám, J. Davenport, P. Fontaine, (eds.): Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation (SC2 ),
Timisoara, Romania, 02-07-2016, published at http://ceur-ws.org
on the left sample points of the cells).                                   build CADs of increasing dimension. First a CAD of R1 is
                                                                          built by splitting on the real roots of the univariate polynomials
 
  (−2, 0)                                                     x < −1      (those in x1 only). Next, a CAD of R2 is built by repeating
                                                                           the process over each cell in R1 with the bivariate polynomials
 
 
 
 
                                                                           in (x1 , x2 ) evaluated at a sample point of the cell in R1 ; and
  
   (−1, −1)       y<0
 
 
                                                                           the process is repeated until a CAD of Rn is produced. We
 
 
     (−1,   0)     y  =0                                       x = −1
 
 
 
 
                                                                         call the cells where a polynomial vanishes sections and those
    (−1, 1)       0<y
                                                                           regions in-between sectors, which together form the stack over
 
 
 
 
                          √                                                the cell. In each lift we extrapolate the conclusions drawn from
 
 
  
     (0, −2)         y < −√−x2 + 1
 
 
 
  
                                                                          working at a sample point to the whole cell requiring validity
                                                                           theorems for the projection operator used.
  
   (0, −1)                     2
                √ y = − −x + √      1
 
 
 
     (0, 0)    − −x + 1√< y < −x2 + 1
                       2                                      −1 < x < 1       CAD cells are represented by at least a sample point (as
                    y√= + −x2 + 1
  
   (0, 1)                                                                 in the left of the example above), and an index: a list of
 
  
 
                                                                           positive integers with each integer indicating the section or
  
  (0, 2)              −x2 + 1 < y
 
  
 
 
 
                                                                          stack each variable is within (in reference to the ordered roots
 
                                                                         of the projection polynomials). Some implementations will
 (1, −1)
                y<0
 
                                                                          also encode the full algebraic description within each cell.
     (1,  0)     y=0                                           x=1
 
 
 
 
                                                                             CAD was originally introduced by Collins for quantifier
 
    (1, 1)      0<y
 
 
                                                                          elimination (QE) in real closed fields [4]. Although CAD con-
                                                                           struction has complexity doubly exponential in the number of
 
 
 
   (2, 0)                                                      1<x
 
                                                                           variables [26], applications range from parametric optimisation
                                                                           [34] and epidemic modelling [16], to reasoning with multi-
A CAD is produced to be invariant for input; originally sign-
                                                                           valued functions [24] and the derivation of optimal numerical
invariant for a set of input polynomials (so on each cell each
                                                                           schemes [33]. There have been many improvements to Collins’
polynomial is positive, zero or negative). The example above
                                                                           original approach most notably refinements to the projection
is a sign invariant CAD for the polynomial x2 +y 2 −1 defining
                                                                           operators [50] [10], [53]; early termination of lifting [22]
the unit circle. More recently CADs have been produced truth-
                                                                           [62]; and symbolic-numeric schemes [58], [42]. Some recent
invariant for input Boolean-valued polynomial formulae. A
                                                                           advances include dealing with multiple formulae [7], [8]; local
sign-invariant CAD for the polynomials in a formula is also
                                                                           projection [14], [60]; and decompositions via complex space
truth-invariant for the formula; but we can often achieve truth-
                                                                           [21], [6]. For a more detailed introduction to CAD see e.g. [8].
invariance with far less cells. For example suppose we need a
CAD truth-invariant for the formula
                                                                                          III.   H EURISTIC USE FOR CAD
            x2 + y 2 − 1 = 0 ∧ (x − 1)2 + y 2 − 1 = 0.                     A. Choosing the variable ordering
A sign-invariant CAD would require 55 cells (with the full                    The most well known choice required for CAD is that
dimensional ones shown on the left of Figure 1). However, a                of the variable ordering, which the cylindricity is defined
truth-invariant CAD would need only 7 cells: 2 of which are                with respect to. This determines the order in which variables
full dimension (as on the right of Figure 1) and 5 more to                 are eliminated during projection and the subspaces through
decompose the line x = 12 at the points of intersection.                   which CADs are built incrementally during lifting. When using
                                                                           CAD for QE we must project variables in the order they are
B. Computation                                                             quantified, but we are free to project the other variables in any
                                                                           order (and to change the order within quantifier blocks).
   CAD construction usually involves two phases. The first
projection, applies operators recursively on polynomials, start-               The variable ordering used can have a great effect on the
ing with the input. Each time the operator produces a set                  output produced. For example, let f := (x − 1)(y 2 + 1) − 1
with one less variable which together define the projection                and consider the minimal sign-invariant CAD in each variable
polynomials. These are used in the second phase, lifting, to               ordering, as visualised in Figure 2. In each case we project
                                                                           down with the left figure projecting x first and the right y.
                                                                           In this toy example the “wrong” choice more than doubles
                                                                           the number of cells, while numerous experiments have shown
                                                                           that for larger examples the choice can determine whether a
                                                                           problem is tractable (see for example the experimental results
                                                                           in [8]). At the extreme end of this observation, [15] defined
                                                                           a class of examples where changing variable ordering would
                                                                           change the number of cells required from constant to doubly
                                                                           exponential in the number of variables.
                                                                           Several heuristics have been developed to choose the variable
                                                                           ordering, including:
                                                                              Brown: Use the following criteria, starting with the first
Fig. 1.   Example visualising sign and truth-invariant CADs                          and breaking ties with successive ones:
            (1)Eliminate variable if lowest overall degree.          Booloean structure of a formula through the identification of
            (2)Eliminate variable if lowest (maximum) total          Equational Constraints (ECs): polynomial equations logically
              degree in terms in which it occurs.                    implied by a formula. Reduced projection operators (using a
        (3) Eliminate variable if smallest number of terms           subset of the usual polynomials) have been proven valid for use
              contains it.                                           when an EC is present with corresponding main variable [51],
           Suggested by Brown in [13, Section 5.2].                  [52]. Results in [29], [31] suggest that the double exponent
    sotd: For all admissible orderings, calculate the projec-        in the complexity bound decreases by 1 for each EC used,
           tion set and choose the one with smallest sum of          although this is restricted to primitive ECs meaning the classic
           total degrees for each of the monomials in each           lower-bound examples of [26], [15] are not violated [25].
           of the polynomials [27]. Performs well but more               These reduced operators can only use one EC for each
           costly than Brown. A greedy alternative is to             projection, so when there are multiple we must make a
           allocate one variable of the ordering at a time by        designation. Note that ECs need not appear explicitly as atoms
           projecting each unallocated variable and choosing         (formula with no logical connectives) in the input formula, but
           the one which increases the sotd least.                   could instead be implicit. For example, the resultant of any two
    ndrr: As with sotd construct the full projection set             ECs in the same main variable is itself an EC (not containing
           and choose the ordering whose set has the least           that variable) [52]. Propagating ECs in this way allows for the
           number of distinct real roots of the univariate           maximal use of the reduced operators. However, it can require
           polynomials within [9]. Even more costly than             multiple choices of which EC to designate at each projection.
           sotd, but sensitive to the real geometry and              Section 4 of [29] described such an example where the wrong
           shown to assist with examples where the sotd              designation could make add tens of thousands to the cell count
           heuristic failed.                                         of the final output, making it more than 15 times bigger.
The papers cited each contain experimental results demonstrat-           2) Making the designation: In [9] the authors experimented
ing their worth. In [39] the results of an experiment comparing      in using the sotd and ndrr measures on this question (the
the 3 on a data set of over 7000 examples were reported. The         Brown heuristic was not applicable since it acted only on the
experiments showed Brown selecting the best ordering (as             input polynomials). In general they were useful in identify-
measured by lowest cell count) more often than the others.           ing the optimal designation, although both could be misled.
However a key finding was that there were substantial subsets        As described above these heuristics essentially complete the
of examples for which each heuristic did best. Further, when         projection stage of the algorithm for each ordering, which
calculating the saving made by the heuristics (compared to the       although minimal in comparison to the lifting stage, is likely
average cell count of the different orderings) the authors of [39]   far more computation than would normally be undertaken by a
found that sotd actually made a greater saving for quantified        heuristic. This becomes an issue when the number of choices
problems on average (i.e. while Brown was superior on                grows. Further, for these experiments a fixed variable ordering
more examples, sotd was superior on examples with greater            was used, and the question of addressing the two choices
savings on offer). Together, this meant that recommending one        together (when the number of possibilities multiplies) has not
heuristic at the expense of all others was not possible.             been addressed.
     If the minimal cell count is a priority then one further            3) Designation in TTICAD: In [7], [8] a truth-table invari-
approach, suggested in [64] is to compute the full dimensional       ant CAD (TTICAD) is defined as a CAD on whose cells
cells for each possible ordering and pick the ordering with the      the truth-table for a set of formulae is invariant. A new
minimum to derive a full CAD. Computing full dimensional             operator was presented which takes advantage of ECs present
cells avoids any work with algebraic numbers and so is not           in the separate formulae (with [7] developing the theory in the
as costly as may be thought, although it does require more           case where all had an EC and [8] extending to the general
computation than ndrr. It was noted in [64] that the full-           case). The operator essentially recognises when to consider
dimensional cell calculations could be done in parallel with the     the interaction of polynomials from different formulae. If an
first to finish extended to a full CAD and the rest discarded.       individual formula has multiple ECs then, as above, we must
                                                                     choose just one to designate for each projection.
B. Choices with equational constraints
                                                                     C. Choices for CAD by Regular Chains
    1) Equational constraints: There are several ways in which
we can modify CAD constriction to achieve truth-invariance               Recently an alternative CAD computational scheme has
(rather than sign-invariance) including refining sign-invariant      been proposed where, instead of projection and lifting, we: first
CAD and truncating lifting once the truth-value is determined.       cylindrically decompose complex space according to whether
A particularly fruitful approach is to take advantage of the         polynomials are zero or not using the theory of triangular
                                                                     decomposition by regular chains; and then refine to a CAD of
                                                                     real space. This was first proposed in [21] with an incremental
                                                                     version described in [20] and an extension to TTICAD in [6].
                                                                     All versions are implemented within the RegularChains
                                                                     Library2 with a summary in [19].
                                                                         Most of the heuristics outlined earlier in this section are not
                                                                     directly applicable to the CAD by Regular Chains computation
Fig. 2.   CADs under different variable orderings                      2 www.regularchains.org
scheme (as there is no “cheap” projection phase to derive
information from). We outline some of the new heuristics
developed for the choices this scheme involves.
    1) Variable order in TTICAD by Regular Chains: This
problem was considered in [30]. Two existing heuristics were
compared: that of Brown introduced in Section III-A and
another, denoted Triangular, already in use for other algorithms
in the RegularChains Library. Triangular chooses first the
variable with lowest degree occurring in the input; then breaks
ties by choosing variables for which leading coefficients have
lowest total degree; and finally sum of degrees in input. In
                                                                    Fig. 3. Visualisations of the four TTICADs which can be built using the
addition the heuristics sotd and ndrr discussed above were          Regular Chains Library for the example in this section. The figures on the top
used (even though the sets of projection polynomials built were     have φ1 → φ2 and those on the bottom φ2 → φ1 . The figures on the left
not explicitly used later). The experiments found sotd to           have f1 → f2 and those on the right f2 → f1 .
make the best choices, but due to its higher costs the Triangular
heuristic was the most efficient choice overall. However, as
with the experiments discussed in Section III-A, the example        degrees of the polynomials in the complex cylindrical decom-
set could be subdivided into groups where different heuris-         position created. As with the ndrr and full dimensional cells
tics were dominant. Further experimentation and illustrative        heuristics above; this requires more computation than is ideal
examples in [30] led to the development of a new heuristic          (although it is the real root refinement that makes up the bulk
(composed from parts of the others) tailored to the variable        of the CAD by Regular Chains computation time).
ordering choice for TTICAD by Regular Chains [6].
                                                                    D. Gröbner Basis preconditioning
    2) Constraint order in TTICAD by Regular Chains: The
latest CAD algorithm within the RegularChains Library                   A Gröbner Basis G is a particular generating set of an
[20] processes constraints incrementally when building the          ideal I defined with respect to a monomial ordering [17]. One
complex cylindrical decomposition and thus are sensitive to         definition is that the ideal generated by the leading terms of I
the order in which constraints are considered. Further, in the      is generated by the leading terms of G. Gröbner Bases (GB)
case of TTICAD we have the extra question of what order to          are used extensively to study ideals and the polynomials that
consider the formulae in. These issues were studied in [28]         define them as they allow properties such as dimension and
which considered the following example.                             number of zeros to be easily deduced. Although like CAD
                                                                    the calculation of GB is doubly exponential in the worst case
   Assume the ordering x ≺ y and consider                           [48], GB computation is now mostly trivial for any problem
               f1 := x2 + y 2 − 1,                                  on which CAD construction is tractable.
               f2 := 2y 2 − x,                                          It was first observed in [18] that replacing a conjunction of
                                                                    polynomial equalities in a CAD problem by their GB (logically
               f3 := (x − 5)2 + (y − 1)2 − 1,                       equivalent) could be useful for the CAD computation. Of
               φ1 := f1 = 0 ∧ f2 = 0,                               the ten test problems studied: 6 were improved by the GB
               φ2 := f3 = 0.                                        preconditioning (speed-up varying from 2- to 1700-fold); 1
                                                                    problem resulted in a 10-fold slow-down; 1 timed out when
The polynomials are graphed within the plots of Figure 3. If        GB preconditioning was applied, but would complete without;
we want to study the truth of φ1 and φ2 (or say a parent            and 2 were intractable both for CAD construction alone and the
formula φ1 ∨ φ2 ) we need a TTICAD to take advantage of the         GB preconditioning step. The problem was revisited in [66].
ECs. There are two possible orders for the formulae and two         As expected, there had been a big decrease in the computation
possible to consider the constraints within φ1 . Hence 4 possible   timings, especially for the GB. However, it was still the case
ways we could calculate a TTICAD by Regular Chains. Below           that 2 of the problems were hindered by GB preconditioning.
we show how many cells are produced by proceeding in the
orders indicated, with the two dimensional cells shown in               The key conclusion is that GB preconditioning will on
Figure 3.                                                           average benefit CAD (sometimes very significantly) but could
                                                                    on occasion hinder it (to the point of making a tractable CAD
   •    φ1 → φ2 and f1 → f2 : 37 cells.                             problem intractable). We are yet to understand why this occurs,
   •    φ1 → φ2 and f2 → f1 : 81 cells.                             but the authors of [66] did develop a metric to predict when it
                                                                    will. They defined the Total Number of Indeterminates (TNoI)
   •    φ2 → φ1 and f1 → f2 : 25 cells.                             of a set of polynomials A as
   •    φ2 → φ1 and f2 → f1 : 43 cells.
                                                                                                    X
                                                                                       TNoI(A) =         NoI(a)
                                                                                                           a∈A
    No previously discussed heuristic was applicable to this
problem. For choosing which EC to process first in a given          where NoI(a) is the number of indeterminates in a polynomial
formula an argument could be made for measuring a set               a. The heuristic is to build a CAD for the preconditioned
of polynomials shown to be rendered sign-invariant by the           polynomials only if the TNoI decreased. For most of their
algorithm (leading to Heuristic 1 in [28]). The only heuristic      test problems the heuristic made the correct choice, but there
derived for the other choices was to measure the sum of             were examples to the contrary.
E. Use of machine learning                                        format (although currently not with any suitable for CAD).
                                                                  The software described in [36] was built to translate problems
    Finally, we note recent experiments using machine learn-
                                                                  in that database into executable code for various computer
ing, specifically support vector machines (see for example
                                                                  algebra systems. The authors of [36] discuss the peculiarities of
[56]), to make choices for CAD construction:
                                                                  computer algebra that make benchmarking particularly difficult
   •    In [40] the authors used an SVM to choose be-             including the fact that results of computations need not be
        tween the three heuristics for CAD variable ordering      unique and that the evaluation of the correctness of an output
        outlined in Section III-A. Simple problem features        may not be trivial (or may be the subject of research itself).
        were selected (e.g. degrees, proportion of monomials          A final point to note is that while SAT / SMT-solvers have
        containing each variable) and parameter optimisation      only a few clear possible answers (e.g. sat, unsat, unknown)
        was applied to maximise Matthews’ Correlation Co-         in computer algebra there is also the quality of the result to
        efficient [47]. Over 7000 examples were studied, and      consider (e.g., size of quantifier-free formula produced). With
        over the 1721 reserved for the test set the machine       CAD the output size is usually correlated to computation time,
        learned choice was found to outperform each heuristic     but this is not always the case with other algorithms.
        individually on average.
   •    In [38] the authors used an SVM to predict when           B. The present authors’ recent experience with CAD
        it will be useful to precondition a CAD problem
                                                                    In our work we have taken various approaches to experi-
        with GB (see Section III-D). The features used were
                                                                  menting with CAD:
        from both the original input and the GB: so the
        study was answering the question should we use this       1 (a) Test new results on examples previously used to evaluate
        GB rather than should we compute it (relevant since         CAD algorithms.
        the GB computation was trivial for the problem set
        involved). The machine learned choice outperformed        For example, the experiments in [66] started with the 10
        both using GB universally, and the human defined          examples in [18] while [24] and [63] focussed on classic
        TNoI heuristic.                                           examples from [44] and [23]. The latter were derived from
                                                                  applications of CAD while the former seem to be a collection
We also note that a recent paper [45] applied a support vector    of geometric problems invented by the authors. Other papers
machine (seeded with the problem features from [40]) to           that have contributed such test problems include [5], [49]
suggest the order in which QE should be performed on sub-         [11], [27]. We wonder whether historic repetition within the
formulae of a non-prenex formula. Experimental results on         literature is alone a strong enough reason to be benchmark?
more than 2,000 non-trivial examples showed that machine
learning was doing better than the human derived heuristics,          In [65], [61] an attempt was made to gather together all
following appropriate parameter optimisation.                     those test examples in the literature for CAD, along with ref-
                                                                  erences of their first appearance in the literature and encodings
            IV.    S TANDARDS AND B ENCHMARKS                     for some computer algebra systems.
A. History of benchmarking in computer algebra                    1 (b) Supplement existing examples with modified versions
                                                                    suitable for demonstrating the feature in question.
    The Computer Algebra community has occasionally recog-
nised the importance of benchmarks. The PoSSo and FRISCO          In [7], [8] the new TTICAD algorithm that was the subject of
projects aimed to do this for polynomials systems and             the paper offered an improvement on the state of the art for
symbolic-numeric problems respectively in the 1990s. PoSSO,       examples consisting of multiple formulae; or a single formulae
with which the second author was involved, collected a series     in disjunctive normal form. Such examples had not been the
of benchmark examples for GB, and a descendant of these           topic of any CAD papers before and no existing examples were
can still be found online3 . However, this does not appear        capable of demonstrating the savings on offer. The experiments
to be maintained; and the polynomials are not stored in a         produced in these papers were made of up two sets:
machine-readable form. Polynomials from this list still crop
up in various papers, but there is no systematic reference,          •    Formulae produced to describe the branch cuts of
and it is not clear whether people are really referring to the            multivalued functions in a proposed simplification
same example. Several of the examples are families, which                 formula [30], with CAD to be applied so that the
is good but means that a benchmark has to contain specific                complex domain could be decomposed into regions
instances. The PoSSo project did its best to do “level playing            where the functions were univariate, and thus the
field” comparisons, but at the time different implementations             formula applicable or not.
ran on different hardware / operating systems meaning this
                                                                     •    Formulae produced by adapting the logical connectors
was not really achievable. The environment is much simpler
                                                                          in previous examples from the literature in [65] so that
these days, and it would be feasible to organise true contests.
                                                                          conjunctions became disjunctions.
    The topic of benchmarking in computer algebra has most
recently been taken up by the SymbolicData Project4 [35]          Clearly the former set is of great interest as they represent
which is beginning to build a database of examples in XML         a real example for the algorithms; but they all conform to a
                                                                  single structure and so are arguably too uniform to alone draw
 3 http://www-sop.inria.fr/saga/POL/                              broad conclusions from. The second set were produced to be
 4 www.symbolicdata.org                                           somehow close to the accepted test examples of the literature,
but whether this is any better than inventing a new examples        in [38]. Thus while the nlsat dataset is an excellent starting
from scratch is debatable.                                          point it needs to be expanded to be less uniform.
2 Derive new sets of random examples                                   We finish this section by noting one possible source of
                                                                    examples for the future.
    A recent experiment using machine learning [40], [38] (see
Section III-E) exposed a shortcoming in the above techniques.          •     The Todai Robot Project8 [46] is a Japanese AI project
To train the SVMs hundreds of examples are required (with                    that aims to have an artificial intelligence pass the
hundreds more then needed for validation and testing). The                   entrance examination for the University of Tokyo by
dataset from the literature in [65] contained not nearly enough              2021. A majority of questions on the Mathematics
examples and while the datasets discussed in the next section                exam can be resolved by real quantifier elimination
were sufficient for the first experiment in [40] they proved                 with a variety of techniques employed [41]. A key
too uniform for [38]. We were left with no choice but to                     difficulty is that the natural language processing of
generate large quantities of new examples, which we did using                the question derives a formula of far greater complex-
the random polynomial generator in M APLE. We had applied                    ity than the human derived equivalent. This process
this technique also in [28], [30] receiving positive feedback                derives a large bank of examples of CAD problems,
from reviewers for the technique; but the initial reviews of                 as discussed in [45] for example. The authors of [45]
[38] were all negative on the use of random data. It seems the               told us there are plans to make this data set public.
appropriateness of this technique varies with the community
(conference) in question. We opine that had we used data from                     V.        C ONCLUSIONS AND QUESTIONS
the example bank of MetiTarski examples discussed in the next           After surveying the work in Section III we see that several
section then reviewers may have praised the focus on examples       approaches to the creation of heuristics have been taken:
from a real application; even though MetiTarski themselves          ranging from human identified algebraic features, justified by
derive examples for benchmarks using random polynomials.            mathematical arguments and observations to different extents;
                                                                    to machine learned choices using a support vector machine. We
C. Sources of large benchmarks sets                                 are interested to hear how these compare with the heuristics
                                                                    used in SAT-solvers and what lessons can be learned.
   We note some other sources of large sets of benchmark
problems that represent real applications of CAD:                       We can identify at least two areas where CAD is in need
                                                                    of further heuristic development.
   •     MetiTarski5 [3], [54] is an automatic theorem prover
         designed to prove theorems involving real-valued spe-         •     How best to take decisions in tandem: The work
         cial functions (such as log, exp, sin, cos and sqrt). In            surveyed all considered choices to be made for CAD
         general this theory is undeciadable but MetiTarski is               in isolation (assuming other choices had already been
         able to solve many problems by applying real polyno-                fixed). Of course, in reality this may not be the case.
         mial bounds and then using real quantifier elimination              We must decide which decisions to prioritise; how
         tools like CAD. Applications of MetiTarski in turn                  heuristics can be combined; and how the combinatorial
         derive examples for CAD.                                            blow-up of decisions can be contained. Does the SAT-
                                                                             solving community have experience in similar issues?
   •     The NRA (non-linear real arithmetic) category of the
         SMT-LIB library6 which according to [43] consists          There are many implementations of CAD including: the dedi-
         mostly of problems originating from attempts to prove      cated command line program Qepcad [12]; Mathematica [58],
         termination of term-rewrite systems.                       [59], where CAD is not available directly but is used as
                                                                    a subroutine for quantifier elimination; the Redlog pack-
    These two data sets where included in the nlsat Bench-          age for R EDUCE [57]; and 3 different M APLE libraries -
mark Set7 produced to evaluate the work in [43]. This also          the RegularChains Library (see Section III-C; SyNRAC
included verification conditions from the Keymaera [55] and         [67] (now part of the Todai Robot project) and our own
parametrized generalizations of the problem from [37]. To-          ProjectionCAD module [32].
gether this dataset had many thousands of problems. However,
we note that the problems come from a small number of classes          •     How to choose between different implementations?
and may have some hidden uniformity.                                         Each implementation includes unique pieces of theory
                                                                             and features and excels on different examples. Ide-
   As mentioned above, the nlsat dataset was unsuitable to                   ally, we would have a single implementation which
use for our machine learning experiment in [38]. Every single                encompasses all recent advances. A more manageable
problem within that had more than one equality was aided                     step may be an overarching M APLE command to
by GB preconditioning, in fact a great many simply had a                     choose between the 3 packages there. SMT-solvers
GB containing only 1 indicating the problem had no solution.                 are designed to use a variety of different theory solvers
Previous experiments on small example sets suggested GB                      and how they choose between these may offer valuable
preconditioning sometimes harms CAD computation and this                     lessons here.
was verified by analysis of a large randomly generated dataset
                                                                       Surveying Section IV raises a number of questions about
 5 https://www.cl.cam.ac.uk/∼lp15/papers/Arith
                                                                    how benchmark sets should be produced:
 6 http://smtlib.cs.uiowa.edu/
 7 http://cs.nyu.edu/∼dejan/nonlinear/                               8 http://21robot.org
      •      How best to generate large numbers of examples                           [10]   C.W. Brown. Improved projection for cylindrical algebraic decomposi-
             which are not internally uniform?                                               tion. Journal of Symbolic Computation, 32(5):447–465, 2001.
                                                                                      [11]   C.W. Brown. Simple CAD construction and its applications. Journal
      •      How important is it that the benchmarks come from                               of Symbolic Computation, 31(5):521–547, 2001.
             current applications?                                                    [12]   C.W. Brown. An overview of QEPCAD B: a tool for real quantifier
      •      How important is it that the benchmarks have histor-                            elimination and formula simplification. Journal of Japan Society for
                                                                                             Symbolic and Algebraic Computation, 10(1):13–22, 2003.
             ically been used in the literature?
                                                                                      [13]   C.W. Brown. Companion to the tutorial: Cylindrical algebraic decompo-
      •      Are randomly generated examples a fairer way to                                 sition, presented at ISSAC ’04. http://www.usna.edu/Users/cs/wcbrown/
             evaluate the software, or irrelevant as too far removed                         research/ISSAC04/handout.pdf, 2004.
             from applications?                                                       [14]   C.W. Brown. Constructing a single open cell in a cylindrical algebraic
                                                                                             decomposition. In Proceedings of the 38th International Symposium
The SAT / SMT community posses a unified, large and                                          on Symbolic and Algebraic Computation, ISSAC ’13, pages 133–140.
                                                                                             ACM, 2013.
growing set of benchmarks in the SMT-LIB library and so we
may be able to extrapolate lessons from this. However, as noted                       [15]   C.W. Brown and J.H. Davenport. The complexity of quantifier elimina-
                                                                                             tion and cylindrical algebraic decomposition. In Proceedings of the 2007
above, this library may be too uniform [38], and comments                                    International Symposium on Symbolic and Algebraic Computation,
from the anonymous referees suggest that this and other critics                              ISSAC ’07, pages 54–60. ACM, 2007.
are already a topic of discussion in the SMT community.                               [16]   C.W. Brown, M. El Kahoui, D. Novotni, and A. Weber. Algorithmic
                                                                                             methods for investigating equilibria in epidemic modelling. Journal of
Acknowledgements                                                                             Symbolic Computation, 41:1157–1173, 2006.
                                                                                      [17]   B. Buchberger. Bruno Buchberger’s PhD thesis (1965): An algorithm for
    Thanks to our collaborators on the work surveyed here:                                   finding the basis elements of the residue class ring of a zero dimensional
Russell Bradford, James Bridge, Changbo Chen, Zongyan                                        polynomial ideal. Journal of Symbolic Computation, 41(3-4):475–511,
Huang, Scott McCallum, Marc Moreno Maza, Lawrence Paul-                                      2006.
son, and David Wilson. Thanks also to the anonymous referees                          [18]   B. Buchberger and H. Hong. Speeding up quantifier elimination
for their comments which improved the paper.                                                 by Gröbner bases. Technical report, 91-06. RISC, Johannes Kepler
                                                                                             University, 1991.
   Most of the work surveyed here was supported by EPSRC                              [19]   C. Chen and M. Moreno Maza. Cylindrical algebraic decomposition
grant EP/J003247/1. The authors are now supported by EU                                      in the RegularChains library. In H. Hong and C. Yap, editors,
H2020-FETOPEN-2016-2017-CSA project SC 2 (712689).                                           Mathematical Software – ICMS 2014, LNCS 8592, pages 425–433.
                                                                                             Springer Heidelberg, 2014.
                                  R EFERENCES                                         [20]   C. Chen and M. Moreno Maza. An incremental algorithm for computing
                                                                                             cylindrical algebraic decompositions. In R. Feng, W. Lee, and Y. Sato,
[1]       E. Ábráham. Building bridges between symbolic computation and                    editors, Computer Mathematics, pages 199—221. Springer Berlin Hei-
          satisfiability checking. In Proceedings of the 2015 International                  delberg, 2014.
          Symposium on Symbolic and Algebraic Computation, ISSAC ’15, pages
                                                                                      [21]   C. Chen, M. Moreno Maza, B. Xia, and L. Yang. Computing cylindrical
          1–6. ACM, 2015.
                                                                                             algebraic decomposition via triangular decomposition. In Proceedings
[2]       E. Ábrahám, J. Abbott, B. Becker, A.M. Bigatti, M. Brain, B. Buch-               of the 2009 International Symposium on Symbolic and Algebraic
          berger, A. Cimatti, J.H. Davenport, M. England, P. Fontaine, S. Forrest,           Computation, ISSAC ’09, pages 95–102. ACM, 2009.
          A. Griggio, D. Kroening, W.M. Seiler, and T. Sturm. SC2 : Satisfiability
                                                                                      [22]   G.E. Collins and H. Hong. Partial cylindrical algebraic decomposition
          checking meets symbolic computation. In M. Kohlhase, M. Johansson,
                                                                                             for quantifier elimination. Journal of Symbolic Computation, 12:299–
          B. Miller, L. de Moura, and F. Tompa, editors, Intelligent Computer
                                                                                             328, 1991.
          Mathematics: Proceedings CICM 2016, LNCS 9791, pages 28–43.
          Springer International Publishing, 2016.                                    [23]   J.H. Davenport. A “Piano-Movers” Problem. SIGSAM Bull., 20(1-
[3]       B. Akbarpour and L.C. Paulson. MetiTarski: An automatic theorem                    2):15–17, 1986.
          prover for real-valued special functions. Journal of Automated Reason-      [24]   J.H. Davenport, R. Bradford, M. England, and D. Wilson. Program
          ing, 44(3):175–205, 2010.                                                          verification in the presence of complex numbers, functions with branch
[4]       D. Arnon, G.E. Collins, and S. McCallum. Cylindrical algebraic                     cuts etc. In 14th International Symposium on Symbolic and Numeric
          decomposition I: The basic algorithm. SIAM Journal of Computing,                   Algorithms for Scientific Computing, SYNASC ’12, pages 83–88. IEEE,
          13:865–877, 1984.                                                                  2012.
[5]       D.S. Arnon. A cluster-based cylindrical algebraic decomposition             [25]   J.H. Davenport and M. England. Need polynomial systems be doubly
          algorithm. Journal of Symbolic Computation, 5(1-2):189–212, 1988.                  exponential? In G.-M. Greuel, T. Koch, P. Paule, and A. Sommese,
                                                                                             editors, Mathematical Software – Proceedings of ICMS 2016, LNCS
[6]       R. Bradford, C. Chen, J.H. Davenport, M. England, M. Moreno Maza,
                                                                                             9725, pages 157–164. Springer International Publishing, 2016.
          and D. Wilson. Truth table invariant cylindrical algebraic decomposition
          by regular chains. In V.P. Gerdt, W. Koepf, W.M. Seiler, and E.V.           [26]   J.H. Davenport and J. Heintz. Real quantifier elimination is doubly
          Vorozhtsov, editors, Computer Algebra in Scientific Computing, LNCS                exponential. Journal of Symbolic Computation, 5(1-2):29–35, 1988.
          8660, pages 44–58. Springer International Publishing, 2014.                 [27]   A. Dolzmann, A. Seidl, and T. Sturm. Efficient projection orders for
[7]       R. Bradford, J.H. Davenport, M. England, S. McCallum, and D. Wilson.               CAD. In Proceedings of the 2004 International Symposium on Symbolic
          Cylindrical algebraic decompositions for boolean combinations. In                  and Algebraic Computation, ISSAC ’04, pages 111–118. ACM, 2004.
          Proceedings of the 38th International Symposium on Symbolic and             [28]   M. England, R. Bradford, C. Chen, J.H. Davenport, M. Moreno Maza,
          Algebraic Computation, ISSAC ’13, pages 125–132. ACM, 2013.                        and D. Wilson. Problem formulation for truth-table invariant cylindrical
[8]       R. Bradford, J.H. Davenport, M. England, S. McCallum, and D. Wilson.               algebraic decomposition by incremental triangular decomposition. In
          Truth table invariant cylindrical algebraic decomposition. Journal of              S.M. Watt, J.H. Davenport, A.P. Sexton, P. Sojka, and J. Urban, editors,
          Symbolic Computation, 76:1–35, 2015.                                               Intelligent Computer Mathematics, LNCS 8543, pages 45–60. Springer
[9]       R. Bradford, J.H. Davenport, M. England, and D. Wilson. Optimising                 International, 2014.
          problem formulations for cylindrical algebraic decomposition. In            [29]   M. England, R. Bradford, and J.H. Davenport. Improving the use
          J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger, editors,          of equational constraints in cylindrical algebraic decomposition. In
          Intelligent Computer Mathematics, LNCS 7961, pages 19–34. Springer                 Proceedings of the 2015 International Symposium on Symbolic and
          Berlin Heidelberg, 2013.                                                           Algebraic Computation, ISSAC ’15, pages 165–172. ACM, 2015.
[30]   M. England, R. Bradford, J.H. Davenport, and D. Wilson. Choosing           [47]   B.W. Matthews. Comparison of the predicted and observed secondary
       a variable ordering for truth-table invariant cylindrical algebraic de-           structure of T4 phage lysozyme. Biochimica et Biophysica Acta (BBA)-
       composition by incremental triangular decomposition. In H. Hong and               Protein Structure, 405(2):442–451, 1975.
       C. Yap, editors, Mathematical Software – ICMS 2014, LNCS 8592,             [48]   E.W. Mayr and A.R. Meyer. The complexity of the word problems
       pages 450–457. Springer Heidelberg, 2014.                                         for commutative semigroups and polynomial ideals. Advances in
[31]   M. England and J.H. Davenport. The complexity of cylindrical algebraic            Mathematics, 46(3):305–329, 1982.
       decomposition with respect to polynomial degree. To appear In:             [49]   S. McCallum. An improved projection operation for cylindrical alge-
       Proceedings CASC 2016 (Springer LNCS), 2016.                                      braic decomposition of three-dimensional space. Journal of Symbolic
[32]   M. England, D. Wilson, R. Bradford, and J.H. Davenport. Using the                 Computation, 5(1-2):141–161, 1988.
       Regular Chains Library to build cylindrical algebraic decompositions       [50]   S. McCallum. An improved projection operation for cylindrical
       by projecting and lifting. In H. Hong and C. Yap, editors, Mathe-                 algebraic decomposition. In B. Caviness and J. Johnson, editors,
       matical Software – ICMS 2014, LNCS 8592, pages 458–465. Springer                  Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts
       Heidelberg, 2014.                                                                 & Monographs in Symbolic Computation, pages 242–268. Springer-
[33]   M. Erascu and H. Hong. Synthesis of optimal numerical algorithms                  Verlag, 1998.
       using real quantifier elimination (Case Study: Square root computation).   [51]   S. McCallum. On projection in CAD-based quantifier elimination
       In Proceedings of the 39th International Symposium on Symbolic and                with equational constraint. In Proceedings of the 1999 International
       Algebraic Computation, ISSAC ’14, pages 162–169. ACM, 2014.                       Symposium on Symbolic and Algebraic Computation, ISSAC ’99, pages
[34]   I.A. Fotiou, P.A. Parrilo, and M. Morari. Nonlinear parametric opti-              145–149. ACM, 1999.
       mization using cylindrical algebraic decomposition. In Decision and        [52]   S. McCallum. On propagation of equational constraints in CAD-
       Control, 2005 European Control Conference. CDC-ECC ’05., pages                    based quantifier elimination. In Proceedings of the 2001 International
       3735–3740, 2005.                                                                  Symposium on Symbolic and Algebraic Computation, ISSAC ’01, pages
[35]   H.G. Graebe, A. Nareike, and S. Johanning. The SymbolicData                       223–231. ACM, 2001.
       project: Towards a computer algebra social network. In M. England,         [53]   S. McCallum, A. Parusińiski, and L. Paunescu. Validity proof of
       J.H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper,                Lazard’s method for CAD construction. Preprint: Arxiv 1607:00264,
       P. Quaresma, A.P. Sexton, P. Sojka, J. Urban, and S.M. Watt, editors,             2016.
       Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and
                                                                                  [54]   L.C. Paulson. Metitarski: Past and future. In L. Beringer and
       Work in Progress track at CICM, number 1186 in CEUR Workshop
                                                                                         A. Felty, editors, Interactive Theorem Proving, LNCS 7406, pages 1–10.
       Proceedings, 2014.
                                                                                         Springer, 2012.
[36]   A. Heinle and V. Levandovskyy. The SDEval benchmarking toolkit.
                                                                                  [55]   A. Platzer, J.D. Quesel, and P. Rümmer. Real world verification. In
       ACM Communications in Computer Algebra, 49(1):1–9, 2015.
                                                                                         R.A. Schmidt, editor, Automated Deduction (CADE-22), LNCS 5663,
[37]   H. Hong. Comparison of several decision algorithms for the existential            pages 485–501. Springer Berlin Heidelberg, 2009.
       theory of the reals. Technical report, RISC, Linz, 1991.
                                                                                  [56]   B. Schölkopf, K. Tsuda, and J.-P. Vert. Kernel methods in computational
[38]   Z. Huang, M. England, J.H. Davenport, and L. Paulson. Using machine               biology. MIT Press, 2004.
       learning to decide when to precondition cylindrical algebraic decom-
                                                                                  [57]   A. Seidl and T. Sturm. A generic projection operator for partial cylindri-
       position with Groebner bases. In 18th International Symposium on
                                                                                         cal algebraic decomposition. In Proceedings of the 2003 International
       Symbolic and Numeric Algorithms for Scientific Computing, SYNASC
                                                                                         Symposium on Symbolic and Algebraic Computation, ISSAC ’03, pages
       ’16. Preprint: Arxiv 1608.04219. IEEE, 2016.
                                                                                         240–247. ACM, 2003.
[39]   Z. Huang, M. England, D. Wilson, J.H. Davenport, and L. Paulson. A
                                                                                  [58]   A. Strzeboński. Cylindrical algebraic decomposition using validated
       comparison of three heuristics to choose the variable ordering for cad.
                                                                                         numerics. Journal of Symbolic Computation, 41(9):1021–1038, 2006.
       ACM Communications in Computer Algebra, 48(3):121–123, 2014.
                                                                                  [59]   A. Strzeboński. Computation with semialgebraic sets represented by
[40]   Z. Huang, M. England, D. Wilson, J.H. Davenport, L. Paulson, and
                                                                                         cylindrical algebraic formulas. In Proceedings of the 2010 International
       J. Bridge. Applying machine learning to the problem of choosing
                                                                                         Symposium on Symbolic and Algebraic Computation, ISSAC ’10, pages
       a heuristic to select the variable ordering for cylindrical algebraic
                                                                                         61–68. ACM, 2010.
       decomposition. In S.M. Watt, J.H. Davenport, A.P. Sexton, P. Sojka,
       and J. Urban, editors, Intelligent Computer Mathematics, LNAI 8543,        [60]   A. Strzeboński. Cylindrical algebraic decomposition using local projec-
       pages 92–107. Springer International, 2014.                                       tions. In Proceedings of the 39th International Symposium on Symbolic
                                                                                         and Algebraic Computation, ISSAC ’14, pages 389–396. ACM, 2014.
[41]   H. Iwane, T. Matsuzaki, N.H. Arai, and H. Anai. Automated natural
       language geometry math problem solving by real quantifier elimination.     [61]   D. Wilson. Real geometry and connectedness via triangular description:
       In Proceedings of the 10th International Workshop on Automated                    Cad example bank, 2013.
       Deduction in Geometry, ADG ’14, pages 75–84, 2014.                         [62]   D. Wilson, R. Bradford, J.H. Davenport, and M. England. Cylindrical
[42]   H. Iwane, H. Yanami, H. Anai, and K. Yokoyama. An effective imple-                algebraic sub-decompositions. Mathematics in Computer Science,
       mentation of a symbolic-numeric cylindrical algebraic decomposition               8:263–288, 2014.
       for quantifier elimination. In Proceedings of the 2009 conference on       [63]   D. Wilson, J.H. Davenport, M. England, and R. Bradford. A “piano
       Symbolic Numeric Computation, SNC ’09, pages 55–64, 2009.                         movers” problem reformulated. In 15th International Symposium on
[43]   D. Jovanovic and L. de Moura. Solving non-linear arithmetic. In                   Symbolic and Numeric Algorithms for Scientific Computing, SYNASC
       B. Gramlich, D. Miller, and U. Sattler, editors, Automated Reasoning:             ’13, pages 53–60. IEEE, 2013.
       6th International Joint Conference (IJCAR), LNCS 7364, pages 339–          [64]   D. Wilson, M. England, J.H. Davenport, and R. Bradford. Using the dis-
       354. Springer, 2012.                                                              tribution of cells by dimension in a cylindrical algebraic decomposition.
[44]   W. Kahan. Branch cuts for complex elementary functions. In A. Iserles             In 16th International Symposium on Symbolic and Numeric Algorithms
       and M.J.D. Powell, editors, Proceedings The State of Art in Numerical             for Scientific Computing, SYNASC ’14, pages 53–60. IEEE, 2014.
       Analysis, pages 165–211. Clarendon Press, 1987.                            [65]   D.J. Wilson, R.J. Bradford, and J.H. Davenport. A repository for CAD
[45]   M. Kobayashi, H. Iwane, T. Matsuzaki, and H. Anai. Efficient subfor-              examples. ACM Communications in Computer Algebra, 46(3):67–69,
       mula orders for real quantifier elimination of non-prenex formulas. In            2012.
       S.I. Kotsireas, M.S. Rump, and K.C. Yap, editors, Mathematical Aspects     [66]   D.J. Wilson, R.J. Bradford, and J.H. Davenport. Speeding up cylindrical
       of Computer and Information Sciences (MACIS ’15), LNCS 9582, pages                algebraic decomposition by Gröbner bases. In J. Jeuring, J.A. Campbell,
       236–251. Springer International Publishing, 2016.                                 J. Carette, G. Reis, P. Sojka, M. Wenzel, and V. Sorge, editors, Intel-
[46]   T. Matsuzaki, H. Iwane, H. Anai, and N. Arai. The most uncreative                 ligent Computer Mathematics, LNCS 7362, pages 280–294. Springer,
       examinee: A first step toward wide coverage natural language math                 2012.
       problem solving. In C.E. Brodley and P. Stone, editors, Proceedings of     [67]   H. Yanami and H. Anai. Development of SyNRAC. In Proceedings
       28th Conference on Artificial Intelligence, AAAI ’14, pages 1098–1104.            of the 6th international conference on Computational Science: Part II.
       AAAI Press, 2014.                                                                 (LNCS vol 3992), ICCS ’06, pages 462–469, 2006.