-In the paper which inspired the SC2 project, [E. A´ bra´ham, Building Bridges between Symbolic Computation and Satisfiability Checking, Proc. ISSAC '15, pp. 1-6, ACM, 2015] the author identified the use of sophisticated heuristics as a technique that the Satisfiability Checking community excels in and from which it is likely the Symbolic Computation community could learn and prosper. To start this learning process we summarise our experience with heuristic development for the computer algebra algorithm Cylindrical Algebraic Decomposition. We also propose and discuss standards and benchmarks as another area where Symbolic Computation could prosper from Satisfiability Checking expertise, noting that these have been identified as initial actions for the new SC2 community in the CSA project, as described in [E. A´ bra´ham et al., SC2: Satisfiability Checking meets Symbolic Computation (Project Paper), Intelligent Computer Mathematics (LNCS 9761), pp. 28-43, Springer, 2015].
This article is inspired by the SC2 project1, a new initiative
to forge a joint community from the existing fields of Symbolic
Computation and Satisfiability Checking. For further details
on the project we refer the reader to:
[
Within [
Another topic where Symbolic Computation might benefit
from experience in Satisfiability Checking is standards and
benchmarks. Competitions based on these form an integral
part of the Satisfiability Checking community, and may have
contributed to the remarkable progress made in practical
algorithms. The lack of a comparable focus for the Symbolic
Computation community was acknowledged in [
In the present paper we outline our experience of these issues for a single Symbolic Computation algorithm, Cylindrical Algebraic Decomposition (CAD). The aim of the paper is to instigate the learning process from the Satisfiability Checking community by illustrating the current use of heuristics, benchmarks and standards in (at least one area of) Symbolic Computation and posing some questions. We start with a summary of the necessary background on CAD in Section II, then survey work with heuristics in CAD in Section III and our experience with standards and benchmarks in Section IV. We finish with conclusions and questions in Section V.
II.
A Cylindrical Algebraic Decomposition (CAD) is a decomposition of Rn into cells (connected subsets). By algebraic we mean semi-algebraic: i.e. each cell can be described with a finite sequence of polynomial constraints. Finally, the cells are arranged cylindrically, meaning the projections of any pair, with respect to the variable ordering in which the CAD was created, are either equal or disjoint. We assume variables labelled according to their ordering (so the projections considered are (x1; : : : ; x`) ! (x1; : : : ; xk) for k < `) with the highest ordered variable present said to be the main variable.
Hence CADs can be represented in a tree like format branching on the semi-algebraic conditions involving increasing main variable, as in the example below (with the branching from right to left; all p indicating the positive root; and the tuples Copyright c by the paper's authors. Copying permitted for private and academic purposes. on the left sample points of the cells). 8( 2; 0) > > > > > >>>8( 1; 1) >>>< >> ( 1; 0) > >>>:( 1; 1) > > > > > >>>8(0; 2) > >> >> >>><>>><(0; 1)
(0; 0) >>>>(0; 1) >> >> >>>:(0; 2) > > > > > > >>>8(1; 1) >>>< >> (1; 0) > >>>:(1; 1) > > > > > > :>(2; 0) y < 0 y = 0 0 < y p p y < x2 + 1 y = x2 + 1 p x2 + 1 < y < p y = +p x2 + 1 p x2 + 1 < y y < 0 y = 0 0 < y x < x = 1 1 A CAD is produced to be invariant for input; originally signinvariant for a set of input polynomials (so on each cell each polynomial is positive, zero or negative). The example above is a sign invariant CAD for the polynomial x2 +y2 1 defining the unit circle. More recently CADs have been produced truthinvariant for input Boolean-valued polynomial formulae. A sign-invariant CAD for the polynomials in a formula is also truth-invariant for the formula; but we can often achieve truthinvariance with far less cells. For example suppose we need a CAD truth-invariant for the formula x2 + y2 1 = 0 ^ (x 1)2 + y2 1 = 0: A sign-invariant CAD would require 55 cells (with the full dimensional ones shown on the left of Figure 1). However, a truth-invariant CAD would need only 7 cells: 2 of which are full dimension (as on the right of Figure 1) and 5 more to decompose the line x = 21 at the points of intersection.
CAD construction usually involves two phases. The first projection, applies operators recursively on polynomials, starting with the input. Each time the operator produces a set with one less variable which together define the projection polynomials. These are used in the second phase, lifting, to Fig. 1. Example visualising sign and truth-invariant CADs build CADs of increasing dimension. First a CAD of R1 is built by splitting on the real roots of the univariate polynomials (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 the process is repeated until a CAD of Rn is produced. We call the cells where a polynomial vanishes sections and those regions in-between sectors, which together form the stack over the cell. In each lift we extrapolate the conclusions drawn from working at a sample point to the whole cell requiring validity theorems for the projection operator used.
CAD cells are represented by at least a sample point (as in the left of the example above), and an index: a list of positive integers with each integer indicating the section or stack each variable is within (in reference to the ordered roots of the projection polynomials). Some implementations will also encode the full algebraic description within each cell.
CAD was originally introduced by Collins for quantifier
elimination (QE) in real closed fields [
III.
The most well known choice required for CAD is that of the variable ordering, which the cylindricity is defined with respect to. This determines the order in which variables are eliminated during projection and the subspaces through which CADs are built incrementally during lifting. When using CAD for QE we must project variables in the order they are quantified, but we are free to project the other variables in any order (and to change the order within quantifier blocks).
The variable ordering used can have a great effect on the
output produced. For example, let f := (x 1)(y2 + 1) 1
and consider the minimal sign-invariant CAD in each variable
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 [
Several heuristics have been developed to choose the variable ordering, including:
Brown: Use the following criteria, starting with the first and breaking ties with successive ones: (1) Eliminate variable if lowest overall degree. (2) Eliminate variable if lowest (maximum) total degree in terms in which it occurs. (3) Eliminate variable if smallest number of terms contains it.
Suggested by Brown in [13, Section 5.2].
sotd: For all admissible orderings, calculate the
projection set and choose the one with smallest sum of
total degrees for each of the monomials in each
of the polynomials [
The papers cited each contain experimental results demonstrating their worth. In [39] the results of an experiment comparing the 3 on a data set of over 7000 examples were reported. The experiments showed Brown selecting the best ordering (as measured by lowest cell count) more often than the others. However a key finding was that there were substantial subsets of examples for which each heuristic did best. Further, when calculating the saving made by the heuristics (compared to the average cell count of the different orderings) the authors of [39] found that sotd actually made a greater saving for quantified problems on average (i.e. while Brown was superior on more examples, sotd was superior on examples with greater savings on offer). Together, this meant that recommending one heuristic at the expense of all others was not possible.
If the minimal cell count is a priority then one further approach, suggested in [64] is to compute the full dimensional cells for each possible ordering and pick the ordering with the minimum to derive a full CAD. Computing full dimensional cells avoids any work with algebraic numbers and so is not as costly as may be thought, although it does require more computation than ndrr. It was noted in [64] that the fulldimensional cell calculations could be done in parallel with the first to finish extended to a full CAD and the rest discarded.
1) Equational constraints: There are several ways in which
we can modify CAD constriction to achieve truth-invariance
(rather than sign-invariance) including refining sign-invariant
CAD and truncating lifting once the truth-value is determined.
A particularly fruitful approach is to take advantage of the
Fig. 2. CADs under different variable orderings
Booloean structure of a formula through the identification of
Equational Constraints (ECs): polynomial equations logically
implied by a formula. Reduced projection operators (using a
subset of the usual polynomials) have been proven valid for use
when an EC is present with corresponding main variable [51],
[52]. Results in [
These reduced operators can only use one EC for each
projection, so when there are multiple we must make a
designation. Note that ECs need not appear explicitly as atoms
(formula with no logical connectives) in the input formula, but
could instead be implicit. For example, the resultant of any two
ECs in the same main variable is itself an EC (not containing
that variable) [52]. Propagating ECs in this way allows for the
maximal use of the reduced operators. However, it can require
multiple choices of which EC to designate at each projection.
Section 4 of [
2) Making the designation: In [
3) Designation in TTICAD: In [
Recently an alternative CAD computational scheme has
been proposed where, instead of projection and lifting, we: first
cylindrically decompose complex space according to whether
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 [
Most of the heuristics outlined earlier in this section are not directly applicable to the CAD by Regular Chains computation 2www.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
addition the heuristics sotd and ndrr discussed above were
used (even though the sets of projection polynomials built were
not explicitly used later). The experiments found sotd to
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
set could be subdivided into groups where different
heuristics were dominant. Further experimentation and illustrative
examples in [30] led to the development of a new heuristic
(composed from parts of the others) tailored to the variable
ordering choice for TTICAD by Regular Chains [
2) Constraint order in TTICAD by Regular Chains: The
latest CAD algorithm within the RegularChains Library
[
Assume the ordering x
y and consider f1 := x2 + y2
1; f2 := 2y2 f3 := (x
x; 5)2 + (y 1)2
1; 1 := f1 = 0 ^ f2 = 0; 2 := f3 = 0: The polynomials are graphed within the plots of Figure 3. If we want to study the truth of 1 and 2 (or say a parent formula 1 _ 2) we need a TTICAD to take advantage of the ECs. There are two possible orders for the formulae and two possible to consider the constraints within 1. Hence 4 possible ways we could calculate a TTICAD by Regular Chains. Below we show how many cells are produced by proceeding in the orders indicated, with the two dimensional cells shown in Figure 3.
1 ! 1 ! 2 ! 2 ! 2 and f1 ! f2: 37 cells. 2 and f2 ! f1: 81 cells. 1 and f1 ! f2: 25 cells.
1 and f2 ! f1: 43 cells.
No previously discussed heuristic was applicable to this
problem. For choosing which EC to process first in a given
formula an argument could be made for measuring a set
of polynomials shown to be rendered sign-invariant by the
algorithm (leading to Heuristic 1 in [
A Gro¨bner Basis G is a particular generating set of an
ideal I defined with respect to a monomial ordering [
It was first observed in [
The key conclusion is that GB preconditioning will on average benefit CAD (sometimes very significantly) but could on occasion hinder it (to the point of making a tractable CAD problem intractable). We are yet to understand why this occurs, but the authors of [66] did develop a metric to predict when it will. They defined the Total Number of Indeterminates (TNoI) of a set of polynomials A as
TNoI(A) =
X NoI(a) a2A where NoI(a) is the number of indeterminates in a polynomial a. The heuristic is to build a CAD for the preconditioned polynomials only if the TNoI decreased. For most of their test problems the heuristic made the correct choice, but there were examples to the contrary.
Finally, we note recent experiments using machine learning, specifically support vector machines (see for example [56]), to make choices for CAD construction:
In [40] the authors used an SVM to choose between the three heuristics for CAD variable ordering outlined in Section III-A. Simple problem features were selected (e.g. degrees, proportion of monomials containing each variable) and parameter optimisation was applied to maximise Matthews’ Correlation Coefficient [47]. Over 7000 examples were studied, and over the 1721 reserved for the test set the machine learned choice was found to outperform each heuristic individually on average.
In [38] the authors used an SVM to predict when it will be useful to precondition a CAD problem with GB (see Section III-D). The features used were from both the original input and the GB: so the study was answering the question should we use this GB rather than should we compute it (relevant since the GB computation was trivial for the problem set involved). The machine learned choice outperformed both using GB universally, and the human defined TNoI heuristic.
We also note that a recent paper [45] applied a support vector machine (seeded with the problem features from [40]) to suggest the order in which QE should be performed on subformulae of a non-prenex formula. Experimental results on more than 2,000 non-trivial examples showed that machine learning was doing better than the human derived heuristics, following appropriate parameter optimisation.
The Computer Algebra community has occasionally recognised the importance of benchmarks. The PoSSo and FRISCO projects aimed to do this for polynomials systems and symbolic-numeric problems respectively in the 1990s. PoSSO, with which the second author was involved, collected a series of benchmark examples for GB, and a descendant of these can still be found online3. However, this does not appear to be maintained; and the polynomials are not stored in a machine-readable form. Polynomials from this list still crop up in various papers, but there is no systematic reference, and it is not clear whether people are really referring to the same example. Several of the examples are families, which is good but means that a benchmark has to contain specific instances. The PoSSo project did its best to do “level playing field” comparisons, but at the time different implementations ran on different hardware / operating systems meaning this was not really achievable. The environment is much simpler these days, and it would be feasible to organise true contests.
The topic of benchmarking in computer algebra has most
recently been taken up by the SymbolicData Project4 [
format (although currently not with any suitable for CAD). The software described in [36] was built to translate problems in that database into executable code for various computer algebra systems. The authors of [36] discuss the peculiarities of computer algebra that make benchmarking particularly difficult including the fact that results of computations need not be unique and that the evaluation of the correctness of an output may not be trivial (or may be the subject of research itself).
A final point to note is that while SAT / SMT-solvers have only a few clear possible answers (e.g. sat, unsat, unknown) in computer algebra there is also the quality of the result to consider (e.g., size of quantifier-free formula produced). With CAD the output size is usually correlated to computation time, but this is not always the case with other algorithms.
In our work we have taken various approaches to experimenting with CAD: 1 (a) Test new results on examples previously used to evaluate
CAD algorithms.
For example, the experiments in [66] started with the 10
examples in [
In [65], [61] an attempt was made to gather together all
those test examples in the literature for CAD, along with
references of their first appearance in the literature and encodings
for some computer algebra systems.
1 (b) Supplement existing examples with modified versions
suitable for demonstrating the feature in question.
In [
Formulae produced by adapting the logical connectors in previous examples from the literature in [65] so that conjunctions became disjunctions.
Clearly the former set is of great interest as they represent a real example for the algorithms; but they all conform to a single structure and so are arguably too uniform to alone draw broad conclusions from. The second set were produced to be somehow close to the accepted test examples of the literature, but whether this is any better than inventing a new examples from scratch is debatable. in [38]. Thus while the nlsat dataset is an excellent starting point it needs to be expanded to be less uniform.
A recent experiment using machine learning [40], [38] (see
Section III-E) exposed a shortcoming in the above techniques.
To train the SVMs hundreds of examples are required (with
hundreds more then needed for validation and testing). The
dataset from the literature in [65] contained not nearly enough
examples and while the datasets discussed in the next section
were sufficient for the first experiment in [40] they proved
too uniform for [38]. We were left with no choice but to
generate large quantities of new examples, which we did using
the random polynomial generator in MAPLE. We had applied
this technique also in [
We note some other sources of large sets of benchmark
problems that represent real applications of CAD:
MetiTarski5 [
The NRA (non-linear real arithmetic) category of the SMT-LIB library6 which according to [43] consists mostly of problems originating from attempts to prove termination of term-rewrite systems.
These two data sets where included in the nlsat Benchmark Set7 produced to evaluate the work in [43]. This also included verification conditions from the Keymaera [55] and parametrized generalizations of the problem from [37]. Together this dataset had many thousands of problems. However, we note that the problems come from a small number of classes and may have some hidden uniformity.
As mentioned above, the nlsat dataset was unsuitable to use for our machine learning experiment in [38]. Every single problem within that had more than one equality was aided by GB preconditioning, in fact a great many simply had a GB containing only 1 indicating the problem had no solution. Previous experiments on small example sets suggested GB preconditioning sometimes harms CAD computation and this was verified by analysis of a large randomly generated dataset
We finish this section by noting one possible source of examples for the future.
The Todai Robot Project8 [46] is a Japanese AI project that aims to have an artificial intelligence pass the entrance examination for the University of Tokyo by 2021. A majority of questions on the Mathematics exam can be resolved by real quantifier elimination with a variety of techniques employed [41]. A key difficulty is that the natural language processing of the question derives a formula of far greater complexity than the human derived equivalent. This process derives a large bank of examples of CAD problems, as discussed in [45] for example. The authors of [45] told us there are plans to make this data set public.
After surveying the work in Section III we see that several approaches to the creation of heuristics have been taken: ranging from human identified algebraic features, justified by mathematical arguments and observations to different extents; to machine learned choices using a support vector machine. We are interested to hear how these compare with the heuristics used in SAT-solvers and what lessons can be learned.
We can identify at least two areas where CAD is in need of further heuristic development.
How best to take decisions in tandem: The work
surveyed all considered choices to be made for CAD
in isolation (assuming other choices had already been
fixed). Of course, in reality this may not be the case.
We must decide which decisions to prioritise; how
heuristics can be combined; and how the combinatorial
blow-up of decisions can be contained. Does the
SATsolving community have experience in similar issues?
There are many implementations of CAD including: the
dedicated command line program Qepcad [
How to choose between different implementations? Each implementation includes unique pieces of theory and features and excels on different examples. Ideally, we would have a single implementation which encompasses all recent advances. A more manageable step may be an overarching MAPLE command to choose between the 3 packages there. SMT-solvers are designed to use a variety of different theory solvers and how they choose between these may offer valuable lessons here.
Surveying Section IV raises a number of questions about how benchmark sets should be produced:
How best to generate large numbers of examples which are not internally uniform? How important is it that the benchmarks come from current applications? How important is it that the benchmarks have historically been used in the literature? Are randomly generated examples a fairer way to evaluate the software, or irrelevant as too far removed from applications? The SAT / SMT community posses a unified, large and growing set of benchmarks in the SMT-LIB library and so we may be able to extrapolate lessons from this. However, as noted above, this library may be too uniform [38], and comments from the anonymous referees suggest that this and other critics are already a topic of discussion in the SMT community.
Thanks to our collaborators on the work surveyed here: Russell Bradford, James Bridge, Changbo Chen, Zongyan Huang, Scott McCallum, Marc Moreno Maza, Lawrence Paulson, and David Wilson. Thanks also to the anonymous referees for their comments which improved the paper.
Most of the work surveyed here was supported by EPSRC grant EP/J003247/1. The authors are now supported by EU H2020-FETOPEN-2016-2017-CSA project SC2 (712689).