Satis ability-modulo-theories (SMT) solving is a technique to check the satis ability of logical formulas. In the context of SMT solving for non-linear real arithmetic, the cylindrical algebraic decomposition (CAD) can be embedded as a theory solver to solve sets (conjunctions) of polynomial constraints. When developing such a CAD theory solver, a design choice is given by the selection of the projection operator used in the CAD method. In this paper we provide some experimental evaluations to analyse how the choice of the projection operator a ects the computational e ciency of SMT solving.
Satis ability-modulo-theories (SMT ) solving [
When solving quanti er-free non-linear real arithmetic (QF NRA) formulas, the theory-solving part requires the invocation of a decision procedure to check the satis ability of conjunctions of polynomial equalities and inequalitites over the real domain. Besides some incomplete algorithms like interval constraint propagation [7, 8] or the virtual substitution method [20], the cylindrical algebraic decomposition (CAD ) method [5] can be expoited for this purpose.
To check the satis ability of a conjunction of polynomial constraints (which we call in the following the input formula), the CAD method works in two phases. In its rst phase it uses a projection operator to generate sets of polynomials of decreasing dimensionality; the sets of real roots of these polynomials are the borders of a nite number of semi-algebraic sets (cells), such that in each cell either all points satisfy the input formula or none of them does so. In its second phase the CAD method identi es a sample point from each of the cells and checks whether the input formula is satis ed by one of those sample points.
In the rst phase of the CAD method, di erent projection operators can be used. Some of them are incomplete, some are complete. In both cases, if one of the sample points satis es the input formula then a solution is found. When using a complete projection operator, if none of the sample points satis es the input formula then the input formula is unsatis able. However, if none of the sample points satisfy the input formula, incomplete projection operators might lead to inconclusive results.
Besides completeness, di erent projection operators di er also in the required computation e ort (both for computing the projection and generating the sample points). Naturally, one expects that a complete projection operator needs more computational e ort than an incomplete one. The natural question of how large these di erences are has been looked at, for example in [13], but a conclusive answer has not yet been found. Hence, it is not a priori known how large these di erences are, and how di erent incomplete projection operators relate in this respect.
The aim of this work is to analyse these aspects via experimental evaluation in the SMT solving context, i.e., when the CAD method gets as input only conjunctions of polynomial constraints. 2 2.1
SMT Solving
SAT-modulo-theories (SMT ) solvers [
Figure 1 illustrates the lazy SMT solving framework. The SAT solver iteratively searches for a satisfying so- input lutions for the Boolean skeleton. Dur- CNF formula constraints ing its search, it consults the theory solver(s) to check whether the Boolean abstraction Theory current Boolean assignment is consis- SAT solver solver(s) tent in the theory. To do so, it collects all theory constraints whose ab- (SAT+model) or straction proposition is true and ap- SAT/UNSAT (UNSA(UTN+KexNpOlaWnaNti)on) or pears non-negated in the formula, and those whose abstraction proposition is Fig. 1: The SMT solving framework false and appears negated in the formula. The resulting theory constraint set is sent to the theory solver(s), which checks whether it is consistent. In the full lazy approach, this communication takes place only for full Boolean solutions, whereas in the less lazy approach the theory checks are invoked more frequently also for partial solutions.
If the constraints are consistent in the theory and the SAT solver's assignment is already complete then a satisfying solution is found for the input formula. If the constraints are consistent but the Boolean assignment is not yet complete, the SAT solver continues its search. Otherwise, if the theory constraints are con icting, the invoked theory solver returns an explanation for the con ict. The explanation is often an infeasible subset fc1; : : : ; cng C of the theory solver's input constraints C, which leads to a tautology (:c1 _: : : :cn), whose abstraction can be added to the SAT solver's clause set to exclude this combination of (con icting) theory constraints from the further search.
First SMT solvers addressed more light-weight theories like equality logic and uninterpreted functions. Aiming at program veri cation, theories for arrays, bitvectors and oating-point arithmetic followed. Nowadays there are also highly tuned SMT solvers for linear arithmetic theories. Recent developments allow also to solve quanti er-free non-linear arithmetic (QF NRA) problems with SMT solvers [10, 6]. 2.2
Non-linear Real Arithmetic Given a nite set V = fx1; : : : ; xng of variables and a coe cient ring R, a polynomial p 2 R[x1; : : : ; xn] is an expression of the form p = Pid=1 ai jn=1xjeij with ai 2 R and ei;j 2 N0 for all i = 1; : : : ; d and j = 1; : : : ; n. The expressions ai jn=1xjeij are called terms, in which jn=1xjeij is a monomial and ai its coe cient. If n = 1 then we call p univariate, otherwise multivariate.
Note that a multivariate polynomial p 2 R[x1; : : : ; xn] in variables x1; : : : ; xn and coe cients from R can also be viewed as a univariate polynomial p 2 R[x1; : : : ; xn 1][xn] in the main variable xn having polynomial coe cients from the polynomial ring R[x1; : : : ; xn 1].
We use the following properties of a polynomial p with the usual meaning: the degree deg(p) and total degree tdeg(p), as well as the leading term ldt(p) and the leading coe cient lcf (p). The reductum red(p) of a non-zero polynomial p is p ldt (p); for p = 0 we de ne red(0) = 0. The kth reductum of p is de ned recursively by red0(p) = p, redj (p) = red(redj 1(p)).
QF NRA formulas are Boolean combinations of polynomial constraints p 0, where p is a polynomial and 2 f<; ; =; 6=; ; >g is a comparison operator. The QF NRA satis ability problem poses the question whether we can assign a real value to each of the variables in a QF NRA formula such that the formula evaluates to true (under the standard semantics of arithmetic operators). The satis ability problem for QF NRA is decidable [19], but it has an exponential time-complexity even for conjunctions of polynomial (in)equalities (in contrast to its linear fragment, in which conjunctions of inequalities are solvable in polynomial time). In this work we will use the cylindrical algebraic decomposition (CAD ) method [5] as a QF NRA theory solver module in the SMT solving context. 2.3
Cylindrical Algebraic Decomposition The sign of a polynomial p 2 Z[x1; : : : ; xn] under some r 2 Rn is either 1 if r evaluates p to a negative value, 1 if the evaluation results in a positive value, and 0 otherwise. We say that p is sign-invariant over a set R Rn if the sign of p is the same under all points in R. A set Pn Z[x1; : : : ; xn] of polynomials is said to be sign-invariant over R Rn if each polynomial in Pn is sign-invarint over R; the set R is then called a Pn-sign-invariant set.
A partition C = fC1; : : : ; Ckg of Rn (with Ci Rn, Ci \ Cj = ; for all i 6= j, and [iCi = Rn) is called a cylindrical algebraic decomposition (CAD ) of Rn if each Ci 2 C is a connected semi-algebraic1 set, and for each Ci; Cj 2 C and each 1 k < n the projections of Ci and Cj to Rn k (by removing the last k coordinates) are either disjoint or identical. We call the sets Ci the cells of the CAD. Intuitively, the last condition assures that the cells of the decomposition are cylindrically ordered, i.e., that the projections of the cells Ci to Rn de ne a CAD of Rn 1.
The cylindrical algebraic decomposition method takes as input a set Pn Z[x1; : : : ; xn] of polynomials and sign conditions 2 for them3, and computes a CAD for Rn such that the CAD cells are all Pn-sign-invariant. That means, it su ces to take a representative sample point from each cell and test whether it satis es the sign conditions for the input polynomials.
The CAD method works in two phases: the projection phase and the construction phase. In the projection phase, a projection operator is used to compute the polynomials that describe the boundaries of the CAD cells. Starting with the input polynomials Pn Z[x1; : : : ; xn], the projection operator is applied to Pn to compute a set Pn 1 Z[x1; : : : ; xn 1] of polynomials, for which a CAD is computed recursively. The projection operator has the important property that each CAD C0 for Pn 1 can be extended to a CAD C for Pn by de ning the cells of C to be the Pn-sign-invariant regions in the cylinders Ci0 R for each cell Ci0 2 C0. 2.4
Projection operators Assume two multivariate polynomials p; q 2 Z[x1; : : : ; xn], which can also be seen as univariate polynomials p = Pik=0 aixin and q = Pli=0 bixin in xn with polynomial coe cients ai; bi 2 Z[x1; : : : ; xn 1]. Assume furthermore that k; l 1 with ak 6= 0 and bl 6= 0, i.e., deg (p) = k 1 and deg (q) = l 1 are the degrees of the polynomials in xn. The Sylvester matrix of p and q (with respect to xn) 1 A set R Rn is semi-algebraic if it can be described by a conjunction of polynomial constraints.
polynomial constraint sets. is the following (k + l) (k + l)-matrix.
0 ak B B B B B
B Syl xn (p; q) := B
BB bl B B B B @ ak bl . . . . . .
ak bl a0 b0 a0 : : : b0 : : : . . . . . .
19 > > C=>
CC l a0 CCCC>>>;
C9 CCC>>>= C k C A>> > ; b0
For some 0 i j k+l let Mi;j be the the matrix obtained from Syl xn (p; q) by deleting the last j rows of p coe cients, the last j rows of q coe cients and the last 2j + 1 columns except the column m + n i j.
{ The j-th subresultant of p and q is de ned as Sj (p; q) = Pj i=0 det (Mj;i)xin. { The j-th principal subresultant coe cient of p and q is pcsj (p; q) = det (Mj;j ) (i.e., the leading coe cient of Sj (p; q)). { The resultant of p and q is de ned as res(p; q) = det (Syl x(p; q)) = psc0(p; q). { The pcs set of p and q is de ned as
P SC(p; q) = fpcsj (p; q) j 0 j min(k; l); pcsj (p; q) 6= 0g: { The reducta set of p is de ned as
RED(p) = fredi(p) j 0 i k; redi(p) 6= 0g:
Assume in the following a set Pn = fp1; : : : ; pmg Z[x1; : : : ; xn 1][xn] of polynomials, which we view as polynomials in xn with polynomial coe cients from Z[x1; : : : ; xn 1]. Let furthermore d be an upper bound on the degrees of the polynomials pi in the main variable xn. A projection operator takes Pn as input and generates a set Pn 1 Z[x1; : : : ; xn 1] of polynomials as output.
Next we describe the projection operators whose e ciency we will compare in Section 3. Due to space limitations, we refer for more detailed explanations to the references given below.
Collins' projection operator [5] projC1(Pn) = projC(Pn) = projC1(Pn) [ projC2(Pn) [ [
(fldcf (r)g [ P SC(r; r0)) projC2(Pn) =
P SC(r1; r2) pi2Pn r2RED(pi)
[ [ 1 i<j m r12RED(pi)
r22RED(pj) Using Collins' operator in the CAD method, a Pn-sign-invariant CAD of Rn can be established. The number of polynomials in projC(Pn) is dominated by m2d3. Note that Collins' operator has been replaced by Hong's operator below without any drawback. As the rst projection operator, we include it nevertheless in this comparison to give an impression on the progress made.
Hong's projection operator [9] Hong showed that within P rojC2, the added psc sets have redundancies and proposed the following operator: projH2(Pn) = projH(Pn) = projC1(Pn) [ projH2(Pn) [ [
P SC(r; pj ) 1 i<j m r2RED(pi) The number of polynomials included in projH(Pn) is dominated by m2d2, which implies a possible signi cant impact on the overall performance compared to Collins' operator, since the degree bound impacts the size in quadratic instead of cubic order.
McCallum's projection operator [14] Let Pn0 = fp01; : : : ; p0mg be the nest squarefree basis of Pn.
projM (Pn) = projM1(Pn0 ) [ projM2(Pn0 ) [ projM1(Pn0 ) = projM2(Pn0 ) =
[ pi2P n0
[ 1 i<j m 0 fres(pi; pj )g
[ fcontx (pi)g
1 [ r2RED(pi) fldcf (r)gA
Although it seems substantially di erent to the previous operators, McCallum showed that one could also rede ne Collins' operator to operate with subdiscriminants rather than subresultants such that projM projC (see Chapter 3.1 in [14]). McCallum's operator not only requires the use of nest square-free basis in each step, but it can only guarantee the correctness of a CAD procedure with his operator when the input polynomials are well-oriented. In addition to this restriction, the nite amount of real roots of the well oriented polynomials in the set projM (A) requires a slight modi cation of the lifting phase to preserve the order-invariance in every step. McCallum also provided incomplete methods to check whether a polynomial has nitely many zeros or not. It is also possible to detect if the input polynomials were not well-oriented during lifting phase, if one keeps track while creating sample points whether they present a space of positive dimension or not. If a sample point p 2 Ri that represents a cell of positive dimension { thus was chosen to represent a sector in some lower dimensional lifting step { causes a (i + 1)-variate projection polynomial to vanish, then this polynomial has an in nite number of zeros: all sample points that could have been chosen instead of the one that lead to p in this lower dimensional lifting step. McCallum further argued that the vast majority of polynomials are well-oriented including all polynomials with at most three variables. Brown's projection operator While McCallum's operator produces order-invariant CADs which might be needed in some scenarios, it is not required to solve QF NRA formulas, because only the sign-invariance is mandatory there. Brown showed that it is su cient for the projM1 operator to only contain the leading coe cient of each polynomial instead of all coe cients. This however needs to come along with further modi cations in the lifting stage.
Let again Pn0 = fp01; : : : ; p0mg be the nest square-free basis of Pn. projB(Pn) = projB1(Pn0 ) [ projM2(Pn0 ) [ projB1(Pn0 ) =
[ fdiscr(pi)g [ fldcf (pi)g
Brown also made another modi cation to the lifting stage, that allows the CAD to stay correct in some cases, where the polynomials are not well-oriented. Note that essentially projB projM projH projC.
Further projection operators There exist a number of further projection operators that we do not consider in this paper. Lazard [12] improved on McCallum's operator, however the proof contained an error that was only recently xed by [15]. Seidl and Sturm [17] proposed an specialized version of Hong's operator for what they call a partial CAD targeting inputs with many parameters. Motivated by applications in SMT solving there are also results on how to compute projections only locally for speci c cells, for example by Strzebonski [18] or Brown and Kosta [4]. 3
We implemented the four projection operators presented in the previous section in the SMT solver SMT-RAT [6]. The test setting was based on SMT-RAT's CAD theory module, which uses some optimizations, including the following. Constants get removed instantly and are not projected down. The same holds for positive de nite and negative de nite functions, as they are always sign- and order-invariant. It does however not provide the calculation of a square-free basis yet { and thus this restriction of McCallum's and Brown's operator is ignored { and also does not attempt to x the projection if a polynomial vanishes during lifting. Both are under active development and some preliminary results are presented at the end.
While SMT-RAT can be run in an incremental fashion and thus can deal with backtracking scenarios by o ering ways of adding and removing polynomials on each projection level, this feature was not utilized here as the study of interest
is the e ciency of the operators by the theoretical improvements, that were made on the eld of CAD. See section 3.2 for more details on how incremental projection works in SMT-RAT. Note that we do not look at the question of variable ordering here. It is well established that choosing a proper variable ordering can have a huge impact on the projection. A comparison of projection operators using a variable ordering tuned to the speci c projection operator would be very interesting, but we have not done this yet. As for this paper, we use a static variable ordering that is essentially the order in which the variables are declared in the input formula.
We used non-linear benchmarks from the SMT competition 2014 and instantiated SMT-RAT in four variants, using the four di erent projection operators in its CAD theory solver. 3.1
CAD projection only As a rst experiment, the CAD modules were programmed to project all polynomials of an SMT problem instance down to the univariate level and then stop. The tests were run on an AMD Opteron 6172 with a time limit of 60 seconds. Table 1 shows for how many benchmarks the projections could be completed within the time limit, when using the di erent projection operators.
In a next step we identi ed those benchmarks for which the projection could be completed within the time limit using all four operators. These benchmarks are exactly those which Collins' operator was able to handle. The performance of the four participants on these benchmarks was observed more closely. As factors having a major implact on performance, the number of di erent polynomials, their maximum degree (in the respective main variable) and their maximum total degree over all polynomials were identi ed. Note that other factors like the number of terms or the coe cient size were not considered here. This information is shown in Table 2, based on the average and the median, as well as the 75% quartile, being the largest data point that is smaller than 25% of the data and the maximum.
From the theoretical analysis, we expect to have a clear order on the projection operators as we established projB projM projH projC. We
Collins 10,89 6 16 99 Hong 8,62 5 12 57 McCallum 6,06 4 8 31 Brown 5,29 4 7 25
also know that using McCallum's (and Brown's) operator have the theoretical drawback of incompleteness. Therefore we try to measure how signi cant the individual gaps are and whether the incompleteness actually occurs in practice. Unfortunately, only a small number of our benchmarks contain more than three variables and only these could reveal this incompleteness.
These questions cover the performance of the di erent projection operators in a single CAD computation, but it is not at all clear whether these results immediately transfer to the SMT setting. Here, multiple incremental calls are performed and { if the problem turns out to be satis able { the computation can be aborted if a single satisfying sample is found. How the di erent operators perform within a full SMT solver is thus analyzed separately.
We tracked the number of polynomials, the maximum degree and the maximum total degree for the rst 4 projection levels and got the results depicted in the Tables 3, 4, 5 and 6. Only few solved instances caused projections with more then 5 variables, which is why this restriction is made. Note that the numbers for the maximum degree and the maximum total degree are essentially the same for all projection levels, only on the rst level a slight di erence exists. This shows that most benchmarks have a rather simple structure as most polynomials are univariate and the multivariate polynomials never have the maximum degree.
We also noticed that with Brown's operator, at times a whole projection level could be skipped. This can happen if a variable is technically present, but does not contribute to any polynomial that actually needs to be considered for projection. This was the case for 11 instances on projection level 1 and for 137 instances on projection level 2. The improvements of Brown's operator compared to McCallum's are rather small and they can handle the exact same benchmarks. This however is no big surprise, as the real strength of Brown's operator is in
Brown the lifting phase, where the amount of lifting points are kept smaller due to the manual adding of points, only when it is necessary.
Looking at the statistics that regard polynomial degrees, Collins' and Hong's operators scored similar results. The same can be seen, when comparing McCallum's operator to the one of Brown. However, there is a major gap between these two groups (Collins' approach vs McCallum's design). This indicates the huge step, that McCallum's operator was able to make in the context of CAD.
Though a somewhat poor performance of Collins's operator was to be expected, it performs much worse than we expected. The increase in the number of polynomials from level 1 to level 2 was about 72 while Hong's operator kept it at about 18 and both McCallum's and Brown's operator stayed below 3. Also the maximum degree is much higher for Collins's operator compared to McCallum's while there is no signi cant di erence between Collins's and Hong's operator or McCallum's and Brown's operator. Altogether, Hong's operator seems to be a viable possibility for cases where McCallum's operator is not applicable as it at least reduces the number of polynomials signi cantly. 3.2
Full SMT solver In a second test run, the previously selected 5698 samples were given to the full SMT solver. The results are shown in Table 7 with a timeout of again 60 seconds. Note that in this scenario, most benchmarks would not cause a single call to the CAD module but multiple theory calls due to the Boolean structure of the problems. We can see that only a relatively small amount of benchmarks is above the timeout, indicating that SMT-RAT does a reasonably good job in exploiting the incremental nature of these theory calls. The previous scenario
Brown also considered all polynomials present in the problem while here, the theory solver will oftentimes never see the full set of constraints as a subset of these is enough to satisfy the formula or to establish unsatis ability.
Furthermore, SMT-RAT interleaves the projection and lifting phases so that a satisfying assingment can be found before the projection is nished. To do that, the projection operator is deconstructed into what we call projection candidates, for example the resultant of two polynomials. Whenever a projection candidate is calculated, new polynomials may appear one level below and thereby spawn new projection candidates on this level. All these projection candidates can be processed individually, thus the projection is decomposed into many individual tasks. After every projection candidate, lifting is continued on the incomplete projection hoping that a satisfying assignment is found.
This can speed up the overall solving time signi cantly, but also has some other e ects that impede gaining any insight about the projection operators in this scenario. Note that the projection operators not only produce di erent polynomials, but may also generate the same polynomials in a di erent order. Every newly produced polynomial induces new sample points which may be satisfying and thus may immediately terminate the solving process. Hence, the purely heuristic decisions of projection order { the order in which projection candidates are processed { and lifting order { the order in which sample points are lifted { can easily supersede any impact of the projection operator. Thus it is even plausible that generating more polynomials could have a bene cial e ect, at least on satis able problems.
Close analysis within the SAT solver enables SMT-RAT to lter out constraints based on the Boolean structure in many cases. In fact, some of the benchmarks, that caused the greatest amount of polynomials in the rst test run, turned out to
be solvable in a very short amount of time. One example is the benchmark \metitarski/polypaver-bench-sqrt-3d-chunk-0479.smt2". Generating a total amount of 24575 polynomials in a full projection, it could be solved in 33 milliseconds due to some contradicting bounds.
The running times on the benchmarks that could be nished are given in the last four columns of Table 7. This data shows that the above e ects dominate the whole solving process. More than 75% of the solvable examples are solved in less than 75 milliseconds with any projection operator, Collins's even being the fastest for the 75% quartile. Note that the four solvers solve di erent benchmarks, for example the solver using McCallum's operator solves instances that Brown's operators cannot cope with and vice-versa. Hence these numbers are a bit skewed. Though it may be surprising that Brown's operator only has a small lead over McCallum's, this can be explained by the structure of the inputs. Brown's operator eliminates coe cients from the projection, but as we have seen in the comparison between the maximum degree and the maximum total degree, the coe cients will usually have a small degree. Furthermore, removing these coe cients of small degree may actually hinder the solver. It may be su cient to
20 40 runtime of McCallum (a) Default ordering consider these coe cients to generate a satisfying solution so that we can spare the e ort of computing resultants and discriminants.
McCallum vs. Brown We now want to compare McCallum's and Brown's operator in more detail. First we compared the overall performance of the solvers with McCallum's and Brown's operator in Figure 2a where every cross represents a single SMT benchmark. As expected the solvers behave rather similarly and Brown's operator tends to solve more instances, but still a notable number of outliers exist for both directions. It seems that in a full SMT solver, being lucky in the heuristics can be more important than the choice of the projection operator. This suggests that running multiple di erent projections in parallel could be bene cial. Note that if the projection order of McCallum's operator is forced to mirror the one of Brown's operator { that is the coe cients are projected last { both behave almost identically.
In order to make use of a portfolio approach, several strategies that behave as di erently as possible are desirable. We tried several modi cations to the projection order, including deferring the projection of resultants as they tend to lead to the greatest increase of polynomial degrees. Figure 2b shows the two solver con gurations that diverged most: McCallum with our regular projection order that is mostly based on the polynomial degree, and Brown's operator deferring resultant computations.
As for the question whether the incompleteness of McCallum's operator is a problem in practice, we performed a test on 5889 benchmarks from the SMT competition, being all those that were not trivially solved before even reaching the CAD module. In 510 cases some polynomial vanished and 353 from those were found to be satis able. Note that a vanishing polynomial does not imply that the projection is incomplete: if the polynomial vanished over a zerodimensional cell, this could be repaired by adding delineating polynomials. The remaining 157 were found to be unsatis able, and all of them are in fact unsatis able. Hence we can conclude that McCallum's operator indeed produces incomplete projections for actual benchmarks, but they did not cause a single error on our benchmark set.
We are working on using CoCoALib [
Altogether, we can recognize the theoretically expected order of the di erent projection operators with respect to the number of solved instances, though it may not be as signi cant as expected and is not directly re ected in the observed solving times. While Hong's operator is a signi cant improvement over Collins's and McCallum's again improves on Hong's operator, the di erence between McCallum's and Brown's operator is small, though existent. 4
In this paper we provided some experimental results to compare the e ciency of di erent projection operators in the cylindrical algebraic decomposition method, both in a isolated theory solver and within a full SMT solver. In the isolated setting, the practical analysis showed that the theoretical results hold on practical examples. In a full SMT solver however, other e ects tend to dominate for individual instances, but the overall trend is still evident.
Future work might include a closer look at the side cases, when using Brown's projection on examples, where points need to be added to the projection. Also the runtimes on the tests, where Brown's operator competed versus McCallum's operator, suggest a dual approach employing multiple projection operators in parallel.
Another quite promising approach that is not yet considered is to use
equational constraints to simplify the CAD procedure as described in [
decomposition. In: Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134{183. Springer (1975)
open source C++ toolbox for strategic and parallel SMT solving. In: Proc. of SAT'15. LNCS, vol. 9340, pp. 360{368. Springer (2015)
In: Proc. of FMCAD'10. pp. 81{90. IEEE (2010)
ing a componentwise Newton method. Tech. Rep. 2/1997, Inst. fur Angewandte
composition. ISSAC '90 Proceedings of the international symposium on Symbolic and algebraic computation pp. 261{264 (1990) 10. Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Proc. of IJCAR'12.
LNAI, vol. 7364, pp. 339{354. Springer (2012) 11. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View.
12. Lazard, D.: An improved projection for cylindrical algebraic decomposition. In:
Abhyankar's 60th birthday conference. p. 467. Springer Verlag (1994) 13. McCallum, S.: An Improved Projection Operation for Cylindrical Algebraic Decomposition (Computer Algebra, Geometry, Algorithms). Ph.D. thesis, The University of Wisconsin - Madison (1984), aAI8500835 14. McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. Tech. rep., University of Wisconsin Madison (1985) 15. McCallum, S., Hong, H.: On using lazard's projection in cad construction. Journal of Symbolic Computation 72, 65 { 81 (2016), http://www.sciencedirect.com/science/article/pii/S0747717115000097 16. Nelson, G., Oppen, D.C.: Simpli cation by cooperating decision procedures. ACM
Transactions on Programming Languages and Systems 1(2), 245{257 (1979) 17. Seidl, A., Sturm, T.: A generic projection operator for partial cylindrical algebraic decomposition. In: Proceedings of the 2003 International Symposium on Symbolic and Algebraic Computation. pp. 240{247. ISSAC '03, ACM, New York, NY, USA (2003), http://doi.acm.org/10.1145/860854.860903 18. Strzebonski, A.: Cylindrical algebraic decomposition using local projections. Journal of Symbolic Computation 76, 36 { 64 (2016), http://www.sciencedirect.com/science/article/pii/S0747717115001170 19. Tarski, A.: A decision method for elementary algebra and geometry. Tech. rep.,
20. Weispfenning, V.: Quanti er elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85{101 (1997)